Integrated Route194 kernel lowering over Route192 #
This replay keeps Route192's candidate actual split, target Route28 literal quotient/action, and compact determinant/pushout provider. It swaps only the Section 7 kernel provider:
- Route192's five Route78 selected least/Frattini leaves are replaced by the
five Route67 Lemma 7.2 packets exposed through
Section7KernelRoute194Closers; - Route192's two Route167 raw quotient/simple-head leaves are retained.
theorem
Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated194KernelRoute192
{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))
Route192 realization replayed under the Route194 kernel route. The realization argument consumes already supplied kernel and determinant packets, so the kernel provider is swapped only in the nonterminal branch below.
theorem
Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated194KernelRoute192
(p : FramedPair)
:
¬ScalarTerminal p → Nonempty (FourierBranchData p)
Route192 nonterminal branch with only the Section 7 kernel provider routed through Route194.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated194KernelRoute192
(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_currentIntegrated194KernelRoute192
(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_currentIntegrated194KernelRoute192
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
:
Route192 finite-surjection equality replayed with only the Section 7 kernel provider lowered through Route194.