hasFDerivAt_hamDynLocalCell_raw
plain-language theorem explainer
On the two-site phase space, the honest local HamDyn density is Fréchet differentiable everywhere, with derivative equal to the precomputed continuous-linear map built from product-rule data. Gravity and HKT-rigidity arguments cite this to justify differentiating the local cell before assembling global Hamiltonians. The proof expands the profile by the chain and product rules from the coordinate projections and matches the scaled numerator form.
Claim. For every site index $j \in \mathbb{Z}/2\mathbb{Z}$ and every point $x$ in the two-site phase space $(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$, the map $y\mapsto \tfrac12\bigl(p_j(y)^2+(1+q_j(y)^2)(q_{j+1}(y)-q_j(y))^2\bigr)$ is Fréchet differentiable at $x$, and its derivative equals the continuous linear map obtained by scaling the product-rule expansion of that numerator by $1/2$.
background
The ambient model is the canonical phase space of a lattice wave field: configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and conjugate momentum $\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ on a periodic lattice. Here $n=2$. Coordinate projections $q_k$ and $\pi_k$ are continuous linear functionals, hence Fréchet differentiable with derivative equal to themselves.
The local HamDyn profile is the scalar density $\tfrac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)$ in neighboring configuration values $a,b$ and momentum $p$. Its companion continuous-linear map packages Mathlib's product-rule expansion of that numerator, scaled by $1/2$, so that a later const_mul step lines up exactly.
Module context is Wave C2 gap5: after killing strong rigidity with a balanced-quartic falsifier, Session B installs an honest HamDyn inhabitant of the CanonicalMom target class. Differentiability of the local cell is the analytic prerequisite for that inhabitant and for vacuum-sector comparisons.
proof idea
Start from Fréchet differentiability of the coordinate maps $y\mapsto y.1,j$, $y\mapsto y.1,(j+1)$, and $y\mapsto y.2,j$. Form the difference $q_{j+1}-q_j$, square it by the product rule, square $q_j$, add the constant $1$, multiply to get the structure gradient $(1+q_j^2)(q_{j+1}-q_j)^2$, square the momentum coordinate, add, and scale by $1/2$.
A short funext identity rewrites the profile as exactly that scaled numerator. After rewriting, the assembled derivative is the claimed continuous-linear map.
why it matters
This lemma is the raw differentiability engine for the honest HamDyn local cell inside the CanonicalMom target. The immediate parent rewrites the same derivative in the expanded basis of partials times coordinate functionals, which is the form needed when assembling global Hamiltonians and checking CanonicalMom axioms.
It is also reused in the vacuum-sector kill path: the vacuum-shift local cell is built by modifying the same profile, so its raw Fréchet lemma invokes this one and adjusts the remainder. In the SevenGaps gravity program this closes an analytic gap on the repaired CanonicalMom route (binding design D-qg-hkt-rigidity-route), without flipping the ledger flag gap5_constraint_recovery. It does not itself prove rigidity; it supplies the $C^1$ cell data that later sessions need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.