Integrated Route197: Route196 with the Section 7 kernel/raw frontier lowered #
This route keeps Route196's candidate, pushout, and target surfaces fixed. The only route change is the Section 7 kernel provider:
- the five Route67 Lemma 7.2 Frattini leaves are replaced by Route72 lower packets;
- the two Route167 raw quotient/simple-head leaves are replaced by Route180/Route43 raw object, action, and simple-head packets.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated197KernelRawRoute72Route180Target164
(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_currentIntegrated197KernelRawRoute72Route180Target164
(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)