Integrated current route, one-hundred-twenty-fourth refinement #
Route124 keeps the Route123 candidate exact-image lowering and compact kernel improvement, then adds two public frontier reductions:
- target: Route46 same-tower pair -> one Route52 coherent literal-action leaf;
- pushout: two broad determinant leaves -> one coherent central-extension leaf.
The candidate remains routed through exact-image final residuals: middle obstruction evaluation + top affine-fibre equivalence.
- compact Route120 kernel closer, removing the theorem-level upper-candidate least-kernel leaf.
This is a work route, not the promoted public route.
theorem
Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated124
{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_currentIntegrated124
(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_currentIntegrated124
(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_currentIntegrated124
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: