decoyPhasePoint
plain-language theorem explainer
Explicit two-site phase-space witness with unit configuration and unit momentum at lattice site 0 and zeros at site 1. Used as the counterexample point that kills the naive frozen-partial reading of a dynamic Hamiltonian. Downstream R0 residual and honest configuration-partial theorems evaluate at this point. The body is a direct pair of piecewise constant maps on ZMod 2.
Claim. Let the two-site phase space be pairs $(q,\pi)$ of real functions on $\mathbb{Z}/2\mathbb{Z}$. Define the decoy point by $q(0)=1$, $q(1)=0$ and $\pi(0)=1$, $\pi(1)=0$. At this point both the discrete gradient of $q$ and $\partial g/\partial q$ are nonzero at site $0$.
background
The ambient setting is Wave C2 on the dynamic structure-function bracket for a two-site periodic lattice. The module closes typed residuals R0 and R1 from the QG gap-5 residual DAG: R0 shows that a naive lookalike Hamiltonian (plug $g x$ into a frozen $HamW$ slot and reuse frozen partials) fails; R1 shows that the honestly differentiated candidate still recovers the target dynamic structure function in the Hamiltonian–Hamiltonian bracket.
Upstream, phase space on $n$ sites is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$, so each field is determined by its values at sites $0$ and $1$. The decoy point concentrates unit $q$ and unit $\pi$ at site $0$, leaving site $1$ at zero, which forces a nonzero discrete gradient and a nonzero $\partial g/\partial q$ contribution exactly where the residual is tested.
proof idea
Definitional construction, not a proof. The value is the ordered pair of maps on $\mathbb{Z}/2\mathbb{Z}$ that send $0$ to $1$ and $1$ to $0$ for both configuration and momentum. Downstream private lemmas unfold the definition by simp to read $q(0)=1$ and $q(1)=0$. No tactics beyond that unfolding are required at the definition site itself.
why it matters
This witness is the concrete evaluation point for residual R0: the theorem that the naive dynamic $HamW$ decoy fails shows that the honest configuration partial of the dynamic Hamiltonian at this point with the decoy lapse differs from the frozen partial evaluated at $w:=g x$ by an uncompensated $\partial g/\partial q$ term (honest value $3$ at site $0$). It is also the sample point underlying the honest partial formula for the dynamic Hamiltonian and the two site-value lemmas that feed those calculations.
In the broader Seven Gaps gravity stack this is scaffolding for dynamic structure-function recovery on the lattice, not a flip of gap5_constraint_recovery. Continuum and HKT residuals stay open. The construction is local to $n=2$ Wave C2 bookkeeping rather than a T0–T8 forcing step, but it is the explicit counterexample that makes the R0 failure checkable rather than schematic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.