hasFDerivAt_HamDyn
plain-language theorem explainer
The dynamic two-site Hamiltonian is Fréchet differentiable at every phase-space point, with derivative equal to an explicit continuous linear map built from lattice coordinate functionals. Workers extracting honest momentum and configuration partials (including metric q-dependence) cite this lemma. The proof is a term-mode assembly of sum, product, difference, and constant Fréchet rules on the coordinate maps.
Claim. For every lapse $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and every point $x$ of the two-site phase space $(q,\pi)$, the scalar map $x\mapsto H_{\mathrm{dyn}}(N,x)=\sum_i(N_i/2)\bigl(\pi_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\bigr)$ is Fréchet differentiable at $x$, and its derivative equals the continuous linear map $DH_{\mathrm{dyn}}(N,x)$ obtained by differentiating the kinetic and metric-weighted difference terms sitewise.
background
Phase space on $n$ lattice sites is the product $(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Coordinate functionals $q_k$ and $\pi_k$ are continuous linear, hence Fréchet differentiable everywhere (their derivatives are the dual basis maps $\mathrm{coord}Q_k$ and $\mathrm{coord}P_k$).
The dynamic Hamiltonian $H_{\mathrm{dyn}}(N,\cdot)$ is the unfolded two-site scalar used for calculus: a sum over sites of lapse-weighted kinetic energy plus a metric factor $(1+q_i^2)$ times squared nearest-neighbour differences. Its candidate derivative $DH_{\mathrm{dyn}}(N,x)$ is the matching continuous linear map, written so the metric-factor contribution aligns with a constant-plus-product rule.
This module closes Wave C2 residuals R0–R1 for the dynamic structure-function bracket at $n=2$: the naive frozen Hamiltonian fails because configuration partials miss $\partial g/\partial q$, while the honest Fréchet derivative cancels those extras in the Hamiltonian–Hamiltonian bracket. Continuum and HKT residuals stay open.
proof idea
Unfold both the Hamiltonian and its candidate derivative. Apply the Fréchet sum rule over the two sites. For each summand, chain the product and sum rules: momentum coordinates contribute via $\mathrm{hasFDerivAt_coord_snd}$; configuration coordinates and their nearest-neighbour differences via $\mathrm{hasFDerivAt_coord_fst}$; the constant $1$ via $\mathrm{hasFDerivAt_const}$. Scale by the constant factor $N_i/2$. The resulting continuous linear map is definitionally $DH_{\mathrm{dyn}}(N,x)$.
why it matters
This is the calculus engine for residual R1: once the Fréchet derivative is known, the momentum partial recovers the kinetic slot unchanged by the metric factor, and the configuration partial acquires the honest $\partial g/\partial q$ correction $N_j q_j(\Delta q_j)^2$. Both partial theorems rewrite through this lemma's fderiv identity.
Differentiability of $H_{\mathrm{dyn}}$ is the one-line corollary. Together they place the candidate in the phase-space-dependent Hamiltonian construction at $n=2$, so the Hamiltonian–Hamiltonian bracket recovers the target dynamic structure function. The module does not flip gap5_constraint_recovery; continuum and HKT residuals remain open. No direct T0–T8 landmark is touched: this is discrete gravity scaffolding inside the SevenGaps program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.