Integrated Route199 determinant-semantic lowering over Route198 #
This route keeps Route198's candidate, target, Route72 Frattini, and Route43 raw kernel surfaces fixed. Its only change is the determinant/pushout provider:
- remove the seven Route198 determinant-semantic atoms;
- replace them by the Route199 same-family determinant surface from
MinimalBlockPushoutRoute199DeterminantSemanticClosers.
The route is diagnostic/audit-facing. It does not edit Route198, kernel, candidate, or target files.
theorem
Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated199DeterminantSemanticTarget164
(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_currentIntegrated199DeterminantSemanticTarget164
(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_currentIntegrated199DeterminantSemanticTarget164
(G : Type)
[Group G]
[Finite G]
[Nonempty G]
: