hasFDerivAt_LocalHamFromProfile
plain-language theorem explainer
At every two-site phase-space point, the local Hamiltonian built by summing lapse-weighted profile cells is Fréchet differentiable, with derivative the matching sum of cell derivatives. Anyone extracting momentum densities or partials of the n=2 local ham cites this. Proof is a short sum of scaled cell Fréchet derivatives from the smoothness package.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian profile equipped with smoothness data (partial profiles and a Fréchet certificate for each cell map), and let $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. Then for every $x$ in the two-site phase space, the map $x\mapsto\sum_j N_j\, h(q_j,q_{j+1},p_j)$ has Fréchet derivative at $x$ equal to $\sum_j N_j\cdot D(\text{cell}_j)(x)$.
background
This module is Wave C2 R5/R6 groundwork for the local-profile functional equation at $n=2$ (mirroring HamDyn). The goal is to reduce the dynamical Hamiltonian identity for local profiles to a momentum-density factorization $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$; R6 is the attack surface and nothing here proves rigidity.
A local Hamiltonian profile is a map $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, read as a cell density on $(q_j,q_{j+1},p_j)$. Smoothness data packages three partial profiles $h_a,h_b,h_p$ together with a certificate that each cell map $y\mapsto h(y_1(j),y_1(j+1),y_2(j))$ is Fréchet differentiable with derivative $h_a,\mathrm{d}q_j+h_b,\mathrm{d}q_{j+1}+h_p,\mathrm{d}p_j$. The assembled local Hamiltonian is $\sum_j N_j,h(q_j,q_{j+1},p_j)$ on the two-site phase space; its candidate derivative is the same sum of scaled cell derivatives.
The immediate upstream fact is that each individual cell already has the stated Fréchet derivative (the smoothness field itself).
proof idea
Unfold the assembled Hamiltonian and its candidate derivative. Apply the sum rule for Fréchet derivatives over $j\in\mathbb{Z}/2\mathbb{Z}$, and on each summand pull out the constant factor $N_j$ via constant-multiplication of derivatives. Each cell contribution is exactly the upstream cell Fréchet lemma, which is the smoothness certificate applied at $(j,x)$.
why it matters
This is the differentiability engine for the local-profile Hamiltonian at $n=2$. Downstream it discharges global differentiability of the assembled map, and it supplies the concrete Fréchet derivative used to evaluate the $p$- and $q$-partials: the $p$-partial collapses to $N_k,h_p$ on the active cell, while the $q$-partial mixes $N_k,h_a$ with the neighboring $N_{k-1},h_b$ term. Those partials are the bridge from the local profile to the momentum-density identity targeted by R5/R6. In the broader SevenGaps gravity stack this is scaffolding toward the hypersurface-deformation / ILG Hamiltonian analysis, not yet a rigidity or uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.