pith. machine review for the scientific record. sign in
def definition def or abbrev high

majorThird

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  55def majorThird : ℝ := 2 ^ (4 / 12 : ℝ)

proof body

Definition body.

  56
  57/-- Just major third: 5/4 = 1.25. -/

used by (18)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.