frozen_structure_differs_from_dynamic_id
plain-language theorem explainer
The dynamic structure factor of the identity map at unit time is not the constant frozen profile value 1. Anyone separating the frozen-G≡1 continuum integrand from the dynamic G=1+q² shape cites this. The proof is a one-line unfold of the structure-profile definition, giving 1+id(1)²=2≠1.
Claim. If $G$ is the dynamic structure profile $G(q)=1+q^2$ and $\mathrm{id}$ is the identity map on $\mathbb{R}$, then $G(\mathrm{id})(1)\neq 1$. Equivalently, the frozen constant-1 structure is not the dynamic structure evaluated on $q=\mathrm{id}$ at $t=1$.
background
Module Wave C2 R4 packages the sampled-lapse Wronskian rate-$h$ residual with the R2 lattice RHS shape and the R3 dynamic structure profile into a continuum shape limit. Lattice summands of the dynamic Hamiltonian bracket scale as $W_k\cdot G_k\cdot(\pi_{k+1}\Delta q_k)$ with structure factor $G_k=1+q(k/n)^2=O(1)$; the honest continuum object is $n\sum$, converging to $\int(NM'-MN')\cdot G\cdot(p\cdot q')$.
The module flags an explicit decoy: the frozen-1 continuum integrand differs from the dynamic $G=1+q^2$ integrand when $q=\mathrm{id}$. The dynamic structure profile is the continuum stand-in for that $G$; the frozen profile is the constant function $1$. Identity here is the real identity map (also appearing as the identity automorphism/homomorphism upstream), evaluated at the sample point $t=1$.
proof idea
Term-mode one-liner: simp [dynamicStructureProfile] unfolds the definition of the dynamic structure profile on the identity map. Under that definition $G(\mathrm{id})(1)=1+\mathrm{id}(1)^2=1+1=2$, which is definitionally unequal to the frozen value $1$. No external lemmas are required beyond the profile def.
why it matters
Feeds the sibling theorem frozen_continuum_density_differs_from_dynamic, whose doc-comment records the explicit continuum-density mismatch at $t=1$ for $N\equiv 1$, $M=\mathrm{id}$, $p\equiv 1$, $q=\mathrm{id}$: dynamic value $2$, frozen value $1$. That parent uses this inequality inside a simp of the continuum Dirac density against the frozen Wronskian–flux product.
In the SevenGaps gravity stack this is the honesty decoy named in the module header: R3 smearing-shape reach alone does not force frozen and dynamic integrands to agree. It does not close gap5 constraint recovery (needs R6) and does not bind the still-free ledger name dirac_algebra_continuum_limit, which awaits a general-$n$ HamDyn binding and periodic wrap treatment. Landmark contact is local to the continuum bracket shape, not T0–T8 forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.