Integrated current route, second refinement

This sidecar keeps IntegratedCurrentRouteProofs.lean stable and combines two post-checkpoint refinements whose source files intentionally import the current route:

• CandidateScalarFrattiniActualClosers replaces the five candidate scalar-pushout / Frattini-coordinate packets by lower §8 packets.
• MinimalBlockSimpleHeadScalarClosers replaces the four simple-head/scalar packets by smaller manuscript-shaped semantic packets.
• MinimalBlockExtraspecialClosers3 replaces the five extraspecial determinant packets by one coherent actual central-pushout/extraspecial construction packet.

The theorem names below mirror the final-count route, so the capstone can point at this strictly refined route without creating an import cycle.

Candidate route through current semantic split packets

theorem Q2Presentation.Induction.centralCover_candidateDirectExactImageResidualData_from_currentSplitClosers2 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateDirectExactImageResidualData B T)

Direct candidate exact-image data from Jason's current semantic split, avoiding the two current candidate residual packet axioms in the route.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_currentSplitClosers2 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Candidate lift-partition data through the current semantic split.

Target route through the same-tower lower K/R split

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

Decoration-kernel closure through Lorentz's same-tower lower K/R split, avoiding the four previous target lower packet axioms in the final route.

Group tower through both kernel-module and simple-head splits

theorem Q2Presentation.Induction.minimalBlock_provenanceConcreteFinalPieces_from_kernelAndSimpleClosers2 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance pieces using Turing's kernel-module split and Maxwell's simple-head/scalar split simultaneously.

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

Cover realization through same-tower target split

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated2 {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 using the same current route as centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated, but with target decoration/framed quotient data routed through the same-tower lower K/R split.

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

Nonterminal Fourier branch through the current route, Maxwell's narrowed simple-head/scalar split, and Hubble's coherent extraspecial determinant split.

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

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated2 (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 after the simple-head/scalar and extraspecial determinant refinements.