distZ_nonneg
plain-language theorem explainer
The non-negativity of the distance-to-nearest-integer function holds for every real argument. Workers on reduced phase potentials in the GCIC framework cite this to guarantee that the associated J-tilde potential remains non-negative. The short proof unfolds the min definition and invokes non-negativity of the fractional part together with a linear-arithmetic bound on its complement.
Claim. For every real number $δ$, the distance to the nearest integer satisfies $0 ≤ d_ℤ(δ)$, where $d_ℤ(δ) = min({δ}, 1 - {δ})$ and ${δ}$ denotes the fractional part of $δ$.
background
In the Reduced Phase Potential module the function distZ implements the distance to the nearest integer $d_ℤ(δ) = min(fract(δ), 1 - fract(δ))$. This quantity lies in $[0, 1/2]$ and vanishes exactly when $δ$ is an integer. The surrounding development formalizes the reduced phase-mismatch potential $J̃_b(δ) = cosh(λ · d_ℤ(δ)) - 1$ with $λ = ln b$, drawn from the GCIC paper Section IV.
proof idea
The proof is a one-line wrapper that unfolds the definition of distZ and applies le_min to the pair consisting of Int.fract_nonneg δ together with the linear-arithmetic consequence of Int.fract_lt_one δ.
why it matters
This result supplies the non-negativity foundation for the reduced phase potential Jtilde in the GCIC paper. It directly supports the sibling theorem Jtilde_nonneg and the structural properties needed for stiffness bounds. Within Recognition Science it anchors the phase-mismatch term that appears in the forcing chain leading to the eight-tick octave and three-dimensional emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.