LocalMomProfile
plain-language theorem explainer
Type synonym for nearest-neighbor local momentum density profiles on the two-site lattice: real maps of bond separation and the two adjacent momenta. Anyone working the point-split HKT repair cites it as the ambient class for translation-covariant momentum cells. Pure definitional abbreviation; no proof content.
Claim. A local momentum profile is a map $f:\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, read as $m_j=f(d_j,\pi_j,\pi_{j+1})$ with bond separation $d_j=q_{j+1}-q_j$. The class is translation-covariant by construction.
background
The module repairs the widened Hojman–Kuchař–Teitelboim dynamic target after the unsplit momentum–Hamiltonian sector proved uninhabitable for honest nearest-neighbor profiles against a frozen quadratic Hamiltonian. On $n=2$ the unsplit advection identity forces a singular PDE on the zero-total-momentum locus; the repaired sibling therefore works with smeared point-split momentum densities and source/target advection densities.
A local momentum profile packages one cell of that density: the value at site $j$ depends only on the bond $d_j=q_{j+1}-q_j$ and the two adjacent momenta $\pi_j,\pi_{j+1}$. The type is simply the space of all such three-argument real functions. Smoothness, Fréchet derivatives, and Poisson brackets are layered on later via companion structures (local cell derivative, profile-to-momentum map, smoothness witness).
proof idea
Definitional abbreviation only: LocalMomProfile is definitionally identical to $\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$. No tactics, no lemmas.
why it matters
This is the ambient function class for the entire point-split HKT repair. Downstream it appears in the forced unsplit partial relation $(p+r)\partial_d f=p^2+d^2$ and its impossibility theorem (witness $(d,p,r)=(1,1,-1)$), in the Fréchet derivative of a local momentum cell and of the smeared momentum functional, and in the no-go bracket identity at the $\delta_0$ witness. The module records that the unsplit Dyn target stays as a falsification-adjacent artifact; the load-bearing repaired class is the strong point-split target. No rigidity theorem and no ledger flag are claimed here; the type merely names the profiles those arguments quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.