Integrated Route197: Route196 with pushout/determinant semantic lowering #
This route keeps the current Route196 candidate, target, and kernel lowerings, but swaps the Section 7/6 determinant provider.
Compared with Route196, the two pushout/determinant atoms
minimalBlock_preheadActualScalarCentralPushoutData;minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData
are replaced by the lower determinant-semantic surface exported by
MinimalBlockPushoutRoute197DeterminantLowerClosers.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated197CandidateKernelPushoutDeterminantTarget164
(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_currentIntegrated197CandidateKernelPushoutDeterminantTarget164
(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)