Integrated Route198: Route196 with both Section 7 lowerings #
This route keeps Route196's candidate and target surfaces fixed, and combines the two disjoint Route197 lowerings:
- kernel/raw: Route67/Route167 packets are lowered to Route72 and Route43 manuscript atoms;
- determinant/pushout: the two compact pushout packets are lowered to the seven determinant-semantic atoms.
The visible non-local count increases, but all Route196 Section 7 aggregate leaves are absent from this theorem closure.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated198KernelPushoutLowerTarget164
(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_currentIntegrated198KernelPushoutLowerTarget164
(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_currentIntegrated198KernelPushoutLowerTarget164
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: