LocalHamSmooth
plain-language theorem explainer
Packages Fréchet smoothness data for a local Hamiltonian profile on the two-site phase space: three coefficient profiles that realize the derivative of each cell map. Gravity workers cite it when unpacking the n=2 alternating ham_ham functional equation and the C2 rigidity obligations (hp linear in momentum, hb momentum-independent). Pure structure definition; no proof content.
Claim. A local Hamiltonian profile $h:\mathbb{R}^3\to\mathbb{R}$ is cell-smooth when there exist coefficient profiles $h_a,h_b,h_p:\mathbb{R}^3\to\mathbb{R}$ such that for every site $j\in\mathbb{Z}/2\mathbb{Z}$ and phase-space point $x=(q,\pi)$, the map $y\mapsto h(q_j(y),q_{j+1}(y),\pi_j(y))$ is Fr\'echet differentiable at $x$ with derivative $h_a\,dq_j+h_b\,dq_{j+1}+h_p\,d\pi_j$, coefficients evaluated on the cell $(q_j,q_{j+1},\pi_j)$ of $x$.
background
The module is Wave C2 groundwork for the local-profile functional equation at lattice size $n=2$. A local Hamiltonian profile is simply a real function of three scalars (two neighboring configuration values and one momentum). The ambient phase space is the product of configuration and conjugate-momentum fields on the periodic two-site lattice.
Configuration and momentum coordinates appear as continuous linear functionals coordQ and coordP on that phase space. The cell map at site $j$ reads off $h(q_j,q_{j+1},\pi_j)$ from a phase-space point; cell-smoothness asserts that this composite is Fréchet differentiable, with derivative spanned by those three coordinate functionals and with coefficient functions that are themselves profiles of the same type.
The module reduces the dynamical ham_ham bracket for local profiles to a momentum-density identity of the form $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$. Nothing in this file yet proves rigidity of the profiles.
proof idea
Structure definition only: four fields, no proof body. The three coefficient profiles and the universal quantifier over sites and phase-space points are the data of cell-wise Fréchet differentiability; Mathlib's HasFDerivAt is the sole analytic primitive. Downstream lemmas construct or unpack instances rather than prove the structure itself.
why it matters
This is the smoothness carrier for the entire C2/R6 attack on local Hamiltonian rigidity at $n=2$. Downstream, profiled_ham_ham_alternating_FE exists a profile together with a cell-smooth witness and extracts the alternating functional equation forced by CanonicalMom ham_ham; specializations fe_at_p_zero and fe_at_r_zero freeze one momentum argument. The coefficient fields feed the C2 obligations HpLinearInP (hp linear in its momentum slot) and HbPIndependent (hb independent of momentum), which Session C2 must force by differentiating the FE after a ContDiff strengthening. Also used by the quadratic ADM gauge analysis and by the explicit ham_ham coefficient alternating sum on the two-site cell. It does not itself close rigidity; it is the interface on which rigidity is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.