distZ_add_int
plain-language theorem explainer
The declaration proves that the distance-to-nearest-integer function d_ℤ satisfies d_ℤ(δ + n) = d_ℤ(δ) for any real δ and integer n. Workers on reduced phase potentials in the GCIC framework cite this to establish periodicity of J̃. The proof is a direct algebraic reduction that unfolds the definition of distZ and invokes the integer-addition rule for the fractional part.
Claim. Let $d_ℤ(δ) := min({δ}, 1 - {δ})$ denote the distance to the nearest integer, where {·} is the fractional part. Then $d_ℤ(δ + n) = d_ℤ(δ)$ for every real number δ and every integer n.
background
In the Reduced Phase Potential module the function J̃(λ, δ) = cosh(λ · d_ℤ(δ)) − 1 captures phase mismatch under discrete scaling. The auxiliary distZ is defined by distZ δ := min (Int.fract δ) (1 - Int.fract δ), which lies in [0, 1/2] and vanishes precisely at integers. This periodicity lemma is a prerequisite for showing that J̃ itself is 1-periodic, as used in the structural properties of the GCIC paper (Thapa–Washburn 2026, Sec. IV). The upstream distZ definition supplies the concrete expression that the proof manipulates.
proof idea
The proof is a one-line wrapper. It unfolds the definition of distZ and rewrites using the library lemma Int.fract_add_intCast, which states that the fractional part of δ + n equals the fractional part of δ.
why it matters
This result supplies the general integer-shift invariance needed by distZ_periodic (the n=1 case) and by Jtilde_add_int, which lifts the periodicity to the full reduced potential J̃. It closes a basic structural property in the GCIC reduced-phase analysis, ensuring that the potential depends only on the fractional part of the phase mismatch. Within the Recognition Science setting it supports the construction of scale-invariant energies that are insensitive to integer lattice shifts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.