differentiable_LocalHamFromProfile
plain-language theorem explainer
Any local Hamiltonian built by summing a smooth two-site profile against weights N on the n=2 phase space is Fréchet differentiable as a real function of phase space. Gravity and ILG workers cite it when they need calculus on discrete Hamiltonian densities before rigidity or kinetic-normalization arguments. The proof is a one-line pointwise lift from the already-established Fréchet derivative at each point.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian profile that is smooth in the sense that each two-site cell map admits a Fréchet derivative with continuous coefficient profiles. For any weight function $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the summed local Hamiltonian $x\mapsto\sum_{j\in\mathbb{Z}/2\mathbb{Z}} N(j)\,h(q_j,q_{j+1},p_j)$ on the $n=2$ phase space is differentiable over $\mathbb{R}$.
background
The module supplies Wave C2 groundwork for the local-profile functional equation at $n=2$ (mirroring HamDyn). It reduces the dynamical Hamiltonian identity for local profiles to a momentum-density factorization; R6 rigidity is not yet proved here.
A local Hamiltonian profile is simply a map $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$. From it one builds the weighted sum $\mathrm{LocalHamFromProfile},h,N$ on the two-site phase space by summing $N(j),h(q_j,q_{j+1},p_j)$ over $j\in\mathbb{Z}/2\mathbb{Z}$. Smoothness of $h$ is packaged as a structure supplying three coefficient profiles and a cellwise Fréchet derivative identity: each cell map is differentiable with derivative a linear combination of the coordinate functionals in the $q_j$, $q_{j+1}$, and $p_j$ directions.
The immediate upstream lemma establishes that this summed map has an explicit Fréchet derivative at every phase-space point (by summing the cell derivatives after constant multiplication by $N(j)$).
proof idea
One-line term proof. At each phase-space point $x$, invoke the upstream lemma that supplies $\mathrm{HasFDerivAt}$ of the local Hamiltonian at $x$, then apply the standard Mathlib conversion from $\mathrm{HasFDerivAt}$ to $\mathrm{DifferentiableAt}$. The resulting pointwise differentiability is exactly the definition of $\mathrm{Differentiable},\mathbb{R}$.
why it matters
This is the calculus gate for the kinetic-normalized vacuum Hamiltonian on the same $n=2$ lattice. Downstream, $\mathrm{differentiable_vacuumKineticHam}$ rewrites the vacuum kinetic density as an instance of $\mathrm{LocalHamFromProfile}$ and applies this theorem directly, so every later rigidity or normalization argument that needs a differentiable vacuum kinetic Hamiltonian inherits the result for free.
In the Seven Gaps gravity program the declaration sits in the R5/R6 attack surface: local-profile functional equations must be differentiable before one can differentiate under the sum, extract partials in the $p$ and $q$ directions, and eventually force the profile shape. It does not itself close rigidity; it only licenses the differential calculus used by those later steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.