zmod2_one_sub_one
plain-language theorem explainer
In the ring of integers mod 2, the difference 1 − 1 equals 0. Gravity and discrete-phase-space arguments that index lattice sites by Z/2Z cite this when simplifying source/target shifts and smeared momentum brackets. The proof is a one-line kernel decision procedure on a finite ring.
Claim. In $\mathbb{Z}/2\mathbb{Z}$, one has $1 - 1 = 0$.
background
The ambient module repairs the Hojman–Kuchař–Teitelboim (HKT) dynamic target after an adjudication that the unsplit momentum–Hamiltonian bracket is uninhabitable for honest nearest-neighbor local momentum profiles against a frozen quadratic Hamiltonian. Phase-space sites and smearing weights live on $\mathbb{Z}/2\mathbb{Z}$ (two cells), so elementary arithmetic identities on that ring appear throughout the bracket expansions.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1 = 1$, which collapses certain generator symmetries and forces the repaired target to use smeared point-split momentum densities rather than a vacuous $D_{\mathrm{gen}}^{\mathrm{sym}}$ sketch. The present fact is the plain subtraction identity $1-1=0$ in that ring; sibling facts cover $0+1$, $1+1$, and $0-1$.
No Recognition-Science forcing landmark (T5–T8, RCL, $\varphi$-ladder) is at stake here: the lemma is pure finite-ring bookkeeping for the $n=2$ discrete gravity model.
proof idea
One-line proof by the decidability kernel on the finite ring $\mathbb{Z}/2\mathbb{Z}$: both sides evaluate to the same concrete residue, so decide closes the goal. No external lemmas are invoked.
why it matters
Feeds two load-bearing bracket identities in the same module: the point-split dynamical Poisson bracket between smeared momentum and the dynamical Hamiltonian, and the no-go evaluation of the unsplit momentum-from-profile bracket at the $\delta_0$ witness. Those theorems expand source/target advection terms whose site indices are elements of $\mathbb{Z}/2\mathbb{Z}$; reducing $1-1$ to $0$ clears residual shift coefficients.
In the Wave C2 R5 repair narrative, the unsplit Dyn target remains as a falsification-adjacent record, while the strong point-split class carries the honest $n=2$ API. This lemma is scaffolding arithmetic only: it does not flip any ledger flag, prove rigidity, or close the open Prop that the unsplit mom–ham obstruction persists against campaign HamDyn. It simply keeps the discrete index algebra honest so the repaired brackets typecheck and compute.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.