Route40 minimal-block kernel/head refinement #

This sidecar is intentionally standalone: no routed or root files import it yet.

Route40 is a drop-in kernel/head provider over the Route39 sidecar. It keeps the Route39 selected K and raw quotient transport route, but strictly lowers two Route39 residual names:

MinimalBlockKernelConcreteRoute39.frattiniCentralizerCollapseData is replaced by the field-level Section 7 collapse packets for the same literal R = Phi(K): a nonidentity witness, centrality in K, fourth-power vanishing on K, and exponent two on R. Normality remains theorem-level from characteristicity of Phi(K) in the selected normal K.
minimalBlock_invariantActualProofs2Data is replaced by the third-pass same-tower split from MinimalBlockInvariantActualProofs3, matching manuscript Lemma 7.1 (lem:simplehead).

Manuscript anchors: reference/q2_manuscript.tex, Section 7, pp. 40--42: Lemma 7.1 "Simple head" and Lemma 7.2 "Frattini--centralizer collapse".

Frattini-collapse through field-level Section 7 packets #

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute40.frattiniData_from_route40Split {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Route40 Frattini packet for the selected least kernel K.

This is the Route39 collapse assembly with the monolithic frattiniCentralizerCollapseData residual replaced by field-level manuscript-shaped obligations from Section 7, Lemma 7.2:

Phi(K) has a nonidentity element;
Phi(K) is centralized by K;
K^4 = 1;
Phi(K) has exponent two.

The normality field is still proved theorem-level from K.Normal.

Raw quotient transport reused from Route39 #

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute40.rawQuotientTowerData_from_route40Transport {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route40 keeps Route39's finer raw quotient transport packets for the same K, Phi(K) tower.

Concrete provenance and same-tower simple head #

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute40.kernelModuleConcreteProvenanceData_from_route40 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete provenance through the Route40 split collapse and Route39 raw transport.

Compared with Route39, this theorem no longer calls MinimalBlockKernelConcreteRoute39.frattiniCentralizerCollapseData; its Frattini frontier is the field-level Lemma 7.2 split above.

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute40.provenanceConcreteFinalPieces_from_route40 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance through Route40 kernel data and the third-pass same-tower simple-head split.

This removes the Route39 dependency on the monolithic minimalBlock_invariantActualProofs2Data residual. The remaining head-side frontier is the finer Lemma 7.1 split exposed by MinimalBlockInvariantActualProofs3.

source