majorThird
plain-language theorem explainer
The major third in twelve-tone equal temperament is defined as the fourth semitone step, equal to 2 raised to the power 1/3. Music theorists building consonance hierarchies and interval cost comparisons cite this definition when contrasting equal-tempered intervals against just-intonation ratios such as 5/4. The definition is introduced directly as a real-number power expression with no lemmas or reductions required.
Claim. The major third interval in twelve-tone equal temperament is given by $2^{4/12}$.
background
The module constructs the Western 12-tone equal-tempered scale from the golden ratio φ by optimizing consonance and circle-of-fifths closure. Twelve semitones per octave arise as the integer nearest φ^5/2, and the major third occupies four of those semitones. Upstream definitions in HarmonicModes and Valence both supply the just major third as the rational 5/4 for direct numerical comparison.
proof idea
This is a direct definition that equates the major third to the exponential 2^(4/12). No lemmas are invoked and no tactics are applied; the expression is introduced as a primitive real number.
why it matters
The definition supplies the equal-tempered major third required by the consonance_hierarchy theorem and the third_quality comparison that establishes 2^(4/12) exceeds the just ratio 5/4. It occupies the slot for the 4-semitone interval inside the φ-derived 12-tone structure, where the octave, fifth, and third ratios are all generated from the same semitone base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.