Integrated current route, fifty-second refinement #
Route52 keeps the validated Route51 target and pushout paths, but accepts two new sidecar refinements:
- candidate Section 8:
centralCover_candidateObstructionMapDataandcentralCover_candidateFrattiniExactImageCardinalityDataare replaced by the coordinate-level Route52 packets; - target Section 8: the two Route37 literal target leaves are replaced by one coherent literal quotient/action packet;
- kernel/raw Section 7: the four Route51 kernel/raw packets are replaced by the two coherent Route52 actual-kernel/invariant packets.
- pushout/determinant Section 7: the Route50 simple-head determinant packet is replaced by the semantic central-pushout family plus the same-family determinant conclusions.
This file is an integration-only route. It does not prove new leaf packets; it routes the final count theorem through the already-verified Route52 sidecars.
theorem
Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated52
{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))
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated52
(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_currentIntegrated52
(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.finite_surjection_counts_equal_currentIntegrated52
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: