Route26 minimal-block kernel/head refinement

Route25 keeps the concrete K, Phi(K), R, M, T, C tower split into the current fine Section 7 leaves, and closes the head nontriviality field from the quotient-head action leaf. This sidecar makes two further theorem-level reductions while leaving routed files untouched:

• the least-kernel candidate is the chief-factor upper subgroup itself, so only the universal leastness packet remains for that split;
• the head/invariant layer is assembled directly from the route21 semantic leaves, avoiding the route10 raw dual/functionals/character residual names.

Least K with theorem-level candidate

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26.leastOverChiefOfUpperCandidate {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelCandidateData chief) (L : MinimalBlockKernelLeastUniversalData K) : MinimalBlockKernelLeastOverChiefData chief

Route26 closes the candidate half of the least-kernel split by taking the chief-factor upper subgroup, leaving only universal leastness for that selected candidate.

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26.leastOverChiefOfUpperCandidate K L = { toMinimalBlockKernelCandidateData := K, minimal_K := ⋯ }

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26.minimalBlock_kernelLeastOverChiefData_from_route26UpperCandidate {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route26 replacement for the split least-kernel construction.

Head/invariant data from route21 semantic leaves

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26.headInvariantOfRoute21Leaves {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (H : MinimalBlockRawInvariantHyperplanesContainTData D) (S : MinimalBlockRawHeadNonzeroStableEqTopData D) (A : MinimalBlockRawHeadActionNotPointwiseTrivialData D) (X : MinimalBlockRawLowerInvariantCharacterExistsData D) : MinimalBlockHeadInvariantSemanticRoute12Data D

Same-raw-tower Route12 semantic packet from the four route21 head leaves.

Equations

• ⋯ = ⋯

Route26 packet and projections

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26Data {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route26 coherent Section 7 kernel/head packet.

The lower tower remains the route25 concrete tower. The head/invariant data is stored in the route12 semantic form produced from route21 leaves, so the final provider avoids the route10 raw head/functionals/character residual names.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattiniFull : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawQuotient : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• headInvariant : MinimalBlockHeadInvariantSemanticRoute12Data self.rawQuotient.rawData.rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26Data.frattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute26Data chief) : MinimalBlockKernelModuleConcreteFrattiniData P.least

The concrete Frattini packet carried by Route26.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26Data.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute26Data chief) : MinimalBlockKernelModuleConcreteRawData P.least ⋯

The coherent raw data carried by Route26.

Equations

• P.rawData = P.rawQuotient.rawData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26Data.actualProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute26Data chief) : MinimalBlockKernelModuleActualProofs chief

The actual lower kernel/module packet selected by Route26.

Equations

• P.actualProofs = Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24.actualProofsOfRawQuotient P.least ⋯ P.rawQuotient

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26Data.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute26Data chief) : MinimalBlockLowerGroupModuleData chief

Lower group/module data selected by Route26.

Equations

• P.lowerGroupModuleData = P.actualProofs.lowerGroupModuleData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26Data.route20Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute26Data chief) : MinimalBlockKernelConcreteRoute20Data chief

Route20-compatible same-tower packet recovered from Route26.

Equations

• P.route20Data = { lower := P.lowerGroupModuleData, headInvariant := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute26Data.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute26Data chief) : MinimalBlockGroupTowerData p chief

Route26 group-tower data.

Equations

• P.groupTowerData = P.route20Data.groupTowerData

Route26 assembly theorems

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute26Data_from_route21HeadSplit {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute26Data chief)

Route26 packet from the route25 concrete lower tower, with a theorem-level least candidate and a route21 semantic head split.

theorem Q2Presentation.Induction.minimalBlock_groupTowerData_from_kernelConcreteRoute26 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Route26 replacement for the current minimal-block group-tower provider.