dynamicInverseMetricN_eq
plain-language theorem explainer
On an n-site phase space the dynamic inverse-metric weight at site j equals one plus the squared configuration coordinate. Bracket and Frechet calculations for the general-n dynamic Hamiltonians cite this identity whenever the structure factor is expanded. Proof is a one-line simplification that unfolds the definition and rewrites a square as a product.
Claim. For every phase-space point $x$ on $n$ sites and every index $j\in\mathbb{Z}/n\mathbb{Z}$, the dynamic inverse-metric weight at $j$ equals $1+q_j(x)^2$, where $q_j$ is the configuration coordinate of $x$ at site $j$.
background
This module (Wave C2 R4 repair, Step 2) lifts the two-site dynamic structure bracket to arbitrary $n$ with $\mathrm{NeZero},n$. Phase space pairs configuration coordinates $q=x.1$ with momenta $p=x.2$, indexed by $\mathbb{Z}/n\mathbb{Z}$. The dynamic Hamiltonians $\mathrm{HamDynN},N$ weight nearest-neighbour differences by a structure factor $g_j=1+(q_j)^2$ placed at the left split point $j$, the same placement used by background weights in related Hamiltonians.
The two-site Frechet derivative $\mathrm{HamDynD}$ already isolates that metric factor so that $\mathrm{HasFDerivAt.const.add}$ applies cleanly; the general-$n$ bookkeeping copies the same pattern (including the $\partial g/\partial q$ correction). ZMod wraparound is periodic, so no boundary term appears. The present lemma simply names the pointwise value of that factor.
proof idea
One-line tactic proof: simp unfolds dynamicInverseMetricN and rewrites the squared configuration coordinate via pow_two, yielding the product form $1+q_j\cdot q_j$. No external lemmas are required beyond definitional reduction.
why it matters
The identity is local infrastructure for the general-$n$ dynamic bracket package. Sibling results (hasFDerivAt_HamDynN, partials in $p$ and $q$, bracket_HamDynN_HamDynN and its primed and evaluated forms) expand derivatives and Poisson brackets of $\mathrm{HamDynN}$; each expansion hits the structure factor and needs this equality to match the true RHS
$$\sum_j(N_j M_{j+1}-M_j N_{j+1}),(1+q_j^2),p_{j+1}(q_{j+1}-q_j).$$
That RHS is the calculus-derived target stated in the module doc and is the $n$-site lift of the proved $n=2$ bracket. In the broader Seven Gaps gravity line it keeps the dynamic-structure side honest while the Frechet and Kronecker-collapse arguments are rewritten for periodic rings. No external parent theorem is recorded yet (used_by is empty); the lemma exists so the module-internal bracket theorems can cite a named fact rather than re-unfold the definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.