Integrated current route, fifty-eighth refinement #
Route58 keeps the Route56/57 candidate and target improvements, and routes the
Section 7 determinant/pushout step through
MinimalBlockPushoutRoute58Proofs.
This is a strict proof-strengthening route: the old split square, diagonal, and
polar pushout packets are replaced by theorem-level data obtained from the
actual phi_lambda packet via the normalized extraspecial square.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated58
(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_currentIntegrated58
(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_currentIntegrated58
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: