Integrated current route, thirteenth refinement #
Route13 keeps route12's candidate, target, and actual central-pushout refinements, and integrates the completed kernel/Frattini sidecar. The group tower is assembled from:
- the coherent route10 kernel/Frattini lower tower;
- the route10 head/invariant sidecar already used by route12.
theorem
Q2Presentation.Induction.minimalBlock_groupTowerData_from_route13KernelHeadProofs
{p : FramedPair}
(chief : NonScalarChiefFactor p)
:
Nonempty (MinimalBlockGroupTowerData p chief)
Group tower with both the route10 kernel/Frattini refinement and the route10 head/invariant refinement active.
theorem
Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated13
(p : FramedPair)
:
¬ScalarTerminal p → Nonempty (FourierBranchData p)
Route13 nonterminal branch.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated13
(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_currentIntegrated13
(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_currentIntegrated13
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
:
Route13 finite-surjection equality.