decoyLapse
plain-language theorem explainer
Defines a two-site lapse that equals 1 at site 0 and 0 at site 1. Gravity and QG residual work cites it as the standard decoy support for residual R0: the naive frozen-partial reading of a dynamic Hamiltonian. The body is a one-line piecewise constant map on Z/2Z.
Claim. The decoy lapse is the map $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ with $N(0)=1$ and $N(j)=0$ for $j\neq 0$. Equivalently, the lapse is supported only at site $0$ on the two-site chain.
background
Module Wave C2 R0+R1 treats the dynamic structure-function bracket on two lattice sites. The configuration lives in a two-site phase space; the lapse $N$ is a real weight on sites indexed by $\mathbb{Z}/2\mathbb{Z}$. The frozen Hamiltonian slot HamW and its frozen configuration partials are the baseline; the dynamic candidate HamDyn plugs a configuration-dependent inverse metric $g(x)$ into that slot.
Residual R0 is the decoy claim that one may reuse the frozen partials after substituting $w:=g(x)$. Residual R1 asks whether the honest Fréchet derivative (including $\partial g/\partial q$) still recovers the target dynamic structure function in the Hamiltonian–Hamiltonian bracket. Continuum and HKT residuals stay open; this module does not flip gap5 constraint recovery.
The decoy lapse is the simplest nontrivial support pattern: unit weight at site 0, zero at site 1. Paired with a fixed decoy phase point, it isolates the uncompensated $\partial g/\partial q$ term in the configuration partial.
proof idea
Pure definition: the map sends $j\in\mathbb{Z}/2\mathbb{Z}$ to $1$ if $j=0$ and to $0$ otherwise. No lemmas. Downstream one-liners decoyLapse_zero and decoyLapse_one discharge the two cases by simp.
why it matters
Supplies the lapse argument for the R0 decoy theorem TypedResidual_naive_dynamic_HamW_decoy_fails: at the decoy phase point, with this lapse and site 0, the honest configuration partial of HamDyn differs from the frozen pderivQ_HamW evaluation by the uncompensated $\partial g/\partial q$ term. Also feeds the evaluation lemmas at 0 and 1, and appears in the honest partial theorem pderivQ_HamDyn when specialized to this $N$.
In the SevenGaps gravity stack this is scaffolding for Wave C2 gap-5 residual bookkeeping: it makes the naive lookalike fail cleanly so the honest dynamic construction (R1) can be stated against a concrete counterexample to the frozen reading. It does not itself close continuum or HKT residuals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.