justMajorThird
The just major third frequency ratio is defined as the real number 5/4. Music theorists and scale designers comparing just intonation to 12-tone equal temperament cite this constant when quantifying interval purity against tempered approximations. The definition is a direct constant assignment with no lemmas or computation required.
claimThe just major third frequency ratio is given by $5/4$.
background
The Aesthetics.MusicalScale module derives the Western 12-tone scale from the golden ratio φ by optimizing consonance via simple ratios and closure of the circle of fifths, noting that 12 semitones emerge from φ^5 scaling and that the major third (four semitones) approximates 5/4. The just major third is the pure interval 5/4 = 1.25 used as a benchmark against the equal-tempered value 2^(1/3) ≈ 1.26. Upstream, the Octave structure supplies the abstract state space, strain functional (J-cost), and observation channels for modeling frequency ratios without embedding physical constants such as φ or the eight-tick period.
proof idea
This is a direct definition that assigns the rational constant 5/4 to justMajorThird. No lemmas or tactics are invoked; the value is hardcoded as the textbook just major third ratio.
why it matters in Recognition Science
This definition supplies the pure reference ratio consumed by the downstream theorem third_quality, which proves the equal-tempered major third exceeds 5/4. It fills the module's prediction that the major third approximates 5/4 within the φ-derived 12-tone scale, supporting the Recognition Science claim that 12 emerges from φ^5 / log(3/2) and circle-of-fifths closure after 12 steps.
scope and limits
- Does not derive 5/4 from the golden ratio or the Octave strain functional.
- Does not claim optimality of 5/4 outside Western just intonation.
- Does not address closure properties or comma calculations for other intervals.
- Does not extend to microtonal or non-12-tone scales.
Lean usage
example : justMajorThird = 5 / 4 := rflformal statement (Lean)
58def justMajorThird : ℝ := 5 / 4
proof body
Definition body.
59
60/-- Octave ratio: 2. -/