distZ
plain-language theorem explainer
distZ supplies the distance to the nearest integer d_Z(δ) for real δ. Researchers working on phase alignment in scale-invariant systems cite it when minimizing the reduced potential J̃. The definition is a direct min of the fractional part and its complement to one, which automatically enforces the interval [0, 1/2] and zero exactly at integers.
Claim. $d_ℤ(δ) := min({δ}, 1 - {δ})$ where {δ} denotes the fractional part of δ.
background
The ReducedPhasePotential module formalizes the reduced phase-mismatch potential J̃_b(δ) = cosh(λ · d_ℤ(δ)) − 1 with λ = ln b, induced by the discrete scaling quotient x ~ b^n x. distZ implements d_ℤ(δ) as the distance to the nearest integer on the circle. This measure is 1-periodic, lies in [0, 1/2], and vanishes precisely when δ is integer, supplying the defect input for the J-cost in phase analyses. The module setting follows the GCIC paper Section IV and draws on Mathlib fractional-part lemmas for its properties.
proof idea
The definition is a direct one-line abbreviation that applies the min operator to Int.fract δ and one minus Int.fract δ.
why it matters
distZ provides the defect distance that underpins the reduced phase potential J̃ in the GCIC paper Section IV. It feeds phase_alignment_minimizes_Jtilde, which shows J̃(λ, 0) is minimal, and the stiffness results theta_coupling_stiffness and phi_coupling_stiffness that deliver the quadratic lower bound (λ d_ℤ(δ))^2 / 2 ≤ J̃(λ, δ). This places the declaration inside the Recognition framework by furnishing the periodic component of the J-cost, supporting the forcing chain steps that fix J-uniqueness and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.