localCellD
plain-language theorem explainer
Packages the Fréchet derivative of one local Hamiltonian cell on the two-site phase space as a continuous linear map. Weights the three partial profiles (in the two neighboring configuration coordinates and the cell momentum) against the corresponding coordinate functionals. Downstream rigidity and functional-equation lemmas evaluate this map on basis directions to recover those partials and match them to ordinary fderivs.
Claim. Fix a local Hamiltonian profile $h:\mathbb{R}^3\to\mathbb{R}$ and smoothness data $S$ supplying partial profiles $h_a,h_b,h_p$ together with a cellwise Fréchet-derivative witness. For each lattice index $j\in\mathbb{Z}/2\mathbb{Z}$ and phase-space point $x=(q,\pi)$, define the continuous linear map $D_{h,S,j}(x):T_x\mathrm{PhaseSpace}_2\to\mathbb{R}$ by $D_{h,S,j}(x)=h_a(q_j,q_{j+1},\pi_j)\,dq_j+h_b(q_j,q_{j+1},\pi_j)\,dq_{j+1}+h_p(q_j,q_{j+1},\pi_j)\,d\pi_j$.
background
The module is Wave C2 R5/R6 groundwork: the local-profile functional equation at lattice size $n=2$ (mirroring HamDyn). It reduces the dynamical Hamiltonian identity for local profiles to the momentum-density relation $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$. Nothing here proves rigidity; the file only sets the attack surface.
Phase space is the product $(q,\pi)$ of configuration and conjugate momentum on the periodic two-site lattice. The continuous linear functionals $\mathrm{coordQ},i$ and $\mathrm{coordP},i$ extract $q_i$ and $\pi_i$. A local Hamiltonian profile is any map $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ reading two neighboring configuration values and one cell momentum. Smoothness data packages three companion profiles $h_a,h_b,h_p$ and asserts that, at every cell and every phase-space point, the Fréchet derivative of the cell evaluation is exactly the linear combination written in this definition.
proof idea
Pure definitional packaging, not a proof. The body is the three-term continuous-linear-map combination that already appears inside the smoothness witness: scale $\mathrm{coordQ},j$ by $h_a$ at the cell coordinates, scale $\mathrm{coordQ},(j+1)$ by $h_b$, and scale $\mathrm{coordP},j$ by $h_p$. No tactics, no lemmas applied; the expression is the derivative map the structure claims exists.
why it matters
This is the reusable derivative object for the $n=2$ local-profile functional equation. Same-module lemmas evaluate it on pure $q$- and $\pi$-basis directions to recover the partial profiles (cell directional identities). The sibling construction that rebuilds a local Hamiltonian from a profile uses it as the candidate Fréchet derivative, and the matching HasFDerivAt lemma closes that reconstruction.
In the kinetic-normalized rigidity module it is the evaluation engine: private lemmas read off $h_b$ and $h_p$ by applying the map to unit basis vectors, and the comparison theorems identify those partials with ordinary $\mathrm{fderiv}$ components of the profile map under $C^2$ hypotheses. That is the R6 attack surface the module doc flags: groundwork toward rigidity of local Hamiltonian profiles, not yet the rigidity theorem itself. Framework context is the gravity SevenGaps chain (hypersurface deformation / HamDyn mirror), not the T0–T8 forcing landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.