stepCost_zero_at_just
plain-language theorem explainer
stepCost_zero_at_just establishes that the J-cost vanishes exactly at the unit ratio. Music theorists ranking just intonation against equal temperaments cite this zero baseline to anchor the JI prediction. The proof reduces directly to the algebraic identity for Jcost at argument one via a one-line wrapper.
Claim. The J-cost of the unit interval ratio equals zero: $J(1) = 0$, where $J(r) = (r-1)^2 / (2r)$ is the quadratic cost on dimensionless ratios.
background
The TuningSystemJCostRanking module ranks tuning systems by average J-cost on interval ratios, with just intonation predicted to carry zero average cost because its ratios sit at exact integer multiples. stepCost is defined as the J-cost of a supplied ratio r. Upstream Jcost_unit0 states that Jcost(1) = 0 and is proved by direct simplification of the quadratic form J(x) = (x-1)^2 / (2x). The module doc notes that this zero supplies the structural baseline for the ordering JI < BP < 12-TET.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters
This result feeds the jiCost_zero theorem that establishes zero cost for just intonation. It realizes the module's structural prediction of zero average J-cost for JI, consistent with the Recognition Science J-uniqueness at the identity and the zero-cost point in the forcing chain. It supports the broader claim that JI ranks below 12-TET and Bohlen-Pierce on average cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.