dynamicStructureProfile_eq_one_add_sq
plain-language theorem explainer
The continuum dynamic structure profile equals one plus the squared field value at every point. Gravity continuum-limit arguments cite this when unpacking the structure factor G in the scaled Wronskian integrand. The proof is definitional reflexivity: the profile is defined by that formula.
Claim. For every real field profile $q:\mathbb{R}\to\mathbb{R}$ and every $t\in\mathbb{R}$, the continuum dynamic structure profile satisfies $G_q(t)=1+(q(t))^2$.
background
In the SevenGaps gravity stack, the continuum shape of the concrete dynamic inverse metric along a field profile is the structure factor $G(x)=1+(q x)^2$. The definition dynamicStructureProfile packages exactly that map: send a profile $q$ to the function $x\mapsto 1+(q x)^2$.
This module (Wave C2 R4) lands the sampled-lapse Wronskian rate-$h$ residual together with the R2 lattice RHS shape and the R3 dynamic structure profile. Lattice bookkeeping treats the structure summand as $G_k=1+q(k/n)^2=O(1)$, so the honest scaled object $n\cdot\sum$ converges to an integrand carrying $G\cdot(p\cdot q')$.
The upstream definition states: continuum shape of the concrete dynamic inverse metric along a field profile is $G(x)=1+(q x)^2$. The present lemma is the pointwise unfolding of that model.
proof idea
One-line definitional proof: rfl. The left-hand side reduces by unfolding the definition of the continuum structure profile, which is literally $x\mapsto 1+(q x)^2$, so equality holds by construction.
why it matters
Gives a named, citable identity for the dynamic structure factor that appears throughout the continuum bracket analysis. Module scaling notes write the lattice summand shape as $W_k\cdot G_k\cdot(\pi_{k+1}\Delta q_k)$ with $G_k=1+q(k/n)^2=O(1)$; this lemma is the continuum counterpart of that $G$.
It supports the renamed shape theorem dynamic_bracket_shape_continuum_limit and the rate-$h$ analysis (wronskian_rate_h_tendsto, forward-density control). The module holds the ledger name dirac_algebra_continuum_limit free pending a general-$n$ HamDyn binding; this identity is independent of that gap and only records the R3 profile shape.
No downstream dependents are wired yet in the graph; the lemma is local infrastructure for rewriting $G$ in continuum integrands and decoy comparisons (frozen-1 vs dynamic $1+q^2$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.