UnsplitMomHamForProfile
plain-language theorem explainer
Predicate encoding the unsplit Dyn-style advection identity: a local momentum profile f satisfies it when the Poisson bracket of the smeared momentum built from f against the frozen quadratic Hamiltonian equals a weighted sum of quadratic Hamiltonian densities on PhaseSpace 2. Gravity/HKT workers cite it as the exact Prop negated by the frozen-Ham no-go. Pure definitional Prop; no proof content.
Claim. A local momentum profile $f:\mathbb{R}^3\to\mathbb{R}$ (with $m_j=f(d_j,\pi_j,\pi_{j+1})$ and $d_j=q_{j+1}-q_j$) satisfies the unsplit momentum-Hamiltonian identity when, for every weight $w$ and lapse $N$ on $\mathbb{Z}/2\mathbb{Z}$ and every phase-space point $x$, $\{M_f[w], H[N]\}(x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w(j)\,(N(j+1)-N(j))\,\mathcal{H}_{\mathrm{quad}}(x)_j$.
background
This module repairs the widened Hojman-Kuchař-Teitelboim dynamic target after the unsplit mom_ham field was shown uninhabitable for honest nearest-neighbor local momenta against the frozen quadratic Hamiltonian. Scope is deliberately narrow (n=2, frozen Ham); the analogous claim against campaign HamDyn remains open.
A local momentum profile is a function $f:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ giving $m_j=f(d_j,\pi_j,\pi_{j+1})$ with link differences $d_j=q_{j+1}-q_j$, translation-covariant by construction. Momentum is smeared against a weight $w$ on $\mathbb{Z}/2\mathbb{Z}$; the frozen Hamiltonian is smeared against a lapse $N$. The quadratic Hamiltonian density is the local density appearing in the frozen Ham sector.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the older $D_{\mathrm{gen}}^{\mathrm{sym}}$ sketch is definitionally empty; the repaired API uses smeared point-split densities instead. No rigidity theorem is proved in this module.
proof idea
Definitional Prop, not a proved statement. The body is the universal quantification over weights $w$, lapses $N$, and phase-space points $x$ of the equality between the Poisson bracket of MomFromProfile f w with Ham N and the two-site weighted sum of quadraticHamDensity. Downstream no-go theorems assume this Prop and derive a contradiction for Fréchet-smooth nearest-neighbor profiles.
why it matters
This is the exact predicate negated by the scoped no-go unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam (and its compatibility alias unsplit_mom_ham_no_smooth_local_witness), which discharge ledger claim C-qg-hkt-unsplit-nogo: no Fréchet-smooth nearest-neighbor local momentum profile satisfies unsplit Dyn advection against the frozen quadratic Hamiltonian on PhaseSpace 2.
It records the unsplit Dyn-style mom_ham identity that the widened HKT dynamic target kept and that the point-split repair replaces. The module header is explicit that the unsplit Dyn target remains only as a falsification-adjacent record; the load-bearing class after adjudication is the strong point-split target. The open sibling is the same no-go shape against campaign HamDyn. No T0-T8 forcing step is closed here; this is gravity-side HKT structure, not foundation forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.