Integrated Route174 candidate plus target plus kernel lowering route #
Route158 keeps Route152's verified kernel and pushout route:
- kernel Section 7 via
Section7KernelRoute151Closers; - pushout/determinant Section 7 via
Section7PushoutRoute151Closers;
and surgically swaps the candidate lift-partition provider inside the central-cover realization from Route147 pointwise to Route130's coherent semantic exact-image split.
This is an attack route, not a public promotion. The expected effect is to
replace the two broad candidate packet leaves
centralCover_candidateObstructionMapData and
centralCover_candidateFrattiniExactImageCardinalityData by Route130's two
semantic residuals
centralCover_candidateMiddleExactImageObstructionEvaluationData_residual and
centralCover_candidateTopExactImageAffineFiberEquivData_residual.
theorem
Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated174CandidateTargetKernelRoute172
{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_currentIntegrated174CandidateTargetKernelRoute172
(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_currentIntegrated174CandidateTargetKernelRoute172
(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_currentIntegrated174CandidateTargetKernelRoute172
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: