zmod2_zero_sub_one
plain-language theorem explainer
In the two-element ring $\mathbb{Z}/2\mathbb{Z}$, zero minus one equals one. Gravity lemmas on the two-site lattice cite this when rewriting neighbor shifts $j-1$ as $j+1$. The proof is a one-line finite decision on the ring.
Claim. In the ring $\mathbb{Z}/2\mathbb{Z}$, $0 - 1 = 1$.
background
The module repairs the Hojman–Kuchař–Teitelboim dynamic target by point-splitting momentum against a frozen quadratic Hamiltonian on a two-site lattice indexed by $\mathbb{Z}/2\mathbb{Z}$. Nearest-neighbor advection therefore only ever shifts a site by $\pm 1$.
In characteristic two the additive inverse of $1$ is $1$ itself, so $0-1=1$ and $j-1=j+1$ for every site $j$. The module doc records the consequence: the generator $D_{\mathrm{gen}}^{\mathrm{sym}}$ vanishes identically as a functional on this lattice, and the unsplit $\mathrm{mom_ham}$ field is uninhabitable for smooth nearest-neighbor profiles (the open Prop against $\mathrm{HamDyn}$ remains separate).
An identical private lemma already lives in DynamicStructureBracket; this copy is local to the point-split target file.
proof idea
One-line wrapper: the decide tactic enumerates the finite carrier of $\mathbb{Z}/2\mathbb{Z}$ and checks the single equality $0-1=1$. No lemmas are invoked.
why it matters
The identity is the arithmetic engine behind the $n=2$ API adaptation stated in the module doc: because $-1=1$ on $\mathbb{Z}/2\mathbb{Z}$, neighbor differences collapse and the adjudicated $D_{\mathrm{gen}}^{\mathrm{sym}}$ sketch is definitionally empty at HamDyn size. Downstream, bracket_MomDyn_HamDyn expands the Poisson bracket of dynamic momentum against dynamic Hamiltonian into smeared source/target advection densities, and bracket_MomFromProfile_delta0_unsplitNoGo evaluates the unsplit no-go witness at $w=\delta_0$. Both rewrites need $0-1=1$ when shifting the zero site. The same fact also appears in the R0 decoy residual that separates honest $\partial_q$ from the frozen HamW reading. No rigidity theorem and no ledger flag are claimed here; the lemma only keeps the two-site algebra honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.