tetStep
plain-language theorem explainer
Defines the real number 2^(1/12) as the semitone frequency ratio in twelve-tone equal temperament. Music theorists ranking tuning systems by average J-cost cite this constant to quantify per-semitone deviation from just intervals in 12-TET. The definition is a direct real-arithmetic abbreviation that supplies the base value for immediate unfolding in bounds and positivity arguments.
Claim. Define the twelve-tone equal temperament step size by the real number $r = 2^{1/12}$. This ratio serves as the base for the quadratic J-cost form $J(r) = (r-1)^2/(2r)$ when comparing average deviation costs against just intonation.
background
The TuningSystemJCostRanking module ranks tuning systems by average J-cost on the dimensionless ratio r measuring deviation from pure harmonic relationships. J-cost uses the quadratic form J(r) = (r-1)^2/(2r). The module contrasts just intonation (average J-cost zero at exact integer multiples), 12-TET (approximately J(2^(1/12)) per semitone), and Bohlen-Pierce (J(3^(1/13)) per step), with the structural prediction JI < BP < 12-TET on average J-cost values.
proof idea
The declaration is a direct definition that assigns the real exponentiation 2^(1/12) verbatim. No lemmas or tactics appear in the body; the constant is introduced for unfolding in downstream results such as tetStep_band and tetStep_jcost_pos.
why it matters
This definition anchors the 12-TET side of the J-cost comparison. It is referenced by ji_beats_tet to conclude just intonation has strictly lower J-cost than 12-TET, by tetStep_jcost_pos to establish positivity, and by the TuningRankingCert structure. The placement supports the module's ordering prediction and aligns with Recognition Science use of J-cost as a deviation measure, consistent with the Recognition Composition Law and the eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.