HamDyn_eq_naive
plain-language theorem explainer
On two-site phase space, the Frechet-ready unfolded dynamic Hamiltonian equals the naive construction that feeds the concrete dynamic inverse metric into the frozen weight Hamiltonian, for every lapse N. Gravity workers checking that the R1 candidate matches its expanded form cite this. The proof is pointwise: unfold both sides, align the finite sums, and finish by ring.
Claim. For every lapse $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the unfolded dynamic Hamiltonian $$H_{\mathrm{dyn}}(N)(q,p)=\sum_{i\in\mathbb{Z}/2\mathbb{Z}}\frac{N_i}{2}\Bigl(p_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\Bigr)$$ equals the naive dynamic Hamiltonian obtained by substituting the concrete dynamic inverse metric into the frozen weight Hamiltonian $H_W$.
background
This module treats Wave C2 residuals R0 and R1 for the dynamic structure-function bracket on two lattice sites. Phase space is PhaseSpace 2: configuration and momentum fields on $\mathbb{Z}/2\mathbb{Z}$. The lapse $N$ weights each site.
HamDyn is the fully expanded scalar used for Frechet calculus: at each site it sums kinetic $p_i^2$ and a configuration term $(1+q_i^2)(\Delta q_i)^2$, scaled by $N_i/2$. The sibling naiveDynamicHamW is the lookalike that plugs concreteDynamicInverseMetric into the frozen weight Hamiltonian HamW and reuses frozen partials.
Module doc: R0 is the decoy claim that this naive plug-in already works with frozen partials (it fails: $\partial g/\partial q$ is uncompensated). R1 asserts that the same candidate, differentiated honestly, inhabits the phase-space-dependent Hamiltonian construction and recovers the target dynamic structure function in the Hamiltonian–Hamiltonian bracket.
proof idea
Term/tactic hybrid, purely algebraic. Apply function extensionality on phase-space points. Unfold HamDyn, naiveDynamicHamW, HamW, and concreteDynamicInverseMetric so both sides are explicit finite sums over $\mathbb{Z}/2\mathbb{Z}$. Reduce to summand-wise equality via Finset.sum_congr, then close each summand by ring. No analytic lemmas; the equality is definitional once the inverse-metric substitution is expanded.
why it matters
Establishes that the Frechet-ready form and the naive structure-function candidate are the same scalar on two sites. That identification is the bridge between the expanded calculus object and the construction that R1 places in PhaseSpaceDependentHamiltonianConstruction concreteDynamicInverseMetric at $n=2$.
It supports the R0/R1 closure narrative in the module: R0 shows the frozen-partial decoy fails; R1 shows honest derivatives cancel in the ham–ham bracket. The equality here guarantees one is not proving R1 about a different Hamiltonian than the decoy used for R0.
Does not flip gap5_constraint_recovery. Continuum and HKT residuals stay open. No downstream consumers are wired yet in the graph; the lemma is local scaffolding glue inside the SevenGaps dynamic-bracket development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.