Periodic1
plain-language theorem explainer
A real function is 1-periodic when shifting its argument by 1 leaves values unchanged, i.e. it descends to the circle of length 1. Gravity continuum-limit arguments cite this as the standing hypothesis on lapses, configuration, and momentum so that wrap-around lattice samples match ordinary mesh samples. The body is the standard universal quantification; a one-line corollary recovers f(1)=f(0).
Claim. A function $f:\mathbb{R}\to\mathbb{R}$ is 1-periodic if $f(t+1)=f(t)$ for every real $t$. Equivalently, $f$ is constant on cosets of $\mathbb{Z}$ and defines a continuous function on the circle $\mathbb{R}/\mathbb{Z}$ of circumference 1.
background
The module repairs the Wave C2 R4 ledger terminal that binds the freestanding Riemann shape sampledDynamicBracketSum to the genuine lattice bracket of dynamic Hamiltonians after periodic wrap treatment, then lands the continuum Dirac-density limit for 1-periodic $C^1$ data.
On $\mathrm{ZMod},n$, site $n-1$ has successor $0$. The non-periodic mesh therefore samples the last cell at $(k+1)/n=1$, while the periodic mesh samples $0$. For fields obeying $f(t+1)=f(t)$ those two sample values coincide, so the periodic and ordinary sampled dynamic brackets agree.
Periodic1 is the Prop packaging that identity. Downstream continuum statements impose it on the two lapses $N,M$, the configuration $q$, and the momentum $p$, together with ContDiff-1 (or continuous-on-$[0,1]$) regularity.
proof idea
Definitional: the body is exactly $\forall t:\mathbb{R},, f(t+1)=f(t)$. No lemmas are invoked. The companion one-liner Periodic1.eval_one instantiates at $t=0$ and simplifies to $f(1)=f(0)$, which is the endpoint identification used when comparing wrap and non-wrap meshes.
why it matters
This is the periodicity hypothesis that makes the wrap treatment honest. It appears as a named assumption in periodicSampled_eq_sampled_of_periodic (wrap mesh equals non-periodic mesh), in scaled_continuumLatticeBracket_eq_scaled_sampled, and in both ledger terminals dirac_algebra_continuum_limit and dirac_algebra_continuum_limit_hamDynN. The Gap-5 residual DAG records the same statement as TypedResidual_gap5_dirac_algebra_continuum_limit.
Without 1-periodicity the last-cell samples at $1$ and $0$ can differ, so the freestanding Riemann shape would not equal the genuine lattice bracket and the scaled continuum limit to the Dirac density would not go through. In the Recognition gravity stack this closes the continuum-binding step that feeds the Dirac-algebra side of the seven-gap residual ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.