distZ_le_half
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend the bound to complex or vector-valued arguments.
- Does not supply derivative or gradient estimates.
- Does not characterize equality cases beyond integer δ.
- Does not address multidimensional lattice distances.
formal statement (Lean)
44theorem distZ_le_half (δ : ℝ) : distZ δ ≤ 1 / 2 := by
proof body
Tactic-mode proof.
45 unfold distZ
46 rcases le_or_gt (Int.fract δ) (1 / 2) with h | h
47 · exact min_le_left _ _ |>.trans h
48 · have : 1 - Int.fract δ ≤ 1 / 2 := by linarith
49 exact min_le_right _ _ |>.trans this
50
51/-- d_ℤ is 1-periodic: d_ℤ(δ + n) = d_ℤ(δ) for integer n. -/