jiCost_zero
plain-language theorem explainer
The just intonation reference cost vanishes at the unit ratio. Music theorists ranking tuning systems by average J-cost cite this to anchor the zero baseline for just intonation against 12-TET and Bohlen-Pierce. The proof is a one-line wrapper that applies the step-cost zero theorem at exact match.
Claim. The J-cost of the just intonation reference ratio is identically zero: $J(1) = 0$.
background
In the TuningSystemJCostRanking module, J-cost on a dimensionless ratio r measures deviation from a target just ratio. The just intonation reference cost is defined as the step cost at unit ratio, where step cost is the cost function induced by a multiplicative recognizer. Upstream, the cost of any recognition event is its J-cost, and the cellular automata step applies local rules but here reduces to the exact-match case. The module states the structural prediction that just intonation achieves average J-cost zero while 12-TET yields a positive per-semitone value near 0.00164.
proof idea
The proof is a one-line wrapper that applies the theorem stepCost_zero_at_just, which itself reduces directly to the unit cost property Jcost_unit0 of the J-cost function.
why it matters
This sets the zero baseline for just intonation inside the tuning ranking certificate. It is invoked by the theorem ji_beats_tet that shows just intonation beats 12-TET and by the definition of the tuning ranking certificate. In the Recognition Science framework it supports the predicted ordering just intonation < Bohlen-Pierce < 12-TET on average J-cost, consistent with J-uniqueness forcing zero cost at exact harmonic ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.