dynamicInverseMetricN
plain-language theorem explainer
On the n-site periodic lattice phase space, the inverse-metric structure factor at site j is g_j = 1 + q_j^2. Structure-bracket identities for the general-n dynamic Hamiltonians cite this factor when rewriting the Ham–Ham Poisson bracket in metric form. It is a one-line algebraic definition, not a derived theorem.
Claim. For a phase-space point $x=(q,\pi)$ on the $n$-site periodic lattice and site index $j\in\mathbb{Z}/n\mathbb{Z}$, the inverse-metric factor is $g_j(x):=1+q_j^2$.
background
The ambient phase space is the product of configuration and conjugate momentum on a periodic lattice: $x=(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Upstream, this is the canonical lattice wave-field phase space used throughout the hypersurface-deformation and SevenGaps gravity stack.
This module (Wave C2 R4 repair, Step 2) lifts the two-site dynamic structure bracket to arbitrary $n$ with $\mathrm{NeZero},n$. The true general RHS of the Hamiltonian–Hamiltonian bracket places a structure factor $g_j=1+(q_j)^2$ at the left split point $j$, matching the placement of the background weight in the static weighted case. The factor multiplies the momentum-difference flux term $\pi_{j+1}(q_{j+1}-q_j)$.
Naming it separately lets later identities write the bracket in metric form without expanding $1+q_j^2$ inline.
proof idea
Pure definition: evaluate $1+(x.1,j)^2$, i.e. one plus the square of the configuration coordinate at site $j$. No lemmas, no tactics. A sibling equality lemma rewrites the power as a product for simp/simpa consumers.
why it matters
Feeds the headline general-$n$ identity: the exact dynamic structure-function bracket of two dynamic Hamiltonians, where $\partial g/\partial q$ corrections cancel by the same telescoping as the $n=2$ case. The primed form of that theorem is literally the unprimed RHS with this factor substituted for $1+q_j^2$. The equality lemma dynamicInverseMetricN_eq is the bridge used by that rewrite.
In the SevenGaps gravity program this is the structure slot of the dynamic inverse metric on the lattice, the object that makes the general-$n$ Poisson algebra match the continuum hypersurface-deformation pattern without boundary terms (ZMod wraparound is periodic). It is scaffolding for the R4 repair, not a forcing-chain (T0–T8) landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.