Route81 kernel closers for the minimal-block route

Route80/79 exposes the Section 7 kernel frontier through seven Route78 aggregate packets. This sidecar keeps the downstream Route55 consumer shape, but routes the provider through smaller owned packets:

• selected least-kernel data is split into a candidate and the universal leastness proof for that selected candidate;
• selected Frattini/internal data is split into element and nontriviality packets;
• centralizer and fourth-power collapse data are split into core and Hall-image packets;
• the literal exponent-two implication is split into a commutator-generator step plus a generated-layer transfer, with square-generator exponent two closed directly from fourth-power vanishing;
• raw object/action/bridge data is split into its three Route55-consumed components;
• the simple-head semantic packet is split into the four fields of lem:simplehead.

The public provider is a drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute79CombinedClosers.

Least kernel selection

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.leastKernelCandidateData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Route81 least-kernel candidate for the selected Section 7 block.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.leastKernelUniversalData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelCandidateData chief) : Nonempty (MinimalBlockKernelLeastUniversalData K)

Route81 universal leastness for the selected least-kernel candidate.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.leastKernelSelectedData_from_route81 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData chief)

Route78 selected least-kernel packet assembled through Route81's split.

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

Route81 least-over-chief packet.

Frattini nonidentity

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.frattiniInternalElementData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K)

Route81 selected internal Frattini element.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.frattiniInternalElementNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementNontrivialData E)

Route81 nontriviality for the selected internal Frattini element.

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

Route78 selected internal-Frattini packet assembled through Route81.

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

Route67 internal nonidentity packet recovered from Route81 split data.

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

Route81 Frattini nontriviality from the selected internal witness.

Centralizer-collapse step

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.frattiniCentralizerCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K)

Route81 centralizer core for the selected least kernel.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.frattiniCentralizerHallImageData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerHallImageData C)

Route81 Hall-image data for the selected centralizer core.

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

Route78 selected centralizer packet assembled through Route81.

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

Route67 Hall-commutator centralizer packet recovered from Route81.

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

Route81 centralizer step.

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

Concrete centrality packet from the Route81 centralizer step.

Fourth-power step

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.fourthPowerKernelCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K)

Route81 fourth-power kernel core for the selected least kernel.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.fourthPowerKernelHallImageData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelHallImageData P4)

Route81 Hall-image data for the selected fourth-power kernel core.

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

Route78 selected fourth-power packet assembled through Route81.

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

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

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

Route81 fourth-power vanishing.

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

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

Elementary Frattini layer

structure Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.FrattiniCommutatorGeneratorExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Route81 commutator-generator exponent-two step after the collapse inputs.

• commutator_generators_square_eq_one_of_collapse : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K → MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K → ∀ a ∈ K.Ksub, ∀ b ∈ K.Ksub, (a⁻¹ * b⁻¹ * a * b) ^ 2 = 1

structure Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.FrattiniGeneratedLayerExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Route81 transfer from square and commutator generators to the literal Frattini subgroup.

• frattini_square_eq_one_of_generators : (∀ k ∈ K.Ksub, (k ^ 2) ^ 2 = 1) → (∀ a ∈ K.Ksub, ∀ b ∈ K.Ksub, (a⁻¹ * b⁻¹ * a * b) ^ 2 = 1) → ∀ r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), r ^ 2 = 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.frattiniCommutatorGeneratorExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCommutatorGeneratorExponentData K)

Residual Route81 commutator-generator exponent packet.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.frattiniGeneratedLayerExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniGeneratedLayerExponentData K)

Residual Route81 generated-layer transfer for the literal Frattini subgroup.

def Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.squareGeneratorsExponentDataOfFourthPower {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K) (k : p.fst.Y) : k ∈ K.Ksub → (k ^ 2) ^ 2 = 1

Square generators have exponent two directly from fourth-power vanishing.

Equations

• ⋯ = ⋯

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

Route78 literal exponent packet assembled through Route81's generator lowering.

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

Route67 square/commutator layer packet recovered from Route81.

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

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

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

Concrete exponent-two packet from the Route81 elementary layer.

Frattini packet

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

Concrete Frattini packet assembled through Route81 lowerings.

Raw object/action/bridge lowering

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.rawObjectsData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelModuleConcreteRawObjectsData K F)

Route81 raw R, M, T, C objects for the selected tower.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.rawActionsData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawObjectsData K F) : Nonempty (MinimalBlockKernelModuleConcreteRawActionsData O)

Route81 transported actions for the selected raw objects.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.rawBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleConcreteBridgeData D)

Route81 same-tower bridge K/Phi(K) ~= M.

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

Route78 raw object/action/bridge packet assembled through Route81.

Simple-head semantic lowering

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.rawInvariantHyperplanesContainTData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

Route81 invariant-hyperplane field of the simple-head lemma.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.rawHeadNonzeroStableEqTopData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadNonzeroStableEqTopData D)

Route81 nonzero stable submodule field of the simple-head lemma.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.rawHeadActionNotPointwiseTrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

Route81 not-pointwise-trivial head-action field.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.rawLowerInvariantCharacterExistsData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Route81 lower invariant-character existence field.

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

Route44 simple-head semantic packet assembled through Route81's four fields.

Route55-shaped provider

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

Route55-shaped packet using all Route81 kernel lowerings on one selected tower.

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

Route54 coherent data supplied through the Route81 kernel path.

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

Route53 consumed data supplied through Route81.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute81Closers.groupInvariantRouteData_from_route81 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route81.

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

Group-tower provider using Route81 kernel lowerings.

Public provider

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

Drop-in kernel provider using Route81 lowered kernel packets.