Integrated current route, one-hundred-twelfth refinement #
Route112 is Route110 with only the kernel raw-head provider swapped:
- candidate exact-image final closer from Route110;
- target Route106/Route28 lowering from Route110;
- kernel Route110 raw-head closer (four Route43 head leaves lowered to one coherent actual simple-head packet);
- pushout Route106 actual scalar-pushout/simple-head determinant split.
This is a work route, not the promoted public route.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated112
(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_currentIntegrated112
(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_currentIntegrated112
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: