decoyLapse_one
plain-language theorem explainer
On the two-site lattice Z/2Z the decoy lapse (supported only at site 0) evaluates to zero at site 1. Cited when assembling the R0 decoy residual that kills the naive frozen-partial Hamiltonian. Proof is a one-line simp unfolding of the piecewise definition.
Claim. Let $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ be the decoy lapse with $N(0)=1$ and $N(j)=0$ for $j\neq 0$. Then $N(1)=0$.
background
Module Wave C2 R0+R1 treats the dynamic structure-function bracket on two lattice sites. The decoy lapse is the indicator of site 0: it equals 1 at $j=0$ and 0 at every other residue class mod 2. It is the test lapse used to probe whether a candidate Hamiltonian can reuse frozen partials from the static HamW construction.
R0 asserts that the naive lookalike (plug $g x$ into the frozen slot and keep frozen configuration partials) fails: the honest $\partial/\partial q$ picks up an uncompensated $\partial g/\partial q$ term. Evaluating that residual needs the numerical values of the decoy lapse at both sites.
proof idea
One-line wrapper: simp [decoyLapse] unfolds the piecewise definition. Since $1\neq 0$ in $\mathbb{Z}/2\mathbb{Z}$, the else-branch returns $0$.
why it matters
Feeds the R0 decoy theorem TypedResidual_naive_dynamic_HamW_decoy_fails, which shows that at the decoy phase point, with this lapse and site 0, the honest configuration partial of the dynamic Hamiltonian differs from the frozen pderivQ_HamW evaluation by the uncompensated $\partial g/\partial q$ term. That residual is the first typed gap closed in the Wave C2 draft; continuum and HKT residuals stay open, and gap5_constraint_recovery is not flipped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.