differentiable_HamDynN
plain-language theorem explainer
The general-n dynamic Hamiltonian with site weights N is Fréchet differentiable as a real map on cyclic phase space. Anyone forming Poisson brackets of structure-weighted Hamiltonians on the Z/n lattice cites this lemma. The argument is a one-line conversion: the already-proved Fréchet derivative at each point yields differentiability at that point, hence global differentiability.
Claim. For every weight map $N:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$, the dynamic Hamiltonian $H_N^{\mathrm{dyn}}$ on phase space (kinetic term unweighted, stiffness weighted by $1+(q_i)^2$) is differentiable over $\mathbb{R}$.
background
This module repairs the dynamic structure bracket at general period $n$ (with NeZero n), lifting the two-site construction. Phase space is the product of configuration and momentum fields indexed by $\mathbb{Z}/n\mathbb{Z}$. The model Hamiltonian $H_N^{\mathrm{dyn}}$ sums, over each site $i$, a kinetic slot $\tfrac12 N_i p_i^2$ plus a stiffness slot $\tfrac12 N_i(1+q_i^2)(q_{i+1}-q_i)^2$.
The structure factor $g_j=1+(q_j)^2$ sits at the left split point of each bond, matching the placement used by the background-weight Hamiltonian. Differentiability of $H_N^{\mathrm{dyn}}$ is the analytic prerequisite for the Hamiltonian–Hamiltonian Poisson bracket and for the Fréchet bookkeeping (partials in $p$ and $q$, Kronecker collapse, periodic reindex) that produces the exact structure-function identity.
Upstream, the pointwise Fréchet derivative hasFDerivAt_HamDynN already exists; the present statement only packages that local derivative into global differentiability on the real vector space of phase-space fields.
proof idea
One-line term proof. For each phase-space point $x$, invoke the sibling lemma that $H_N^{\mathrm{dyn}}$ has a Fréchet derivative at $x$, then apply the Mathlib conversion from HasFDerivAt to DifferentiableAt. The resulting pointwise differentiability assembles into Differentiable ℝ (HamDynN N).
why it matters
Without global differentiability the Poisson bracket of two dynamic Hamiltonians is not even defined in the calculus used here. The lemma feeds the recovery theorem bracket_HamDynN_recovers_bracket_HamDyn, which checks that at $n=2$ the general-$n$ bracket collapses to the concrete two-site dynamic inverse-metric formula. That recovery is the consistency hinge of Wave C2 R4 Step 2: the same telescoping $\partial g/\partial q$ cancellation that works for two sites continues to work under ZMod wraparound, with no boundary term.
In the broader Recognition gravity stack this is scaffolding for the exact dynamic structure-function identity ${H_N,H_M}=\sum_j(N_j M_{j+1}-M_j N_{j+1})\cdot g_j,p_{j+1}(q_{j+1}-q_j)$, the general-$n$ analogue of the $n=2$ bracket that underwrites structure-weighted continuum limits. It does not itself touch T5–T8 or the RCL; it is pure analytic infrastructure inside the SevenGaps gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.