zmod1_lapse_diff_zero
plain-language theorem explainer
On the one-site lattice Z/1Z every discrete lapse difference vanishes: for any real-valued lapse N and any site j, N(j+1) − N(j) = 0. Gravity and constraint-algebra workers cite it when showing that Hojman–Kuchař–Teitelboim target fields become vacuous at n = 1. The proof is a one-line rewrite using j+1 = j followed by ring cancellation.
Claim. For every function $N : \mathbb{Z}/1\mathbb{Z} \to \mathbb{R}$ and every site $j \in \mathbb{Z}/1\mathbb{Z}$, the discrete lapse difference vanishes: $N(j+1) - N(j) = 0$.
background
This module supplies Wave C2 groundwork for gap 5 in the gravity constraint-recovery chain. Codex adjudication found that the stated HKT rigidity claim is false on the degenerate one-site lattice: every discrete difference and Wronskian vanishes, so a quartic kinetic density with zero momentum density can satisfy every field of the Hojman–Kuchař–Teitelboim target at $n=1$ while escaping the quadratic pin.
The ambient discrete geometry is the cyclic group $\mathbb{Z}/1\mathbb{Z}$. The sibling lemma $j+1=j$ on this group (via $1=0$ in $\mathbb{Z}/1\mathbb{Z}$) is the only nontrivial arithmetic input. Lapse fields are arbitrary maps $N : \mathbb{Z}/1\mathbb{Z} \to \mathbb{R}$; the discrete difference $N(j+1)-N(j)$ is the finite-difference stand-in for a spatial derivative of the lapse in the Dirac hypersurface-deformation algebra.
The module does not flip the main gap-5 recovery theorem and does not prove any repaired rigidity statement. It only lands the counterexample against the real Fréchet-derivative bracket.
proof idea
Term-mode, two steps. Rewrite the goal with the sibling fact that $j+1=j$ on $\mathbb{Z}/1\mathbb{Z}$. The difference becomes $N(j)-N(j)$, which ring closes as zero. No analysis or differentiability is used.
why it matters
This is the lapse half of the disclosure that every discrete Wronskian and every discrete lapse difference vanishes identically on $\mathbb{Z}/1\mathbb{Z}$. Downstream, one_site_wronskians_vacuous packages it with the companion Wronskian identity, and the inhabitant quarticOneSiteHKT uses that package to fill every real field of HojmanKucharTeitelboimTarget 1 with a quartic Hamiltonian density and zero momentum density.
In the Recognition gravity ledger this forces the terminal claim that Hojman pins general relativity to bind to a repaired statement (a dynamical or $n$-restricted nondegenerate form), with the one-site counterexample disclosed rather than papered over. It does not touch the forcing chain T0–T8, the Recognition Composition Law, or the $\varphi$-ladder mass formula; its role is strictly inside the SevenGaps constraint-algebra audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.