ForcedUnsplitPartialRelation
plain-language theorem explainer
Names the PDE coefficient identity forced by unsplit advection on nearest-neighbor local momentum profiles: for every real triple (d,p,r), (p+r) times the profile equals p²+d². Gravity workers citing the HKT point-split repair use it as the exact obstruction predicate. It is a pure Prop abbreviation; unsatisfiability is proved one line later by a concrete counter-evaluation.
Claim. For a local momentum profile $f:\mathbb{R}^3\to\mathbb{R}$ (arguments $d,\pi_j,\pi_{j+1}$), the forced unsplit partial relation asserts $\forall\, d,p,r\in\mathbb{R},\ (p+r)\,f(d,p,r)=p^2+d^2$.
background
This module repairs the HKT dynamic target after the unsplit mom_ham field was shown uninhabitable. The widened Dyn target kept an unsplit momentum-Hamiltonian coupling; against a frozen quadratic Hamiltonian at $n=2$, unsplit advection forces a singular coefficient identity on nearest-neighbor profiles.
A LocalMomProfile is a real ternary map $f(d_j,\pi_j,\pi_{j+1})$ with $d_j=q_{j+1}-q_j$, translation-covariant by construction. Unsplit advection of such a profile against the quadratic Hamiltonian density produces the algebraic demand that $(p+r)$ times the profile equal $p^2+d^2$ at every real triple.
The module scope is deliberately narrow (Codex D-qg-hkt-pointsplit adjudication): no rigidity theorem, no ledger flag. The load-bearing repaired class is the strong point-split target; this predicate records the unsplit obstruction that motivated the split.
proof idea
Definitional, not a proof. The body is the universal quantification $\forall d,p,r,\ (p+r)\cdot f(d,p,r)=p^2+d^2$ over a LocalMomProfile. No tactics, no lemmas. Downstream, forced_unsplit_partial_relation_impossible discharges unsatisfiability by instantiating at $(1,1,-1)$ and norm_num.
why it matters
Records the exact algebraic obstruction that kills unsplit HKT momentum-Hamiltonian coupling for honest nearest-neighbor profiles. Parent theorem forced_unsplit_partial_relation_impossible proves the Prop empty: at $(d,p,r)=(1,1,-1)$ the left side vanishes while the right side is $2$. A second consumer, unsplit_RHS_delta0_unsplitNoGo, works in the same unsplit no-go cluster on $\mathrm{ZMod},2$.
In the SevenGaps gravity stack this is the Wave C2 R5 repair witness: the unsplit Dyn target stays as a falsification-adjacent record, while the repaired sibling uses smeared point-split momentum densities. It does not touch the forcing chain T0-T8, RCL, or the phi-ladder mass formula; it is local to the HKT discrete-gravity bracket analysis. The analogous claim against campaign HamDyn remains the open Prop UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.