decoyLapse_zero
plain-language theorem explainer
On the two-site lattice Z/2Z, the decoy lapse supported at site 0 evaluates to 1 at that site. Gravity residual proofs cite it when specializing the naive dynamic Hamiltonian at the decoy configuration. The proof is a one-line simp unfolding of the piecewise definition.
Claim. Let $N$ be the two-site index set $\mathbb{Z}/2\mathbb{Z}$. Define the decoy lapse $N_j$ by $N_j = 1$ if $j = 0$ and $N_j = 0$ otherwise. Then $N_0 = 1$.
background
Module Wave C2 R0+R1 treats the dynamic structure-function bracket on two lattice sites. Residual R0 is a decoy: the naive lookalike that plugs a configuration-dependent inverse metric $g(x)$ into the frozen Hamiltonian slot HamW and reuses frozen partials fails, because the configuration partial picks up an uncompensated $\partial g/\partial q$ term.
The decoy lapse is the test lapse supported only at site $0$: it equals $1$ at $j=0$ and $0$ at the other site. Together with a fixed decoy phase-space point, it specializes the naive dynamic Hamiltonian so the residual inequality can be checked by direct evaluation.
Upstream, decoyLapse is exactly that piecewise real-valued function on $\mathbb{Z}/2\mathbb{Z}$. This lemma records its value at the supported site.
proof idea
One-line wrapper: simp [decoyLapse] unfolds the definition and discharges the true branch of the if j = 0 guard, yielding $1$.
why it matters
Feeds the R0 decoy theorem TypedResidual_naive_dynamic_HamW_decoy_fails, which states 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 plan for dynamic structure functions in the gravity sector. It does not flip constraint recovery (gap5_constraint_recovery); continuum and HKT residuals stay open. Within RS gravity scaffolding, the lemma is bookkeeping that makes the decoy specialization fully explicit on the two-site octave fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.