no_fixed_profile_equals_all_dynamic_profiles
plain-language theorem explainer
No single fixed weight profile can equal the dynamic structure-function profile of every continuous field q on [0,1]. Gravity residual auditors cite this decoy to block the claim that fixed-background continuum reach already covers the full HamDyn family. The proof specializes the universal-W hypothesis to the constant fields 0 and 1, then feeds the resulting pointwise collision into the banked miss lemma.
Claim. There is no fixed function $W:\mathbb{R}\to\mathbb{R}$ such that for every field profile $q:\mathbb{R}\to\mathbb{R}$ continuous on $[0,1]$, one has $W$ equal to the dynamic structure-function profile of $q$ (the continuum shape $G_q(x)=1+(q\,x)^2$ of the concrete dynamic inverse metric along $q$).
background
Wave C2 R3 packages dynamic structure-function continuum smearing: the fixed-background continuum reach is extended so the structure-function profile is induced by a continuum field $q$ through the same law that inhabits the dynamic lattice bracket, $G(x)=1+(q,x)^2$. That continuum shape is the dynamic structure profile of $q$, and the package is witnessed by the HamDyn family built on the concrete dynamic inverse metric.
Admissible fields are those continuous on the unit interval $[0,1]$; global continuity is not required. Honesty clauses in the module: this is only the smearing half of the continuum story; the sampled-lapse Wronskian rate-$h$ limit stays open in ledger terminal R4, and the package does not flip gap-5 constraint recovery.
A sibling already records that background weighted reach misses the dynamic family. The present statement is the stronger decoy: no one fixed $W$ can equal every dynamic profile at once.
proof idea
Proof by contradiction. Assume some fixed $W$ equals the dynamic structure profile of every $q$ continuous on $[0,1]$. Specialize to the two constant fields $q\equiv 0$ and $q\equiv 1$ (both continuous on the interval by the constant-map lemma). Then both dynamic profiles equal $W$, so they equal each other. Pointwise evaluation at $0$ (via function extensionality) produces a sample-point collision, which the sibling miss lemma background_weighted_reach_misses_dynamic_family rules out. The whole argument is a short specialize-and-rewrite tactic script; no analysis beyond continuity of constants is used.
why it matters
Feeds the R3 headline residual typedResidual_gap5_dynamic_continuum_smearing, whose doc states: the dynamic continuum-smearing residual holds. That residual conjoins (1) continuum reach for every admissible field profile, (2) binding of the continuum law to the concrete dynamic inverse metric on sampled phase points, and (3) the already-banked Hamiltonian inhabitant of the dynamic bracket.
Without this decoy, a referee could claim a single fixed weight already stands in for the whole $q$-family, collapsing dynamic smearing back into the banked fixed-background reach. The theorem blocks that collapse and forces the residual to carry genuine $q$-dependence.
Framework placement: gravity seven-gaps ledger, continuum structure functions tied to dynamic lattice brackets and the HamDyn/eight-tick constructions. It does not close gap-5 constraint recovery, and the Wronskian continuum limit remains the open R4 item.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.