differentiable_HamDyn
plain-language theorem explainer
For any two-site lapse field N, the dynamic Hamiltonian HamDyn N is Fréchet differentiable on the two-site phase space. Gravity and HKT residual proofs cite this to populate the phase-space-dependent Hamiltonian construction and to differentiate vacuum-shifted Hamiltonians. The proof is a one-line pointwise conversion of the existing Fréchet derivative certificate.
Claim. For every lapse assignment $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the map $x\mapsto H_{\mathrm{dyn}}(N,x)$ on the two-site phase space is differentiable over $\mathbb{R}$. Explicitly, $H_{\mathrm{dyn}}(N,x)=\sum_{i\in\mathbb{Z}/2\mathbb{Z}}(N_i/2)\bigl(p_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\bigr)$.
background
Module Wave C2 targets residuals R0 and R1 of the dynamic structure-function bracket on two sites. R0 kills the naive decoy that freezes the inverse metric inside the old HamW slot: the configuration partial then carries an uncompensated $\partial g/\partial q$. R1 rebuilds the candidate with an honest Fréchet derivative (including $\partial g/\partial q$) so that the Hamiltonian–Hamiltonian bracket recovers the target dynamic structure function at $n=2$.
HamDyn N is the unfolded two-site Hamiltonian used for that calculus: a sum over $\mathbb{Z}/2\mathbb{Z}$ of kinetic $p_i^2$ plus a configuration term weighted by the dynamic factor $(1+q_i^2)$ and nearest-neighbour differences. Differentiability of this map is a prerequisite for any Poisson-bracket identity that invokes Fréchet derivatives of the Hamiltonian densities.
The local ambient type is the two-site phase space (configuration and momentum fields on $\mathbb{Z}/2\mathbb{Z}$). Continuum and full HKT constraint recovery remain open; this lemma only supplies the $C^1$ certificate for the discrete dynamic Hamiltonian.
proof idea
One-line term proof. At each phase-space point $x$, invoke the already-proved pointwise Fréchet derivative certificate hasFDerivAt_HamDyn N x and convert it with Mathlib's HasFDerivAt.differentiableAt. No new derivative computation occurs here; the work lives in the upstream Fréchet lemma.
why it matters
This is the differentiability half of residual R1. Downstream, concreteDynamicHamiltonianConstruction packages HamDyn together with this lemma and the ham_ham bracket identity into an inhabitant of PhaseSpaceDependentHamiltonianConstruction concreteDynamicInverseMetric at $n=2$.
HKT vacuum-sector work reuses it directly: differentiable_HamVac is the sum of this certificate with the vacuum-smear derivative; bracket_HamVac_HamVac and bracket_MomDyn_HamVac compare vacuum-shifted brackets against the pure dynamic ones; hamDynPointSplitTarget and vacuumShiftStrongTarget install HamDyn densities into the repaired point-split Dyn targets.
In the Recognition gravity stack this is scaffolding for discrete Hamiltonian structure functions on the two-site model, not yet a continuum or full constraint-recovery result. Gap5 continuum and HKT residuals stay open per the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.