UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn
plain-language theorem explainer
Open target Prop: no Fréchet-smooth nearest-neighbor local momentum profile satisfies unsplit momentum–Hamiltonian advection against the campaign dynamic density HamDyn. Gravity workers on the HKT point-split repair would cite it once closed. The declaration only names the statement; the frozen-Ham factorization proof does not transport, and no proof is supplied.
Claim. For every local momentum profile $f:\mathbb{R}^3\to\mathbb{R}$ equipped with a Fréchet cell-smoothness package, the unsplit Dyn advection identity fails: it is not the case that for all smearing weights $w$ and lapses $N$ on $\mathbb{Z}/2\mathbb{Z}$ and all phase-space points $x$, $\{M_f[w],\mathrm{HamDyn}[N]\}(x)$ equals $\sum_j w_j(N_{j+1}-N_j)\,h^{\mathrm{dyn}}_j(x)$.
background
This module repairs the Wave C2 R5 point-split HKT dynamic target. The widened Dyn target keeps an unsplit mom_ham field. Against the frozen quadratic Hamiltonian that field is already uninhabitable for honest nearest-neighbor profiles at $n=2$: unsplit advection forces a singular identity on the locus $p_0+p_1=0$.
A local momentum profile is a map $f(d_j,\pi_j,\pi_{j+1})$ with link $d_j=q_{j+1}-q_j$, translation-covariant by construction. LocalMomSmooth packages Fréchet cell derivatives in the distance and the two momentum slots. UnsplitMomHamForProfileDyn is the Dyn-style advection identity: the Poisson bracket of the smeared momentum built from $f$ against HamDyn equals the weighted sum of hamDynDensity cells, not the frozen quadratic density.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the symmetric difference operator is definitionally zero and the older DgenSym sketch of split mom_ham is empty at HamDyn size. The repaired API therefore uses smeared point-split momentum densities already present in the HamDyn brackets.
proof idea
Definition only, not a theorem. The body is the universal statement that every Fréchet-smooth local momentum profile $f$ fails UnsplitMomHamForProfileDyn: no such $f$ satisfies the unsplit bracket identity against HamDyn for all smearings, lapses, and phase-space points. No lemmas are applied; there is no tactic or term proof.
why it matters
Names the HamDyn-level analogue of the proved frozen no-go unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam. The module keeps the unsplit Dyn target as a falsification-adjacent record and routes load-bearing work through HKTPointSplitTargetDynStrong; this Prop is the explicit open obstruction on the unsplit side.
The honest-effort note records why the frozen argument fails to lift: at the frozen witness the LHS factorizes as $(N_0+N_1)\cdot\mathrm{scalar}$ while the RHS is $N_1-N_0$, yielding a two-lapse contradiction, but HamDyn configuration partials break that factorization. Closing this Prop would finish the nearest-neighbor unsplit no-go at dynamic level; until then the doc forbids citing it as a theorem. No rigidity theorem is proved in the module, and no ledger flag is flipped. Downstream bookkeeping (including RHS evaluations such as the delta0 unsplit witness identity) sits in the same point-split repair surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.