jiCost
plain-language theorem explainer
jiCost defines the zero baseline J-cost for exact integer ratios at r=1 in just intonation. Music theorists ranking 12-TET against JI cite this value to anchor comparisons of average deviation from harmonic purity. The definition is a direct one-line application of stepCost to the unit ratio.
Claim. The JI reference cost is defined as $J(1)$, where $J(r)$ denotes the J-cost of the dimensionless ratio $r$.
background
The TuningSystemJCostRanking module ranks tuning systems by average J-cost, where J-cost on the ratio $r$ = interval_ratio / target_just_ratio measures deviation from pure harmonic relationships. Just intonation achieves average J-cost zero at exact integer multiples, while 12-TET yields a positive per-semitone value near $J(2^{1/12})$ and Bohlen-Pierce is designed for lower cost on odd-harmonic series.
proof idea
One-line definition that applies stepCost to the argument 1.
why it matters
This supplies the zero baseline for jiCost_zero and the comparison ji_beats_tet that shows JI J-cost is strictly less than the 12-TET per-step cost. It is used directly in the TuningRankingCert structure that certifies the ordering. The definition instantiates the structural prediction that exact integer ratios carry J-cost zero, consistent with the Recognition Science J-cost function and the module's claim that JI < BP < 12-TET on average J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.