gapCost_nonneg
plain-language theorem explainer
Gap costs on the φ-ladder are non-negative for every natural number k. Partition theorists and Recognition Science modelers cite the result when confirming that admissible rung occupations carry no negative energy penalties. The argument reduces immediately to the AM-GM bound on the J-cost function applied to φ^k > 0.
Claim. For every natural number $k$, $0 ≤ gapCost(k)$, where $gapCost(k)$ denotes the J-cost of the positive real number $φ^k$.
background
The φ-ladder consists of positions at powers φ^n for n ∈ ℤ, with J-cost defined by J(x) = (x + x^{-1})/2 − 1 for x > 0. The module shows that adjacent occupations (ratio φ) produce positive J-cost and therefore collapse, while gap-2 occupations achieve the minimal stable configuration. Jcost_nonneg states that J(x) ≥ 0 for all x > 0 by the AM-GM inequality, rewritten as a square-over-positive-denominator form.
proof idea
The proof is the one-line term exact Jcost_nonneg (pow_pos phi_pos k), which feeds the positivity of φ^k directly into the upstream non-negativity lemma for J-cost.
why it matters
The result supplies the non-negativity anchor for the φ-ladder stability argument that re-derives the Rogers-Ramanujan “differ by ≥ 2” rule from J-cost minimality. It sits inside the chain that forces φ as the self-similar fixed point and eight-tick octave structure. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.