frequencyRatioCost_nonneg
plain-language theorem explainer
The theorem shows that the J-cost assigned to any positive frequency ratio is non-negative. Workers on the φ-ladder in Recognition Science cite it when bounding resonance costs before selecting the golden ratio as the minimal non-trivial ratio. The proof is a one-line wrapper that applies the core Jcost non-negativity lemma directly to the positivity hypothesis.
Claim. For every real number $r > 0$, $0 ≤ J(r)$, where $J(r) = ½(r + r^{-1}) - 1$ is the J-cost of the frequency ratio $r$.
background
The module Cost.FrequencyLadder defines the J-cost of a frequency ratio $r = f_2/f_1$ as $J(r) = ½(r + r^{-1}) - 1$. This function evaluates the cost of any positive ratio and is central to identifying φ as the unique positive fixed point of the self-similar equation $r^2 = r + 1$. The module proves that φ is the minimal-cost non-trivial ratio, justifying the first φ-harmonic in downstream resonance constructions.
proof idea
The proof is a one-line wrapper that applies the upstream lemma Jcost_nonneg (from JcostCore) to the hypothesis $0 < r$. That lemma itself follows from rewriting Jcost as a square over a positive denominator and invoking non-negativity of squares.
why it matters
This result supplies the non-negativity step required before the module can isolate φ as the minimal-cost self-similar ratio. It supports the claim in the module doc that the first φ-harmonic is the minimal-cost resonance above a given frequency, feeding the φ-ladder construction used in BodyCosmosResonance. Within the framework it reinforces T6 (phi forced as self-similar fixed point) and the overall cost non-negativity that precedes the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.