frozen_continuum_density_differs_from_dynamic
plain-language theorem explainer
At continuum level, the Dirac structure density with dynamic profile G = 1 + q² differs from the frozen-G≡1 integrand at t = 1 on the constant-lapse, identity-field configuration. Dynamic value is 2; frozen value is 1. Cited by anyone tracking the SevenGaps frozen-vs-dynamic honesty demotion. Proof is a one-line simplification of the density definitions and elementary derivatives.
Claim. For constant lapse $N \equiv 1$, identity shift $M = \mathrm{id}$, identity configuration $q = \mathrm{id}$, and constant momentum $p \equiv 1$, the continuum Dirac density at $t = 1$ (structure factor $G = 1 + q^2$) is unequal to the frozen integrand that replaces $G$ by $1$: left side equals $2$, right side equals $1$.
background
The module lands the sampled-lapse Wronskian rate-$h$ residual as a continuum shape theorem for the dynamic bracket. Continuum Dirac density is $(N M' - M N') \cdot G \cdot D$ with structure profile $G = 1 + q^2$ and momentum flux $D = p \cdot q'$. Continuum momentum flux is the pointwise product $p(t),q'(t)$.
The module doc flags an explicit decoy: the frozen-$1$ continuum integrand differs from the dynamic $G = 1+q^2$ integrand for $q = \mathrm{id}$. This declaration is that decoy at a concrete evaluation point. Upstream, the shape continuum limit shows scaled sampled dynamic-bracket sums tend to the integral of the continuum Dirac density; the present mismatch shows why freezing $G \equiv 1$ would target the wrong continuum object.
proof idea
Term-mode proof by simp on the two density definitions together with the dynamic structure profile, deriv_id, and deriv_const. Unfolding yields Wronskian factor $1\cdot 1 - 1\cdot 0 = 1$, dynamic $G(1) = 1 + 1^2 = 2$, flux $1\cdot 1 = 1$, so the left side is $2$; the frozen right side drops $G$ and equals $1$. No mean-value or limit lemmas are required.
why it matters
Documents the decoy called out in the module honesty section: frozen continuum integrand differs from the dynamic $G = 1+q^2$ integrand on $q = \mathrm{id}$. Supports the claim that the rate-$h$ continuum limit must carry the phase-space-dependent structure, not a frozen $G \equiv 1$ placeholder. Sits beside the dynamic bracket shape continuum limit (which converges to the dynamic density) and the discrete decoy that frozen structure differs from dynamic on the identity. Does not close the ledger name for the Dirac algebra continuum limit, held free pending general-$n$ HamDyn binding and periodic wrap treatment. No downstream consumers yet; it is a receipt that the frozen and dynamic continuum objects are genuinely distinct.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.