forced_unsplit_partial_relation_impossible
plain-language theorem explainer
No local momentum profile can obey the coefficient identity forced by unsplit advection: (p+r) f(d,p,r) = p² + d² for all reals. Gravity workers on the HKT point-split repair cite this no-go when ruling out unsplit mom_ham against the frozen quadratic Hamiltonian. The proof is a one-point counterexample at (d,p,r)=(1,1,-1), where the left side is zero and the right side is two.
Claim. For every real function $f:\mathbb{R}^3\to\mathbb{R}$, the identity $(p+r)\,f(d,p,r)=p^2+d^2$ fails to hold for all $d,p,r\in\mathbb{R}$. In particular it fails at $(d,p,r)=(1,1,-1)$, where the left side vanishes and the right side equals $2$.
background
A local momentum profile is any real map $f(d,p,r)$ used to build nearest-neighbor cell momenta $m_j=f(d_j,\pi_j,\pi_{j+1})$ with link differences $d_j=q_{j+1}-q_j$. Translation covariance is built in by that dependence pattern alone.
Unsplit advection against the frozen quadratic Hamiltonian forces the coefficient identity $(p+r)\partial_d f=p^2+d^2$ on that class (equivalently the multiplicative form written in the forced-relation predicate). The module is the Wave C2 R5 repair of the point-split HKT dynamic target: the widened Dyn target keeps an unsplit mom_ham field that is uninhabitable for honest nearest-neighbor profiles, while the repaired sibling works with smeared point-split momentum densities.
Scope is deliberately narrow (Codex adjudication D-qg-hkt-pointsplit-adjudication-20260722). The analogous claim against campaign HamDyn remains an open Prop; this lemma only kills the forced partial relation on the profile class itself.
proof idea
Assume some profile $f$ satisfies the forced relation for all real triples. Instantiate at the witness $(d,p,r)=(1,1,-1)$. The left side is $(1+(-1)),f(1,1,-1)=0$; the right side is $1^2+1^2=2$. norm_num closes the contradiction. No upstream lemmas are required beyond the definition of the forced-relation predicate.
why it matters
This no-go is the algebraic reason unsplit advection cannot sit on nearest-neighbor local momentum profiles against the frozen quadratic Hamiltonian. It underwrites the point-split repair path in this module and is consumed by the (demoted, weak-schema) rigidity statement HKTRigidityStatementPointSplitDynN2, whose doc notes that binding rigidity lives on the Strong class instead.
In the broader SevenGaps gravity stack it records why the unsplit Dyn target is kept only as a falsification-adjacent witness, while load-bearing work moves to smeared source/target advection densities. It does not flip any ledger flag and does not close the open HamDyn analogue. Framework contact is local to the HKT dynamic-structure bracket, not to the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.