frequencyRatioCost
plain-language theorem explainer
frequencyRatioCost defines the cost of any positive frequency ratio r as its J-cost J(r). Researchers modeling resonance ladders or minimal-cost harmonics in Recognition Science cite this when bridging frequencies to the cost framework. It supplies the base map for Gap B closure in the φ-ladder. The implementation is a direct one-line abbreviation of the imported Jcost function.
Claim. For a positive real number $r$, the frequency ratio cost is defined by $J(r)$, where $J(r) = ½(r + r^{-1}) - 1$.
background
The Cost.FrequencyLadder module supplies the φ-ladder frequency bridge under Gap B closure. The J-cost function J(r) = ½(r + r⁻¹) − 1 evaluates the cost of any positive ratio r; φ is the unique positive fixed point of the self-similar equation r = 1 + 1/r. Upstream, ObserverForcing.cost states that the cost of a recognition event is Jcost of its state, while MultiplicativeRecognizerL4.cost derives the cost from the comparator on positive ratios. PhiForcingDerived.of supplies the structure of J-cost.
proof idea
This is a one-line wrapper that applies the Jcost function directly to the input ratio r.
why it matters
This definition supports the claim that φ is the minimal-cost non-trivial ratio, as stated in the module documentation. It is used by frequencyRatioCost_nonneg (J-cost non-negative for positive ratios) and frequencyRatioCost_unit (zero cost at unit ratio). In the framework it connects to T5 J-uniqueness and T6 φ as self-similar fixed point, justifying the first φ-harmonic as the minimal-cost resonance above a given frequency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.