Integrated current route, one-hundred-thirty-eighth all-sidecars lowering #
This non-public attack route composes all Route135 sidecars that have landed:
- Section 8 candidate/target lowering from
CandidateTargetRoute135Closers; - Section 7 kernel lowering from
Section7KernelRoute135Closers; - Section 7 pushout/determinant lowering from
Section7PushoutRoute135Closers.
It is intended as the current concrete implementation frontier. The public presentation theorem remains on compact Route130 until a route is worth promoting.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated138AllSidecarsLowered
(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_currentIntegrated138AllSidecarsLowered
(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_currentIntegrated138AllSidecarsLowered
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: