Route116 kernel closers #

This sidecar leaves all integrated route files untouched. It sits below MinimalBlockKernelRoute114Closers and makes two route-neutral refinements of the Section 7 kernel provenance frontier:

the selected least kernel is built from the theorem-level upper chief-factor candidate, so the provider no longer depends on the residual MinimalBlockKernelRoute81Closers.leastKernelCandidateData atom;
the raw quotient tower is assembled directly through the Route43 literal transport packet, so the raw-tower theorem itself does not drag in the simple-head semantic atoms that are only needed later for the invariant packet.

The final group-tower provider has the same consumer shape as the Route114 kernel provider, with a strictly smaller overall kernel axiom closure.

Least kernel #

source

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

Type

Route116 selected least-kernel packet.

The candidate is supplied theorem-level by the upper chief-factor subgroup; the remaining residual is only universal leastness for that selected candidate.

candidate : MinimalBlockKernelCandidateData chief
universal : MinimalBlockKernelLeastUniversalData self.candidate

Instances For

source

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

MinimalBlockKernelLeastOverChiefData chief

Forget the selected upper-candidate/universal packet to the least-over-chief interface consumed downstream.

Equations

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

Instances For

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute116Closers.leastCandidateData_from_route116Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelCandidateData chief)

Candidate half of the Route116 least-kernel split.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute116Closers.upperLeastKernelSelectedData_from_route116Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (UpperLeastKernelSelectedData chief)

Selected universal leastness for the theorem-level upper candidate.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute116Closers.leastOverChiefData_from_route116Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelLeastOverChiefData chief)

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

Frattini collapse #

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute116Closers.frattiniCollapseFullData_from_route116Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelFrattiniCollapseFullData K)

Route116 Frattini-collapse packet. The proof-step frontier is the Route81 collapse split already exposed below Route114.

Raw quotient tower #

source

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

Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route116 raw-quotient tower packet.

This uses the direct Route43 literal/transport assembly. In contrast to the Route114 raw-tower theorem, it does not route through the actual invariant packet and therefore avoids the three simple-head semantic atoms that are not part of the raw tower itself.