distZ_le_half
plain-language theorem explainer
The theorem proves that the distance to the nearest integer d_ℤ(δ) is bounded above by one half for every real δ. Workers on reduced phase potentials in scale-invariant systems cite this when controlling the argument of the cosh in J̃ or deriving stiffness lower bounds. The proof works by case split on the fractional part of δ followed by direct comparison to the two arguments of the min.
Claim. For every real number $δ$, $d_ℤ(δ) ≤ 1/2$, where $d_ℤ(δ) := min({δ}, 1 - {δ})$ and ${δ}$ is the fractional part of $δ$.
background
The Reduced Phase Potential module defines the reduced phase-mismatch potential J̃_b(δ) = cosh(λ · d_ℤ(δ)) − 1 with λ = ln b, where d_ℤ(δ) is the distance to the nearest integer. This distance is constructed explicitly as min(Int.fract δ, 1 − Int.fract δ) and is guaranteed to lie in the closed interval [0, 1/2]. The module supplies the structural lemmas needed for the GCIC paper section on rigidity and compact phase emergence in scale-invariant ratio-based energies.
proof idea
The proof unfolds the definition of distZ, then splits into cases according to whether the fractional part is at most 1/2. The first branch applies the left projection of the min; the second branch uses a linear-arithmetic step to bound the complementary distance and applies the right projection of the min.
why it matters
This bound is the elementary control on the phase distance that feeds every subsequent property of J̃, including non-negativity, periodicity, and the stiffness lower bound κ = λ²/2. It directly supports the phase-coherence arguments in the eight-tick octave and the self-similar scaling fixed point of the Recognition Science forcing chain. No open scaffolding remains for this specific inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.