zmod2_zero_sub_one
plain-language theorem explainer
In the two-element ring $\mathbb{Z}/2\mathbb{Z}$, subtraction yields $0-1=1$. Gravity and HKT bracket proofs cite this when site indices wrap under neighbor shifts on a two-site lattice. The proof is a one-line decidability check.
Claim. In $\mathbb{Z}/2\mathbb{Z}$, the identity $0 - 1 = 1$ holds.
background
The module closes Wave C2 residuals R0 and R1 for a dynamic structure-function bracket on two lattice sites. Sites are indexed by $\mathbb{Z}/2\mathbb{Z}$, so neighbor maps $j \mapsto j\pm 1$ are arithmetic in that ring: the unique nonzero element is both $+1$ and $-1$.
Hamiltonian and momentum observables (HamDyn, MomDyn, and the frozen HamW lookalike) evaluate partials at concrete sites such as $0$. Bracket expansions therefore rewrite terms like $0-1$ when the second site appears as the predecessor of site $0$. The same fact is duplicated in the HKT point-split target module for local use there.
R0 shows the naive frozen-partial decoy fails; R1 shows the honest Fréchet derivative cancels extra $\partial g/\partial q$ terms in the ham–ham bracket. Continuum and full HKT constraint recovery remain open.
proof idea
One-line wrapper: the decide tactic discharges the finite equality in $\mathrm{ZMod},2$ by exhaustive evaluation of the ring operations. No lemmas are invoked beyond decidable equality on a two-element type.
why it matters
Feeds four downstream sites: the R0 decoy failure TypedResidual_naive_dynamic_HamW_decoy_fails (honest vs frozen pderivQ at site $0$), the dynamic momentum–Hamiltonian bracket bracket_MomDyn_HamDyn, the unsplit no-go witness bracket_MomFromProfile_delta0_unsplitNoGo, and the twin copy in HKTPointSplitTarget.
Without $0-1=1$, neighbor shifts in two-site Poisson brackets cannot be normalized, blocking the algebraic cancellation that recovers the target dynamic structure function in R1. It is pure index arithmetic supporting the SevenGaps gravity stack; it does not itself touch gap5 constraint recovery or the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.