Route90 kernel closers for the minimal-block route

This sidecar is isolated from the integrated routes. It provides a drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute85Closers while removing the four current Route90 kernel residual names from the provider closure:

• minimalBlock_invariantActualProofs2Data;
• MinimalBlockKernelRoute84Closers.rawLiteralObjectActionTowerData;
• MinimalBlockKernelRoute85Closers.frattiniCentralizerCollapseSectionData;
• MinimalBlockKernelRoute85Closers.leastKernelSectionData.

The replacement keeps the same Route55 consumer surface. The least-kernel and Frattini-collapse Section 7 packets are reassembled from the Route81 split packets; the literal R, M, T, C tower is reassembled from the Route43 literal object/action packets; and the simple-head packet is projected from MinimalBlockInvariantActualProofs3.

Route85 Section 7 packets from lower split packets

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.leastKernelSectionData_from_route90 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute85Closers.LeastKernelSectionData chief)

Route90 replacement for Route85's selected least-kernel Section 7 packet.

This proves the Route85 packet from the Route81 candidate/universal split rather than using MinimalBlockKernelRoute85Closers.leastKernelSectionData.

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

Least-over-chief data recovered through the Route90 selected Section 7 packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniCentralizerCollapseSectionData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute85Closers.FrattiniCentralizerCollapseSectionData K)

Route90 replacement for Route85's Frattini--centralizer collapse packet.

This is the manuscript Lemma 7.2 packet rebuilt from the Route81 lower split: internal nonidentity in Phi(K), centralizer core/image, fourth-power core/image, and the generated elementary Frattini layer.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniInternalSelectedData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniInternalSelectedData K)

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniInternalNonidentityData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniInternalNonidentityData K)

Route67 internal nonidentity packet recovered from Route90.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniNontrivialData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNontrivialData K)

Route90 Frattini nontriviality from the selected internal witness.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniCentralizerSelectedData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniCentralizerSelectedData K)

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniCentralizerHallCommutatorData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniCentralizerHallCommutatorData K)

Route67 Hall-commutator centralizer packet recovered from Route90.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniCentralizerStepData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K)

Route90 centralizer step.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniCentralData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniCentralData K)

Concrete centrality packet from the Route90 centralizer step.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.fourthPowerKernelSelectedData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FourthPowerKernelSelectedData K)

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.fourthPowerKernelCommutatorData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FourthPowerKernelCommutatorData K)

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.fourthPowerMapVanishesData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K)

Route90 fourth-power vanishing.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.fourthPowerData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFourthPowerData K)

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniSquareCommutatorLiteralExponentData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniSquareCommutatorLiteralExponentData K)

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniSquareCommutatorLayerData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K)

Route90 square/commutator layer packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniElementaryLayerData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniElementaryLayerData K)

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniExponentData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniExponentData K)

Concrete exponent-two packet from the Route90 elementary layer.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Concrete Frattini packet assembled through the Route90 Section 7 packets.

Route84 literal raw tower from Route43 literal pieces

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.rawLiteralObjectActionTowerData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRoute84Closers.RawLiteralObjectActionTowerData K F)

Route90 replacement for Route84's coherent literal raw tower packet.

This selects the literal Section 7 objects R = Phi(K), M = K/Phi(K), T = (K cap S)/Phi(K), and C = Y/K, together with the transported actions and T-stability, from the Route43 proof-step packets.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.rawObjectActionBridgeData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData K F)

Route78-shaped raw object/action/bridge packet from the Route90 literal raw tower.

Simple-head packet without the ActualProofs2 axiom

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

Route90 reassembly of the ActualProofs2 invariant packet.

This proves the old packet surface without using minimalBlock_invariantActualProofs2Data. Compared with the generic minimalBlock_invariantActualProofs2Data_proven, the nontrivial action witness is supplied directly by the Route43 witness, so this theorem does not reselect a separate minimalBlock_headNontrivialData packet for an arbitrary raw tower.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.rawInvariantHyperplanesContainTData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

Route90 direct hyperplane form from the same-raw-tower actual packet reassembled above.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.rawHeadNonzeroStableEqTopData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadNonzeroStableEqTopData D)

Route90 nonzero-stable quotient-head criterion from the reassembled actual packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.rawHeadActionNotPointwiseTrivialData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

Route90 not-pointwise-trivial head action from the reassembled actual witness.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.rawLowerInvariantCharacterExistsData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Route90 existential lower-character field from the actual character hitting 1.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.rawSimpleHeadSemanticData_from_route90 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route90 same-tower simple-head semantic packet.

The four fields are projected from invariantActualProofs2Data_from_route90, so this theorem does not call the old minimalBlock_invariantActualProofs2Data axiom.

Route55-shaped provider

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.kernelRoute55Data_from_route90 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute55.KernelRoute55Data chief)

Route55-shaped packet using Route90 least/Frattini, raw tower, and simple-head replacements.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.kernelRoute54Data_from_route90 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute54.KernelRoute54Data chief)

Route54 coherent data supplied through Route90.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.consumedData_from_route90 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute53.ConsumedData chief)

Route53 consumed data supplied through Route90.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.groupInvariantRouteData_from_route90 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route90.

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

Group-tower provider using Route90 kernel/minimal-block lowering.

Public provider

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

Drop-in kernel provider replacing minimalBlock_groupTowerData_from_kernelRoute85Closers.