tetStep_jcost_pos
plain-language theorem explainer
The J-cost of the 12-TET semitone step is strictly positive. Music theorists and Recognition Science researchers cite it when ranking tuning systems by deviation from just intonation. The proof applies the general J-cost positivity lemma after verifying the step ratio is positive and unequal to one via the band condition.
Claim. Let tetStep denote the frequency ratio of one semitone in twelve-tone equal temperament. Then the associated J-cost satisfies $0 < stepCost(tetStep)$.
background
The module ranks tuning systems by average J-cost on dimensionless ratios, where J-cost measures deviation from pure harmonic relationships. Just intonation achieves zero average J-cost at exact multiples, 12-TET incurs positive cost per semitone, and Bohlen-Pierce minimizes cost on odd-harmonic series, yielding the predicted order JI < BP < 12-TET.
proof idea
The proof applies the lemma Jcost_pos_of_ne_one to tetStep. The hypothesis 0 < tetStep follows from tetStep_band.1 by linarith, while tetStep ≠ 1 is obtained from the same band fact by linarith.
why it matters
This result supplies the positive 12-TET cost used by ji_beats_tet to conclude JI J-cost < 12-TET J-cost and by tuningRankingCert to package the full ranking certificate. It realizes the positive-cost side of the module's structural prediction and connects to the general J-cost positivity from the multiplicative recognizer and observer forcing definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.