Compact Route120 kernel closer

This sidecar keeps the Route118/Route120 public kernel closure compact while removing one avoidable leaf from the Route110 raw-head kernel provider.

The least-kernel candidate is theorem-level: for the selected upper chief-factor subgroup P, the candidate K = P is Y-normal, lies in P, and satisfies K S = P. Downstream still needs universal leastness for the selected candidate, and still uses the compact Frattini collapse, raw quotient tower, and same-raw-tower invariant packets.

No integrated route imports this module yet.

Least kernel with theorem-level candidate

structure Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.UpperLeastKernelSelectedData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type

Selected least-kernel packet for the theorem-level upper chief-factor candidate.

• candidate : MinimalBlockKernelCandidateData chief
• universal : MinimalBlockKernelLeastUniversalData self.candidate

def Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.UpperLeastKernelSelectedData.leastOverChief {p : FramedPair} {chief : NonScalarChiefFactor p} (D : UpperLeastKernelSelectedData chief) : MinimalBlockKernelLeastOverChiefData chief

Forget the selected upper-candidate/universal packet to the route-ready least-over-chief interface.

Equations

• D.leastOverChief = { toMinimalBlockKernelCandidateData := D.candidate, minimal_K := ⋯ }

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.leastCandidateData_from_compactRoute120Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Candidate half of the compact Route120 split.

This is the theorem-level manuscript candidate K = P, so it does not use the public minimalBlock_kernelLeastCandidateData leaf.

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.upperLeastKernelSelectedData_from_compactRoute120Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (UpperLeastKernelSelectedData chief)

Selected universal leastness for the theorem-level upper candidate.

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.leastOverChiefData_from_compactRoute120Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route-ready least-over-chief data recovered from the selected upper candidate.

Compact Frattini/raw/invariant surfaces

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.frattiniCollapseFullData_from_compactRoute120Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelFrattiniCollapseFullData K)

Compact Frattini-collapse packet preserved from Route118.

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.rawQuotientTowerData_from_compactRoute120Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Compact raw quotient tower packet preserved from Route118.

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.invariantActualProofs2Data_from_compactRoute120Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockInvariantActualProofs2Data D)

Compact same-raw-tower invariant packet preserved from Route118.

Route-ready kernel provider

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.kernelModuleConcreteProvenanceData_from_compactRoute120Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete provenance through the compact Route120 kernel tower.

Compared with Route110 raw-head, this selects the least-kernel candidate theorem-level and therefore avoids minimalBlock_kernelLeastCandidateData, while preserving the other compact kernel leaves.

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.lowerGroupModuleData_from_compactRoute120Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through the compact Route120 kernel tower.

theorem Q2Presentation.Induction.MinimalBlockKernelCompactRoute120Closers.rawSimpleHeadSemanticData_from_compactRoute120ClosersLower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

Selected-tower simple-head semantic packet through the same compact invariant leaf used by Route110 raw-head.

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

Route118/Route120-compatible compact kernel provider.

It has the same consumer shape as minimalBlock_groupTowerData_from_kernelRoute110RawHeadClosers, but its compact kernel closure drops minimalBlock_kernelLeastCandidateData.

Public route-ready aliases

theorem Q2Presentation.Induction.minimalBlock_kernelLeastCandidateData_from_compactRoute120Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Public candidate-half closer for the compact Route120 kernel provider.

theorem Q2Presentation.Induction.minimalBlock_kernelUpperSelectedLeastUniversalData_from_compactRoute120Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCompactRoute120Closers.UpperLeastKernelSelectedData chief)

Public selected upper-candidate/universal packet for the compact Route120 kernel provider.

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

Public least-over-chief provider for the compact Route120 kernel provider.

theorem Q2Presentation.Induction.minimalBlock_lowerGroupModuleData_from_kernelCompactRoute120Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Public lower-tower provider for the compact Route120 kernel provider.

theorem Q2Presentation.Induction.minimalBlock_rawSimpleHeadSemanticData_from_kernelCompactRoute120Closers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

Public selected-tower simple-head alias for the compact Route120 kernel provider.

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

Public drop-in kernel provider matching minimalBlock_groupTowerData_from_kernelRoute110RawHeadClosers.