HamDynD
plain-language theorem explainer
Explicit Fréchet derivative of the two-site dynamic Hamiltonian HamDyn, as a continuous linear map on phase space. Anyone computing honest configuration/momentum partials for the dynamic structure-function bracket cites this map. The body is a term-mode sum of scaled coordinate functionals, with a dummy 0+ term so the metric factor matches HasFDerivAt.const.add.
Claim. For a lapse $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and a phase-space point $x=(q,\pi)$ on the two-site lattice, $\mathrm{HamDynD}(N,x)$ is the continuous linear map $T_x\mathrm{PhaseSpace}_2\to\mathbb{R}$ equal to the Fréchet derivative $D(\mathrm{HamDyn}\,N)_x$. Explicitly it is $\sum_{i\in\mathbb{Z}/2\mathbb{Z}}(N_i/2)\cdot\bigl(2\pi_i\,d\pi_i + (1+q_i^2)\cdot 2\Delta q_i\,d(\Delta q_i) + (\Delta q_i)^2\cdot 2q_i\,dq_i\bigr)$, with $\Delta q_i=q_{i+1}-q_i$.
background
The ambient setting is the two-site lattice wave field of Wave C2 (residuals R0–R1). Phase space is $\mathrm{PhaseSpace},n=(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$; here $n=2$. Coordinate functionals $\mathrm{coordQ},i$ and $\mathrm{coordP},i$ are the continuous linear projections onto $q_i$ and $\pi_i$.
The scalar Hamiltonian $\mathrm{HamDyn},N$ is the unfolded dynamic candidate $$\sum_i\frac{N_i}{2}\Bigl(\pi_i^2+(1+q_i^2)(\Delta q_i)^2\Bigr),$$ where the factor $g_i=1+q_i^2$ is the concrete dynamic inverse metric. Unlike the frozen $\mathrm{HamW}$ slot, $g$ depends on configuration, so honest Fréchet calculus must retain $\partial g/\partial q$.
Module goal: show this Hamiltonian inhabits the phase-space-dependent construction and that the Hamiltonian–Hamiltonian bracket recovers the target dynamic structure function after the extra derivative terms cancel.
proof idea
Pure definition, not a proof. The body is the term obtained by formally differentiating $\mathrm{HamDyn}$ under the sum: each summand contributes a scaled continuous linear map built from $\mathrm{coordP},i$, $\mathrm{coordQ},i$, and $\mathrm{coordQ},(i+1)$. Kinetic piece yields $2\pi_i,d\pi_i$. Metric piece is product-ruled: constant-plus-$q_i^2$ times $(\Delta q_i)^2$ produces the two summands with doubled $\Delta q$ differentials and the $2q_i,dq_i$ factor. The final metric factor is written $0+\cdots$ solely to line up with HasFDerivAt.const.add in the companion lemma.
why it matters
This map is the witness that $\mathrm{HamDyn}$ is Fréchet differentiable. Downstream, hasFDerivAt_HamDyn asserts $\mathrm{HasFDerivAt},(\mathrm{HamDyn},N),(\mathrm{HamDynD},N,x),x$; the momentum and configuration partials pderivP_HamDyn and pderivQ_HamDyn read off by applying the map and simplifying. The configuration partial carries the honest $\partial g/\partial q$ correction $N_j q_j(\Delta q_j)^2$ that the decoy (R0) missed.
Those partials feed the Hamiltonian–Hamiltonian bracket identity that closes residual R1: the candidate inhabits PhaseSpaceDependentHamiltonianConstruction concreteDynamicInverseMetric at $n=2$, and extra derivative terms cancel so ham_ham recovers the dynamic structure function. It does not flip gap5_constraint_recovery; continuum and HKT residuals stay open. Also referenced when generalizing the inverse-metric identity in the $N$-site module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.