momFromProfile
plain-language theorem explainer
Evaluates a local nearest-neighbor momentum density at one lattice site from a profile on the two-site phase space. Gravity workers assembling the point-split HKT momentum sector cite it as the cell-level density before smearing against a weight. The body simply feeds the link difference and the two adjacent momenta into the profile.
Claim. Given a local momentum profile $f:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ and a phase-space point $(q,\pi)$ on the two-site periodic lattice $\mathbb{Z}/2\mathbb{Z}$, the momentum density at site $j$ is $f(q_{j+1}-q_j,\,\pi_j,\,\pi_{j+1})$.
background
The ambient setting is the Wave C2 R5 repair of the Hojman–Kuchař–Teitelboim dynamic target. The unsplit mom_ham field on the widened Dyn target is uninhabitable for honest nearest-neighbor local momentum profiles against the frozen quadratic Hamiltonian at $n=2$; this module supplies the point-split sibling.
A local momentum profile is a pure function $f(d_j,\pi_j,\pi_{j+1})$ of the link difference $d_j=q_{j+1}-q_j$ and the two adjacent conjugate momenta. Translation covariance is built in by using only differences of configuration coordinates. The canonical phase space is the product of configuration and momentum maps on the periodic lattice: $(q,\pi):(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})$, specialized here to $n=2$.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the symmetric generator is definitionally empty; the repaired API therefore works with smeared point-split momentum densities already present in the HamDyn brackets, with source/target advection densities.
proof idea
One-line definitional unpacking. Write $x=(q,\pi)$. The value at site $j$ is the profile applied to the three scalars $q_{j+1}-q_j$, $\pi_j$, and $\pi_{j+1}$. No lemmas are invoked; the body is pure application of $f$.
why it matters
Cell-level density for the repaired point-split HKT momentum sector. Downstream, MomFromProfile smears it against a weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ by $\sum_j w_j\cdot m_j$, and hasFDerivAt_MomFromProfile lifts cellwise Fréchet derivatives of smooth profiles to the smeared functional. That differentiability is the load-bearing input for the strong point-split Dyn class after the unsplit target was left as a falsification-adjacent record.
No rigidity theorem is proved in this module, and no ledger flag is flipped. The construction sits inside the SevenGaps gravity campaign: honest nearest-neighbor momentum against frozen quadratic Hamiltonians, with the open unsplit claim against HamDyn recorded separately. Framework landmarks T0–T8 are not touched here; this is pure classical lattice phase-space bookkeeping for the HKT deformation algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.