LocalHamProfile
plain-language theorem explainer
Names the type of a three-argument real function used as a local Hamiltonian density profile on two neighboring cells. Gravity and HKT rigidity arguments cite it whenever ham density is written pointwise as a function of (q_j, q_{j+1}, π_j). It is a pure type abbreviation with no proof content.
Claim. A local Hamiltonian profile is a map $h:\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, i.e. a real-valued function of three real arguments (neighboring configuration values and one momentum).
background
This module sets up Wave C2 groundwork for the local-profile functional equation at $n=2$ (mirroring HamDyn). The goal is to reduce the dynamical ham–ham identity for local profiles to a factored form $\mathrm{momDensity}_j = h_b(j), h_p(j+1)$. Nothing in the module itself proves rigidity; it only supplies the attack surface for R6.
A local profile packages the Hamiltonian density on a two-site cell as a single function of the two neighboring configuration coordinates and the momentum at the first site. Downstream, the smeared density on phase space is recovered by evaluating that profile at $(q_j,q_{j+1},\pi_j)$. Smoothness data (partials $h_a,h_b,h_p$) live in a companion structure, not in this type.
proof idea
No proof: the declaration is a one-line type abbreviation equating the name to the function type $\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$.
why it matters
This type is the carrier for every local-profile statement in the HKT canonical-momentum rigidity development. Downstream theorems quantify over $h:\mathrm{LocalHamProfile}$ when specializing the alternating functional equation at $p=0$ or $r=0$, when equating smeared ham density to the profile evaluation on a two-cell phase-space chart, and when running the linear-$h_p$ / momentum-independent-$h_b$ ansatz that forces the gradient couplings $h_b(a,b)\cdot\mathrm{kinCoeff}(b,a)=c_{\mathrm{Mom}}(b-a)g(a)$.
It sits in the SevenGaps gravity stack: local profiles are the concrete ansatz class against which the dynamical ham–ham identity is tested before any claim that momentum density factors. The module doc is explicit that R6 rigidity is still open; this abbreviation only names the objects those later arguments manipulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.