gcic_kappa_pos
plain-language theorem explainer
The theorem shows that the stiffness constant κ in the reduced phase potential is strictly positive. Workers on phase rigidity for scale-invariant ratio energies would cite it to anchor the quadratic lower bound used in energy minimization arguments. The proof is a direct term-mode reduction that applies positivity of the squared logarithm of the golden ratio together with a numerical denominator check.
Claim. $0 < κ$ where $κ = λ²/2$, $λ = ln φ$, and $φ$ denotes the golden ratio (the unique positive root of $x² - x - 1 = 0$).
background
The module defines the reduced phase potential induced by the discrete scaling quotient: $J̃(δ) = cosh(λ · d_ℤ(δ)) - 1$ with $λ = ln b$ and $d_ℤ(δ)$ the distance to the nearest integer. The constant κ is the small-gradient stiffness lower bound obtained from the quadratic term in the Taylor expansion of $J̃$ near zero. The upstream lemma one_lt_phi supplies $1 < φ$, which forces $λ > 0$ and thereby guarantees the positivity of the squared logarithm that appears in κ.
proof idea
The proof is a one-line wrapper. It unfolds the definition of gcic_kappa, then applies the library lemma div_pos to the numerator (log φ)² (positive by log_pos and one_lt_phi) and a denominator shown positive by norm_num.
why it matters
The result supplies the strict positivity of the quadratic coefficient required for the phase-rigidity statement (Result 3) in the GCIC paper, Section IV. It sits inside the eight-tick octave structure and the self-similar fixed point φ of the forcing chain, ensuring the reduced phase energy is locally convex about constant fields. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.