Integrated current final route

This sidecar wires the newest de-axiomatization sidecars into one final-count route. It combines:

• the candidate exact-image split from CandidateRLiftFrattiniSemanticProofs;
• the target K/R quotient-action split from TargetKmodRActionProofs;
• the same-tower Section 7 provenance packet from MinimalBlockProvenanceSemanticProofs;
• the determinant reduction to one semantic central-pushout family plus one actual simple-head determinant packet.

The goal is only route integration: no new axiom is introduced here.

Target framed packet through the quotient-action route

theorem Q2Presentation.Induction.centralCover_targetFramedMarkedQuotientData_from_kmodRQuotientAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetFramedMarkedQuotientData B D)

Target framed/marked quotient data routed through the concrete Y/K action packet, avoiding the broader centralCover_targetKmodRActionCompatibilityData axiom in the final closure.

Cover realization through all current narrow packets

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

Cover realization for the current route, with the candidate and target pieces both routed through their newest narrowed packets.

Determinant route through two coherent packets

theorem Q2Presentation.Induction.minimalBlock_preheadPushoutRouteLowerData_from_currentIntegrated {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadPushoutRouteLowerData D)

Lower pushout route from one semantic central-pushout family and one actual simple-head determinant packet for that same family.

Final count route

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

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

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

Current strongest integrated finite-surjection equality route.