Route124 kernel closers

This sidecar leaves IntegratedCurrentRouteProofs124 untouched. It supplies a drop-in kernel provider with the same downstream shape as minimalBlock_groupTowerData_from_kernelCompactRoute120Closers.

Route124 currently keeps the compact Route120 kernel surface:

• minimalBlock_kernelLeastUniversalData;
• minimalBlock_kernelFrattiniCollapseFullData;
• minimalBlock_kernelRawQuotientTowerData;
• minimalBlock_invariantActualProofs2Data.

The theorem below replaces the first three lower-tower atoms by the existing coherent lower group/module packet

• minimalBlock_lowerGroupModuleData,

which ties the selected least kernel, Frattini subgroup, raw module/action tower, K/R bridge, and nonzero head to one Section 7 tower. The invariant packet is kept compact rather than split, since the available decompositions increase the visible closure.

Coherent lower tower plus compact invariant packet

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

Route124 lower group/module data through the existing coherent Section 7 lower packet.

This is the public-route candidate replacement for the compact Route120 trio: least-universal, Frattini-collapse, and raw-quotient tower.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute124Closers.invariantActualProofs2Data_from_route124ClosersLower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Route124 keeps the compact same-raw-tower invariant packet on the selected lower tower.

The finer Route122 invariant split is retained as an attack route, not used here, because its visible closure is larger than the compact invariant leaf.

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

Route124 kernel provider with the same consumer shape as minimalBlock_groupTowerData_from_kernelCompactRoute120Closers.

Axiom-closure effect relative to the Route120 compact provider:

• removes minimalBlock_kernelLeastUniversalData;
• removes minimalBlock_kernelFrattiniCollapseFullData;
• removes minimalBlock_kernelRawQuotientTowerData;
• adds the coherent lower-tower packet minimalBlock_lowerGroupModuleData;
• keeps minimalBlock_invariantActualProofs2Data.

Public route-ready aliases

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

Public lower-tower provider for the Route124 kernel closer.

theorem Q2Presentation.Induction.minimalBlock_invariantActualProofs2Data_from_kernelRoute124Closers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Public same-selected-lower invariant provider for the Route124 kernel closer.

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

Public drop-in kernel provider matching minimalBlock_groupTowerData_from_kernelCompactRoute120Closers.

Route124 audit branch with only the kernel provider swapped

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated124_kernelRoute124Closers (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Route124 nonterminal branch with the kernel provider swapped to this sidecar. This is for audit/public-route readiness; IntegratedCurrentRouteProofs124 itself is unchanged.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated124_kernelRoute124Closers (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursive branch for the Route124 audit path with the kernel provider swapped.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated124_kernelRoute124Closers (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursion step for the Route124 audit path with the kernel provider swapped.

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_currentIntegrated124_kernelRoute124Closers (p : FramedPair) : framedCountA p = framedCountQ p

Framed-count equality for the Route124 audit path with the kernel provider swapped.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated124_kernelRoute124Closers (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Finite-surjection equality for the Route124 audit path with the kernel provider swapped.