distZ_eq_zero_iff
plain-language theorem explainer
The theorem states that the distance-to-nearest-integer function vanishes exactly when its real argument is an integer. Researchers analyzing reduced phase potentials in discrete scaling quotients cite this to locate zero-energy states in the GCIC framework. The proof unfolds the min definition of distZ, splits the biconditional, and resolves the forward direction via a case split on the fractional part relative to its complement to one.
Claim. $d_ℤ(δ) = 0 ↔ ∃ n ∈ ℤ, δ = n$
background
The module develops the reduced phase potential J̃(lam, δ) = cosh(lam · d_ℤ(δ)) − 1 that arises from the discrete scaling quotient x ~ b^n x, with lam = ln b. Here d_ℤ(δ) is the distance to the nearest integer, defined as min_{n∈ℤ} |δ − n|. The present result supplies the zero set of this distance function, which is required to characterize when J̃ itself vanishes. The surrounding development sits in the GCIC paper (Thapa–Washburn 2026, Sec. IV) and draws on upstream structures for J-cost, eight-tick phases, and phi-forcing derivations that motivate the discrete quotient.
proof idea
The tactic proof first unfolds the definition of distZ. It then constructs both directions of the biconditional. The forward direction invokes Int.fract_nonneg and Int.fract_lt_one, performs a case split on whether Int.fract δ ≤ 1 − Int.fract δ, rewrites the min accordingly, and concludes that the fractional part must be zero; the integer is recovered via floor. The reverse direction substitutes the integer, applies Int.fract_intCast, and simplifies.
why it matters
This zero characterization is invoked directly by the downstream theorem Jtilde_zero_iff to conclude that J̃(lam, δ) = 0 precisely when δ is integer (for lam ≠ 0). It supplies the structural fact needed for the zero-energy condition in the reduced phase potential of the GCIC paper. Within the Recognition framework it supports phase-coherence analysis under the eight-tick octave and the self-similar forcing chain that forces discrete quotients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.