Integrated Route143 all current lowerings

This non-public attack route combines the current successful Route141/142 sidecars:

• Section 8 candidate/target lowering from Route141Section8Closers;
• Section 7 least/Frattini lowering from Section7KernelRoute141FrattiniClosers;
• Section 7 raw/action/invariant lowering from Section7KernelRoute141RawClosers;
• Section 7 pushout semantic lowering from Section7PushoutRoute141SemanticClosers.

The public presentation_correct route remains Route130. This file is an audit frontier: it shows the smallest current non-local leaf set exposed by the sidecars that actually compile in this workspace.

Combined Section 7 kernel provider

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

Route143 kernel provenance: use the Frattini sidecar for the selected least kernel and R = Phi(K) package, then use the raw sidecar for the literal raw-module/action tower over that same K,F.

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

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

Integrated Route143

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated143 (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_currentIntegrated143 (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_currentIntegrated143 (p : FramedPair) : framedCountA p = framedCountQ p

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