Integrated current route, sixtieth refinement #
Route60 keeps the Route59 candidate and target Section 8 refinements, and swaps the Section 7 determinant/pushout provider from Route58 to the lower-level Route60 scalar-pushout packet.
The Route59 realization theorem is already parameterized by the determinant
family data, so this file only changes where that determinant family comes from:
minimalBlock_preheadDeterminantPackets_from_route60.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated60
(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_currentIntegrated60
(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_currentIntegrated60
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: