Integrated Route145 all-lowered attack route

Route145 composes the four verified Route145 sidecars over the green Route144 route:

• candidate Section 8 via CandidateRoute145Closers;
• target Section 8 via TargetKmodRRoute145SameTowerClosers;
• kernel/raw Section 7 via Section7KernelRoute145ActualClosers;
• pushout/determinant Section 7 via Section7PushoutRoute145ActualClosers.

This is an attack route, not a public promotion. It intentionally lowers broad Route144 packets into more manuscript-shaped atoms, so the visible axiom count can rise while the semantic content becomes more concrete.

Route145 combined kernel provider

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

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

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

Route145 central-cover realization

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated145AllLowered {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))

Route145 cover realization: Route145 target/candidate Section 8 providers, Route145 Section 7 kernel provider, and supplied determinant packets.

Integrated Route145

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

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

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

Route145 finite-surjection equality with all four Route145 lowerings composed over the Route144 attack route.