concreteDynamicInverseMetric_eq_sample
plain-language theorem explainer
When a phase-space coordinate samples a continuum field profile q at a Riemann node k/N, the concrete dynamic inverse metric equals 1 + q(k/N)^2. Continuum-smearing and lattice-to-integral arguments cite this to pin lattice values to the continuum structure law G = 1 + q^2. Proof is a one-line specialization of the general profile identity at t = k/N.
Claim. Let $q:\mathbb{R}\to\mathbb{R}$, $N,k\in\mathbb{N}$, $x$ a point of 2-dimensional phase space, and $j\in\mathbb{Z}/2\mathbb{Z}$. If the $j$-th coordinate of $x$ equals $q(k/N)$, then the concrete dynamic inverse metric of $x$ at index $j$ equals $1+\bigl(q(k/N)\bigr)^2$.
background
Module Wave C2 R3 extends the banked fixed-background continuum reach so the structure-function profile is induced by a continuum field $q$ through the same law that lives in the dynamic lattice bracket:
$$G(x)=1+(q,x)^2.$$
That is the continuum shape of the concrete dynamic inverse metric along $q$, witnessed by the HamDyn family built on that metric. The admissible class is $q$ continuous on $[0,1]$; no global continuity is required.
The sibling identity equates the concrete dynamic inverse metric at a phase-space point to the dynamic structure profile of $q$ evaluated at the matching field value. The profile itself is the named map $t\mapsto 1+q(t)^2$. This theorem only specializes that identity to the Riemann-sum nodes $k/N$ used in lattice sums.
proof idea
One-line term proof. Apply the general identity that the concrete dynamic inverse metric equals the dynamic structure profile of $q$ at the field value matching the phase-space coordinate, instantiated at $t=k/N$ with the sampling hypothesis. Then simpa unfolds the structure-profile definition to obtain the explicit right-hand side $1+q(k/N)^2$.
why it matters
Pins lattice samples of the dynamic inverse metric to the continuum structure law $G=1+q^2$ at Riemann nodes. That match is the bridge from the dynamic lattice bracket to continuum smearing: $h$-scaled lattice sums of $G\cdot(W_r\cdot S)$ with $G$ the dynamic profile are set up to tend to the integral on $[0,1]$, unlike the fixed-background weighted reach.
Honesty constraints from the module stand: this is only the smearing half of the continuum story; the sampled-lapse Wronskian rate-$h$ limit stays open in ledger terminal R4 and is not claimed here. Does not flip gap5_constraint_recovery. No downstream dependents are recorded yet; the immediate consumers are the dynamic weighted continuum-reach package and the typed residual for gap-5 dynamic continuum smearing in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.