HamDynN_eq_HamDyn
plain-language theorem explainer
At two sites, the general-n dynamic Hamiltonian with structure weight equals the original two-site Hamiltonian, definitionally. Anyone specializing the Wave C2 R4 general-n bracket back to the n=2 case cites this bridge. The proof is pure reflexivity: the two definitions coincide after fixing n=2.
Claim. For every coefficient map $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the general-$n$ dynamic Hamiltonian evaluated at $n=2$ equals the original two-site dynamic Hamiltonian: $\mathrm{HamDynN}_{n=2}(N)=\mathrm{HamDyn}(N)$.
background
The module generalizes the two-site dynamic structure bracket to arbitrary $n$ with $\mathrm{NeZero},n$. Both Hamiltonians live on discrete phase space: configuration and momentum fields indexed by $\mathbb{Z}/n\mathbb{Z}$. The kinetic slot is unweighted; the stiffness slot carries the structure factor $g_j=1+(q_j)^2$ at the left split point $j$, matching the placement used by the background weight in the related weighted Hamiltonian.
The original two-site form HamDyn is the unfolded expression used for Fréchet calculus on $n=2$. The general form HamDynN is the same sum over $\mathbb{Z}/n\mathbb{Z}$: for each site $i$, $(N_i/2)$ times kinetic energy plus $g$-weighted squared nearest-neighbor difference. ZMod wraparound is periodic, so the generalization introduces no boundary term.
This lemma is the definitional consistency check that the $n=2$ specialization of the general model is literally the old object.
proof idea
One-line reflexivity. After setting $n=2$, the body of the general Hamiltonian is identical (as a Lean term) to the body of the two-site Hamiltonian, so rfl closes the equality. No algebraic rewriting or calculus lemmas are required.
why it matters
The parent use is the consistency theorem that the general-$n$ Poisson bracket of two dynamic Hamiltonians, specialized to $n=2$, recovers the original two-site bracket identity. That parent rewrites both Hamiltonian arguments via this equality, then inherits the $n=2$ result.
In the Seven Gaps gravity stack this is bookkeeping for Wave C2 R4 Step 2: once the general RHS $\sum_j(N_j M_{j+1}-M_j N_{j+1})\cdot((1+q_j^2),p_{j+1}(q_{j+1}-q_j))$ is proved, the $n=2$ case must match the already-established two-site structure bracket without a separate calculation. The lemma is the definitional hinge for that recovery. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it keeps the discrete gravity Hamiltonian layer coherent under the $n$-generalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.