hasFDerivAt_localCell
plain-language theorem explainer
At each site of the two-site phase space, the local Hamiltonian cell map built from a profile is Fréchet differentiable, with derivative the linear combination of coordinate functionals weighted by the three coefficient profiles in the smoothness witness. Gravity and ILG workers cite it to extract partials of local cells and to force uniqueness of those coefficient slots. The proof is a one-line wrapper unpacking the differentiability field of the smoothness structure.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian profile and $S$ a smoothness witness for $h$ (supplying coefficient profiles $h_a,h_b,h_p$). For every site $j\in\mathbb{Z}/2\mathbb{Z}$ and every point $x=(q,\pi)$ in the two-site phase space, the map $y\mapsto h(q_j(y),q_{j+1}(y),\pi_j(y))$ is Fréchet differentiable at $x$, with derivative the continuous linear map $h_a\,\mathrm{d}q_j+h_b\,\mathrm{d}q_{j+1}+h_p\,\mathrm{d}\pi_j$ evaluated at the cell coordinates of $x$.
background
The module is Wave C2 R5/R6 groundwork for the local-profile functional equation at lattice size $n=2$, mirroring the Hamiltonian-dynamics package. It reduces the dynamical Hamiltonian identity for local profiles toward the momentum-density factorization $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$. The module is an R6 attack surface; nothing here proves rigidity.
Phase space on $n$ sites is the product of configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and conjugate momentum $\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. A local Hamiltonian profile is a real map of three arguments (two neighboring configurations and one momentum). A smoothness witness packages three coefficient profiles $h_a,h_b,h_p$ together with a Fréchet certificate for each cell map $y\mapsto h(q_j,q_{j+1},\pi_j)$, whose derivative is the indicated linear combination of the coordinate functionals $\mathrm{d}q_j$, $\mathrm{d}q_{j+1}$, $\mathrm{d}\pi_j$.
The continuous linear map assembled from those coefficients at a fixed point is exactly the cell derivative used as the claimed Fréchet derivative.
proof idea
One-line wrapper. The smoothness structure already carries a field asserting Fréchet differentiability of each cell map at every site and phase-space point, with derivative equal to the coefficient combination that defines the cell derivative. The lemma applies that field at the given site and point.
why it matters
Uniqueness theorems for the $h_b$ and $h_p$ coefficient slots invoke Fréchet uniqueness on this derivative: if two smoothness witnesses exist for the same profile, their $h_b$ (resp. $h_p$) values agree because both realize the unique Fréchet derivative of the same cell map. Parallel results identify those slots with the corresponding directional Fréchet derivatives of the profile map under a $C^2$ hypothesis.
The same lemma lifts, by finite sum and scalar multiplication, to Fréchet differentiability of the full local Hamiltonian assembled from a profile and a density weight. That places the result on the R6 path toward kinetic-normalized rigidity of local Hamiltonian profiles in the Seven Gaps gravity program, without closing the rigidity claim itself. The parent chain sits in the gravity domain of Recognition Science, feeding the local functional equation that is meant to constrain Hamiltonian profiles before global ILG action comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.