function
plain-language theorem explainer
Packages the continuum structure-function profile induced by a field q via G(x)=1+(q x)^2, the continuum shape of the dynamic inverse metric. Gravity and continuum-limit authors cite it when lifting fixed-background weighted reach to a q-dependent dynamic family. As a structure definition it only records the data and equalities; no proof work lives here.
Claim. A structure whose data assert that the dynamic structure function coincides with the continuum profile value of $G(x)=1+(q x)^2$ for an admissible continuum field $q$ (continuous on $[0,1]$), matching the continuum shape of the concrete dynamic inverse metric along $q$.
background
Module Wave C2 R3 extends the banked fixed-background continuum reach (weighted structure-sum tendsto limits) so the structure-function profile is no longer a fixed background weight. Instead it is induced by a continuum field profile $q$ through the same algebraic law that inhabits the dynamic lattice bracket:
$$G(x)=1+(q x)^2.$$
That $G$ is the continuum shape of the concrete dynamic inverse metric along $q$, and the package is witnessed by the HamDyn family (phase-space-dependent Hamiltonian construction on that inverse metric).
Admissible $q$ need only be continuous on the closed unit interval; global continuity is not required. Upstream census and Ehrhart-span machinery supply the discrete structure-function side that this continuum profile is meant to smear against.
proof idea
Definitional structure, not a proved theorem. Fields package the continuum profile data and the equality between the structure function and that profile value; no tactics or lemma applications appear in the body. Downstream theorems that need the smeared dynamic family unpack these fields rather than re-deriving the $G(x)=1+(q x)^2$ identification.
why it matters
This is the smearing half of the dynamic continuum story inside the Seven Gaps gravity ladder. It lets later results (dynamic weighted continuum reach, typed residual for gap 5 continuum smearing, and the no-fixed-profile-equals-all-dynamic-profiles obstruction) treat $q$-dependent structure functions on the same footing as the fixed-background weighted hypersurface bracket.
It does not close the sampled-lapse Wronskian rate-$h$ limit (still open in the ledger terminal R4 continuum limit) and does not flip gap-5 constraint recovery. Within Recognition gravity it is the data hinge between the dynamic lattice bracket and continuum smearing, sitting under the broader HamDyn / phase-space-dependent Hamiltonian construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.