TuningRankingCert
plain-language theorem explainer
TuningRankingCert packages three facts establishing that just intonation has lower J-cost than 12-TET. Music theorists and Recognition Science modelers cite it to rank tuning systems by average recognition cost. The structure is assembled directly from the zero-cost property of integer ratios, the positivity of the 12-TET step cost, and the comparison that just intonation beats 12-TET.
Claim. A certificate that the J-cost of the just-intonation reference ratio is zero, the J-cost of the 12-TET semitone ratio $2^{1/12}$ is positive, and the just-intonation J-cost is strictly less than the 12-TET step cost.
background
The Tuning System J-Cost Ranking module derives from the cost function in MultiplicativeRecognizerL4, where cost is the derived cost of the comparator on positive ratios, and from ObserverForcing, where the cost of a recognition event is its J-cost. stepCost applies this J-cost to an interval ratio r, jiCost is stepCost at the unit ratio 1, and tetStep is the 12-TET ratio 2 to the power of 1/12. The module doc states the structural prediction that just intonation has average J-cost zero while 12-TET has positive average J-cost per semitone, with the certificate capturing the key comparison.
proof idea
This is a structure definition with no proof body. Its fields are filled by the zero property of jiCost at the unit ratio, the positivity result for the 12-TET step cost, and the ji_beats_tet theorem that supplies the strict inequality.
why it matters
The certificate is used to define the concrete tuningRankingCert instance in the same module. It supports the module's claim of JI ranking below 12-TET on J-cost, extending the J-cost framework from the foundation modules. This aligns with the Recognition Science cost non-negativity and the prediction of zero cost at exact harmonic ratios, while leaving the Bohlen-Pierce comparison as a separate structural claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.