concreteDynamicInverseMetric_eq_dynamicStructureProfile
plain-language theorem explainer
When a two-site phase-space configuration at lattice site j matches a continuum field profile q at sample location t, the lattice inverse-metric structure function equals the continuum profile value 1+(q t)^2. Continuum-smearing arguments in the dynamic gravity bracket cite this binding lemma to identify lattice and continuum structure shapes. The proof is a one-line simplification of the two model definitions under the matching hypothesis.
Claim. For any field profile $q:\mathbb{R}\to\mathbb{R}$, phase point $x$ on the two-site phase space, site $j\in\mathbb{Z}/2\mathbb{Z}$, and sample location $t\in\mathbb{R}$, if the configuration coordinate of $x$ at site $j$ equals $q(t)$, then the concrete dynamic inverse metric at $(x,j)$ equals $1+(q(t))^2$.
background
This module (Wave C2 R3) extends fixed-background continuum reach so the structure-function profile is induced by a continuum field $q$ through the same law that inhabits the dynamic lattice bracket: $G=1+(q\cdot)^2$. That law is the continuum shape of the concrete dynamic inverse metric along $q$, witnessed by the HamDyn family on the two-site phase space.
The lattice model is the positive inverse-metric candidate on two-site phase space: at phase point $x$ and site $j$ it returns $1+(x_1(j))^2$, depending only on the configuration coordinate at that site. The continuum counterpart is the dynamic structure profile $t\mapsto 1+(q(t))^2$. The admissible class is continuous-on-$[0,1]$ profiles; no global continuity is required.
The honesty clause is explicit: this rung is only the smearing half of the continuum story. The sampled-lapse Wronskian rate-$h$ limit stays open in the ledger terminal R4 and is not claimed here.
proof idea
One-line tactic proof. Unfold both model definitions (lattice inverse metric and continuum structure profile) and rewrite with the hypothesis that the configuration sample at site $j$ equals $q(t)$. Both sides reduce to $1+(q(t))^2$, so equality is immediate. No external lemmas are needed beyond definitional simplification.
why it matters
Binding lemma for the R3 dynamic continuum-smearing package. Downstream, the Riemann-sum specialization at sample points $k/N$ is a direct corollary, and the R3 headline residual packages this equality with the dynamic weighted continuum reach and the two-site dynamic-bracket residual.
In the Recognition gravity ledger this closes the identification step between lattice structure functions and continuum profiles induced by $q$, so weighted hypersurface sums can pass to continuum limits along the dynamic family rather than only fixed backgrounds. It does not flip gap-5 constraint recovery and does not discharge the open Dirac-algebra continuum limit (R4). Parent use is local to the SevenGaps continuum-smearing residual stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.