Jtilde_nonneg
plain-language theorem explainer
The reduced phase potential J̃(λ, δ) = cosh(λ d_ℤ(δ)) − 1 is nonnegative for all real λ and δ. Workers on discrete scaling quotients in the GCIC derivation cite this to bound the energy from below. The proof unfolds the definition and invokes the elementary inequality cosh(x) ≥ 1. It supplies the base case for sign properties used in coupling and alignment arguments.
Claim. $0 ≤ cosh(λ ⋅ d_ℤ(δ)) − 1$ for all real λ and δ, where d_ℤ(δ) denotes the distance from δ to the nearest integer.
background
The module formalizes the reduced phase-mismatch potential induced by the discrete scaling quotient x ~ b^n x. The potential is defined as J̃(λ, δ) = cosh(λ d_ℤ(δ)) − 1 with λ = ln b and d_ℤ(δ) = min(fract(δ), 1 − fract(δ)), which lies in [0, 1/2] and vanishes exactly at integers. This sits in the GCIC paper Section IV on rigidity and compact phase emergence in scale-invariant ratio-based energies.
proof idea
Unfolds the definition of the reduced phase potential and applies linear arithmetic to the inequality cosh(x) ≥ 1 evaluated at x = λ times the distance to the nearest integer.
why it matters
This result is used by neg_Jtilde_coupling_nonpos to show the negative potential is nonpositive and by phase_alignment_minimizes_Jtilde to confirm alignment minimizes the potential. It fills the structural property J̃ ≥ 0 in the GCIC derivation, supporting the phase alignment that minimizes the reduced potential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.