distZ_periodic
plain-language theorem explainer
The distance to the nearest integer satisfies d_Z(δ + 1) = d_Z(δ) for every real δ. Workers on reduced phase potentials in scale-invariant ratio energies cite this unit case when establishing periodicity of J̃. The proof is a one-line wrapper that casts the unit shift to an integer addition and invokes the general add-integer theorem.
Claim. Let $d_ℤ(δ)$ be the distance from $δ$ to the nearest integer. Then $d_ℤ(δ + 1) = d_ℤ(δ)$ for all real $δ$.
background
In the Reduced Phase Potential module the function d_Z(δ) is defined as min(fract(δ), 1 − fract(δ)), taking values in [0, 1/2] and vanishing exactly at integers. This distance appears inside the reduced phase potential J̃(λ, δ) = cosh(λ · d_Z(δ)) − 1 that models phase mismatch under discrete scaling quotients x ~ b^n x. The module formalizes results from Thapa–Washburn (2026) Section IV on rigidity and compact phase emergence in scale-invariant energies. The upstream theorem distZ_add_int already proves the general statement d_Z(δ + n) = d_Z(δ) for arbitrary integer n.
proof idea
The tactic proof first constructs the auxiliary equality δ + 1 = δ + (1 : ℤ) via push_cast and ring. It rewrites the goal with this equality and finishes by exact application of the general theorem distZ_add_int at n = 1.
why it matters
The unit-periodicity result is the direct input to Jtilde_periodic, which lifts the property to the full reduced phase potential J̃. It supplies the n = 1 special case required by the GCIC paper's treatment of phase potentials and supports downstream structural claims such as Jtilde_zero_iff and stiffness lower bounds. Within the Recognition framework it anchors the periodicity needed for the eight-tick octave and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.