frequencyRatioCost_unit
plain-language theorem explainer
The J-cost of a unit frequency ratio is zero, meaning equal frequencies incur no recognition cost. Researchers working on the phi-ladder frequency bridge would cite this as the base case when establishing zero-cost resonances before stepping to the minimal-cost phi-harmonic. The proof is a one-line wrapper that unfolds frequencyRatioCost to Jcost and applies simp to reduce the expression at r=1.
Claim. Let $J(r) = ½(r + r^{-1}) - 1$ denote the J-cost of a positive ratio $r$. Then $J(1) = 0$.
background
The module sets up the φ-ladder frequency bridge for gap B closure. The J-cost is defined by J(r) = ½(r + r⁻¹) − 1, which evaluates the cost of any positive ratio r; the golden ratio φ is the unique positive fixed point of the self-similar recursion r = 1 + 1/r. frequencyRatioCost is the sibling definition frequencyRatioCost(r) := Jcost r, where Jcost is the cost induced by a multiplicative recognizer on positive ratios. Upstream results establish that the cost of any recognition event is its J-cost and that this cost is non-negative.
proof idea
The proof is a one-line wrapper: it unfolds frequencyRatioCost to Jcost and applies simp, which reduces J(1) directly to zero by the algebraic definition of J.
why it matters
This base fact anchors the zero-cost point on the phi-ladder before the minimal-cost non-trivial ratio φ is identified. It supports the module's claim that the first φ-harmonic is the minimal-cost resonance above a given frequency, feeding the step that defines f_phi_rung1 in BodyCosmosResonance. In the Recognition framework it supplies the unit case for T5 J-uniqueness and the non-negativity of costs used in the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.