UnsplitMomHamForProfileDyn
plain-language theorem explainer
Defines the unsplit advection identity for a local nearest-neighbor momentum profile against the campaign dynamic Hamiltonian density (not the frozen quadratic). Gravity workers on the HKT point-split Dyn target cite it as the predicate that a profile either satisfies or fails. It is a pure Prop packaging: no proof content, only the equality of the Poisson bracket to the smeared density sum.
Claim. For a local momentum profile $f$ (with $m_j = f(d_j,\pi_j,\pi_{j+1})$ and $d_j = q_{j+1}-q_j$), the unsplit Dyn advection property holds when, for every weight $w$ and lapse $N$ on $\mathbb{Z}/2\mathbb{Z}$ and every phase-space point $x$, $\{M_f[w], H_{\mathrm{Dyn}}[N]\}(x) = \sum_{j\in\mathbb{Z}/2\mathbb{Z}} w_j(N_{j+1}-N_j)\,h^{\mathrm{Dyn}}_j(x)$.
background
In the HKT (Hojman–Kuchař–Teitelboim) campaign the momentum–Hamiltonian bracket encodes spatial diffeomorphism advection of the Hamiltonian density. The module repairs the widened Dyn target after adjudication that the unsplit mom_ham field is uninhabitable for honest nearest-neighbor profiles against the frozen quadratic Hamiltonian at $n=2$: unsplit advection forces a singular relation on the locus $p_0+p_1=0$.
A local momentum profile is a map $f:\mathbb{R}^3\to\mathbb{R}$ giving cell momenta $m_j=f(d_j,\pi_j,\pi_{j+1})$ with link differences $d_j=q_{j+1}-q_j$, translation-covariant by construction. MomFromProfile smears that profile against a weight $w$; HamDyn is the campaign dynamic Hamiltonian (with density hamDynDensity), distinct from the frozen quadratic used in the earlier no-go.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the symmetric generator sector is definitionally empty; the structure therefore works with smeared point-split momentum densities already present in the Dyn–Dyn and Ham–Ham brackets.
proof idea
Definition only: the body is the universal quantification of the unsplit bracket identity. No tactics, no lemmas applied. The right-hand side is the discrete advection form $\sum_j w_j(N_{j+1}-N_j)$ times the Dyn density; the left-hand side is the Poisson bracket of the profile-smeared momentum against HamDyn. Downstream open targets negate this Prop under a Fréchet-smoothness hypothesis on $f$.
why it matters
This Prop is the load-bearing predicate for the open Dyn-level no-go UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn, which asserts that no Fréchet-smooth nearest-neighbor profile satisfies the identity. That open target is the HamDyn analogue of the proved frozen no-go unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam.
It sits inside the Wave C2 R5 point-split HKT repair: the unsplit Dyn target remains as a falsification-adjacent record while the load-bearing class is the strong point-split target. The frozen proof's two-lapse factorization (LHS $\propto(N_0+N_1)$, RHS $\propto N_1-N_0$) does not transport because configuration partials of HamDyn break that factorization; packaging the identity cleanly isolates what still needs a new witness argument. No rigidity theorem and no ledger flag are claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.