Integrated Route144 Section 8 + pushout lowering

Route144 is a non-public attack route built from the verified Route143 frontier. It keeps the Route143 Section 7 kernel provider, but swaps:

• Section 8 candidate realization to the existing Route130 provider;
• Section 8 target realization to the Route144 same-tower provider;
• Section 7 kernel to the Route143 actual Frattini/raw providers;
• Section 7 determinant/pushout to the Route143 actual-pushout provider.

So this route is intended to remove the broad Route143 Section 8 target packet surface and the five Route143 pushout atoms from the integrated audit closure.

Route144 combined kernel provider

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteProvenanceData_currentIntegrated144 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Route144 kernel provenance: combine the actual least/Frattini provider with the actual raw object/action provider over the same selected K,F.

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

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

Route144 central-cover realization

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated144 {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) : Nonempty (CoverRealization (G.toMinimalBlock h Fdet A Rdet))

Route144 cover realization: Route143 kernel/group tower, Route130 candidate/target Section 8 providers, and arbitrary supplied determinant packets.

Integrated Route144

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated144 (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)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated144 (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)

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

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated144 (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)))

Route144 finite-surjection equality with Route143 kernel lowerings, Route130 candidate/target Section 8 lowerings, and Route143 actual pushout lowering.