stepCost
plain-language theorem explainer
stepCost defines the per-step J-cost for an interval ratio r. Music theorists ranking just intonation against 12-TET cite it to quantify harmonic deviation per step. The definition is a direct one-line wrapper around the Jcost function from the RSNative cost module.
Claim. For an interval ratio $r$, the step cost function is defined by $s(r) := J(r)$, where $J$ is the J-cost measuring deviation from pure harmonics.
background
The module ranks tuning systems by average J-cost across generated intervals. J-cost on the dimensionless ratio r measures deviation from pure harmonic relationships, with just intonation at zero average and 12-TET positive per semitone. The upstream result defines Cost as Quantity CostUnit in the RSNative core, supplying the Jcost function.
proof idea
This declaration is a one-line wrapper that applies the Jcost function from the Cost module to the input ratio r.
why it matters
stepCost supplies the basic cost measure used to prove just intonation beats 12-TET in ji_beats_tet and to build the TuningRankingCert structure. It applies J-uniqueness from the Recognition Science forcing chain (T5) to music intervals. The module doc states the structural prediction JI < BP < 12-TET on average J-cost values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.