distZ_add_int
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish bounds on the rate of variation of d_ℤ.
- Does not extend to non-integer real shifts.
- Does not characterize the function beyond its periodicity.
- Does not connect directly to the phi-ladder or forcing chain.
Lean usage
example (δ : ℝ) (n : ℤ) : distZ (δ + ↑n) = distZ δ := distZ_add_int δ nformal statement (Lean)
52theorem distZ_add_int (δ : ℝ) (n : ℤ) : distZ (δ + ↑n) = distZ δ := by
proof body
Term-mode proof.
53 unfold distZ
54 rw [Int.fract_add_intCast]
55
56/-- d_ℤ is 1-periodic (special case n = 1). -/