LocalHamFromProfileD
plain-language theorem explainer
Defines the Fréchet derivative of a two-site local Hamiltonian built from a smooth profile: a continuous linear map on phase space equal to the N-weighted sum of the three-term cell derivatives. Gravity workers cite it when differentiating local HKT profiles before extracting momentum densities. The body is a two-line sum of scaled cell maps.
Claim. Given a local profile $h:\mathbb{R}^3\to\mathbb{R}$ with smooth data $(h_a,h_b,h_p)$ witnessing cellwise Fréchet differentiability, a lapse $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, and a phase-space point $x$, the continuous linear map $DH(x):T_x\mathrm{PhaseSpace}_2\to\mathbb{R}$ is $\sum_{j\in\mathbb{Z}/2\mathbb{Z}} N(j)\, D\mathrm{cell}_j(x)$, where each cell derivative is $h_a\,dq_j+h_b\,dq_{j+1}+h_p\,dp_j$ evaluated at the neighboring coordinates of $x$.
background
The module is Wave C2 R5/R6 groundwork for the local-profile functional equation at $n=2$ (mirroring HamDyn). It reduces the dynamical Hamiltonian identity for local profiles toward the momentum-density relation $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$; R6 is the attack surface and nothing here proves rigidity.
Phase space on the two-site periodic lattice is pairs $(q,\pi)$ of maps $\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. A local Hamiltonian profile is any $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, read as $h(q_j,q_{j+1},p_j)$. Smoothness packages three companion profiles $h_a,h_b,h_p$ together with the cellwise Fréchet derivative identity: each cell map has derivative $h_a,\mathrm{coord}Q_j+h_b,\mathrm{coord}Q_{j+1}+h_p,\mathrm{coord}P_j$.
The sibling localCellD is exactly that three-term continuous linear map at a fixed site and base point. The total local Hamiltonian from a profile is the $N$-weighted sum of the cells; this definition is the corresponding derivative object.
proof idea
Pure definitional construction, not a proof. The continuous linear map is written as the finite sum over $j:\mathbb{Z}/2\mathbb{Z}$ of the scalar multiple $(N,j)\bullet\mathrm{localCellD},h,S,j,x$. Each summand reuses the already-defined cell derivative (the linear combination of the three coordinate functionals with coefficients $h_a,h_b,h_p$ at the neighboring phase-space values). No tactics or lemmas are invoked; the equality is by construction.
why it matters
This derivative object is the linear map that the Fréchet-differentiability lemma for the profile Hamiltonian identifies as $D(\mathrm{LocalHamFromProfile},h,N)$ at each base point. Downstream partial-derivative theorems then read off the $P$- and $Q$-directional derivatives by applying that map: $p$-derivatives collapse to $N_k,h_p$ at site $k$, while $q$-derivatives mix the $h_a$ term at $k$ with the $h_b$ term from the previous site. Those identities are the concrete R5/R6 groundwork toward reducing the dynamical Hamiltonian constraint for local profiles to the momentum-density factorization. In the broader Recognition gravity stack this sits inside the hypersurface-deformation / ILG action layer for lattice wave fields; it does not yet touch the forcing chain (T5–T8) or the global constants ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.