Documentation

Q2Presentation.Induction.MinimalBlockKernelRoute85Closers

Route85 kernel closers for the minimal-block route #

This sidecar advances the Route88 kernel frontier without editing the integrated Route88 file. Route84 already lowers the raw tower to one coherent literal R, M, T, C packet and Route83 projects the simple-head fields from the actual invariant packet. The remaining Route84 provider closure still passes through ten Route81 least/Frattini atoms.

Route85 replaces those atoms by two Section 7 packets:

a selected least-kernel packet, matching the manuscript choice of K normal in Y, K <= P, minimal subject to K S = P;
a Frattini--centralizer collapse packet for that selected K, matching the manuscript proof that R = Phi(K) is nontrivial, central elementary abelian, and that K^4 = 1.

The downstream Route55 consumer still sees the same least, concrete Frattini, raw object/action/bridge, raw-head, and simple-head fields, so the public provider is a drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute84Closers.

Selected least kernel #

structure Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.LeastKernelSectionData {p : FramedPair} (chief : NonScalarChiefFactor p) :

Route85 manuscript-shaped selected least-kernel packet.

selected : MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData chief

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.LeastKernelSectionData.least {p : FramedPair} {chief : NonScalarChiefFactor p} (D : LeastKernelSectionData chief) :

MinimalBlockKernelLeastOverChiefData chief

Forget the Route85 selected least-kernel packet to the consumed interface.

Equations

D.least = D.selected.least

Instances For

axiom Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.leastKernelSectionData {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (LeastKernelSectionData chief)

Residual Route85 selected least-kernel packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.leastKernelSelectedData_from_route85 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData chief)

Route78-shaped selected least-kernel packet recovered from Route85.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.leastOverChiefData_from_route85 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route85 least-over-chief packet.

Frattini--centralizer collapse #

structure Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.FrattiniCentralizerCollapseSectionData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Route85 manuscript-shaped Frattini--centralizer collapse packet.

The fields are the selected pieces needed by the existing Route78/Route63 conversion API, but they are owned by one selected K, following lem:collapse rather than the Route81 atomization.

internal : MinimalBlockKernelRoute78FrattiniClosers.FrattiniInternalSelectedData K
centralizer : MinimalBlockKernelRoute78FrattiniClosers.FrattiniCentralizerSelectedData K
fourthPower : MinimalBlockKernelRoute78FrattiniClosers.FourthPowerKernelSelectedData K
elementaryLayer : MinimalBlockKernelRoute78FrattiniClosers.FrattiniSquareCommutatorLiteralExponentData K

Instances For

axiom Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniCentralizerCollapseSectionData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (FrattiniCentralizerCollapseSectionData K)

Residual Route85 Frattini--centralizer collapse packet for the selected least kernel.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniInternalSelectedData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniInternalSelectedData K)

Selected internal-Frattini witness projected from the Route85 collapse packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniInternalNonidentityData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniInternalNonidentityData K)

Route67 internal nonidentity packet recovered from Route85.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniNontrivialData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniNontrivialData K)

Route85 Frattini nontriviality from the selected internal witness.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniCentralizerSelectedData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniCentralizerSelectedData K)

Selected centralizer core/image data projected from the Route85 collapse packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniCentralizerHallCommutatorData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniCentralizerHallCommutatorData K)

Route67 Hall-commutator centralizer packet recovered from Route85.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniCentralizerStepData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K)

Route85 centralizer step.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniCentralData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniCentralData K)

Concrete centrality packet from the Route85 centralizer step.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.fourthPowerKernelSelectedData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FourthPowerKernelSelectedData K)

Selected fourth-power core/image data projected from the Route85 collapse packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.fourthPowerKernelCommutatorData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FourthPowerKernelCommutatorData K)

Route67 fourth-power kernel/commutator packet recovered from Route85.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.fourthPowerMapVanishesData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K)

Route85 fourth-power vanishing.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.fourthPowerData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFourthPowerData K)

Concrete fourth-power packet from the Route85 fourth-power step.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniSquareCommutatorLiteralExponentData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniSquareCommutatorLiteralExponentData K)

Literal exponent-two implication projected from the Route85 collapse packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniSquareCommutatorLayerData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K)

Route85 square/commutator layer packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniElementaryLayerData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniElementaryLayerData K)

Route85 elementary Frattini layer from the literal square/commutator data.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniExponentData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniExponentData K)

Concrete exponent-two packet from the Route85 elementary layer.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.frattiniData_from_route85 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Concrete Frattini packet assembled through Route85 Section 7 packets.

Route55-shaped provider #

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.kernelRoute55Data_from_route85 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute55.KernelRoute55Data chief)

Route55-shaped packet using Route85 least/Frattini packets, Route84 raw literal tower data, and Route83 actual simple-head projections.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.kernelRoute54Data_from_route85 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute54.KernelRoute54Data chief)

Route54 coherent data supplied through Route85.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.consumedData_from_route85 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute53.ConsumedData chief)

Route53 consumed data supplied through Route85.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.groupInvariantRouteData_from_route85 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route85.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.groupTowerData_from_route85 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Group-tower provider using Route85 least/Frattini lowering.

Public provider #

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

Nonempty (MinimalBlockGroupTowerData p chief)

Drop-in kernel provider using Route85 least/Frattini lowering.