Jtilde_stiffness_lb
plain-language theorem explainer
The reduced phase potential satisfies the quadratic stiffness lower bound (λ d_Z(δ))²/2 ≤ J̃(λ, δ) for real λ and δ. Researchers deriving coupling stiffness in the GCIC framework for scale-invariant ratio-based energies cite this estimate to control small-gradient behavior. The proof is a one-line wrapper that unfolds the definition of J̃ and invokes the quadratic lower bound on cosh via linear arithmetic.
Claim. For real numbers λ and δ, (λ ⋅ d_ℤ(δ))² / 2 ≤ J̃(λ, δ), where J̃(λ, δ) := cosh(λ ⋅ d_ℤ(δ)) − 1 and d_ℤ(δ) is the distance from δ to the nearest integer.
background
The Reduced Phase Potential module formalizes J̃_b(δ) = cosh(lam ⋅ d_ℤ(δ)) − 1 with lam = ln b for the discrete scaling quotient. Here distZ δ is defined as min(fract(δ), 1 − fract(δ)), taking values in [0, 1/2] and vanishing exactly at integers. The upstream quadratic lower bound states cosh x ≥ 1 + x²/2 for all real x, obtained from the Taylor series with non-negative remainder terms or from convexity at the origin.
proof idea
The proof unfolds the definition of Jtilde and applies the linear arithmetic tactic linarith directly to the instance of the cosh quadratic lower bound evaluated at lam * distZ δ.
why it matters
This lower bound supplies the small-gradient stiffness κ = lam²/2 that is applied verbatim in the GCIC derivation theorems phi_coupling_stiffness and theta_coupling_stiffness. It realizes the quadratic approximation near alignment points required for collective cost subadditivity in the J-cost framework. The result closes a basic estimate needed for the GCIC paper Section IV on rigidity and compact phase emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.