dynamicStructureProfile
plain-language theorem explainer
Defines the continuum structure-function profile G_q(x) = 1 + (q(x))^2 induced by a real field profile q. Gravity continuum and Dirac-algebra modules cite it as the smeared shape of the dynamic inverse metric. The body is a one-line pointwise definition, not a derived identity.
Claim. For a real field profile $q:\mathbb{R}\to\mathbb{R}$, the induced continuum structure profile is the map $G_q:\mathbb{R}\to\mathbb{R}$ given by $G_q(x)=1+(q(x))^2$.
background
Wave C2 R3 extends fixed-background continuum reach so the structure-function profile is induced by a continuum field $q$, not held frozen. The governing law is the same one that inhabits the dynamic lattice bracket: $G(x)=1+(q(x))^2$, the continuum shape of the concrete dynamic inverse metric along $q$. The package is witnessed by the HamDyn family (phase-space-dependent Hamiltonian construction with that inverse metric).
Admissible $q$ are continuous on the closed unit interval $[0,1]$; global continuity is not required. This module is the smearing half of the continuum story only. The sampled-lapse Wronskian rate-$h$ limit remains open under the ledger name for the full Dirac-algebra continuum limit, and gap-5 constraint recovery is not flipped here.
proof idea
Pure definitional abbreviation: the profile is introduced as the anonymous function $x\mapsto 1+(q(x))^2$. No lemmas are applied; equality to $1+(q,t)^2$ is definitional (rfl downstream).
why it matters
This profile is the continuum carrier of dynamic structure in the Seven Gaps gravity stack. Downstream, the continuum Dirac density multiplies the Wronskian factor by $G_q$ and a momentum flux; sampled dynamic-bracket sums use the same $G_q$ on the mesh $k/n$. The shape-only Riemann theorem then sends scaled sampled sums to $\int_0^1$ of that density, with $G=1+q^2$ phase-space dependent.
It also supplies the decoy contrast against frozen structure: $G_{\mathrm{id}}(1)=2\neq 1$, and the corresponding continuum densities differ. That separation is what makes dynamic smearing strictly larger than background-weighted reach. It does not close the open R4 continuum-limit ledger name or gap-5 recovery; it only banks the $G$ factor those arguments need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.