justMajorThird
plain-language theorem explainer
The just major third frequency ratio is defined as the real number 5/4. Scale theorists and acousticians cite this as the reference value in just intonation for the major third interval. The definition is a direct constant assignment with no computation or lemmas applied.
Claim. The just major third frequency ratio equals $5/4$.
background
The module derives 12-tone scales from φ by optimizing consonance via simple ratios and closure under fifths. The major third (four semitones) is noted to approximate 2^(4/12) ≈ 1.26, close to the just value 5/4. Upstream, the Octave structure supplies an abstract model: 'An octave: a state space with strain and observation channels. This is the abstract structure; no physical constants (φ, 8-tick) here. Those are hypotheses layered on top.' The strain functional corresponds to the J-cost.
proof idea
Direct definition that assigns the rational constant 5/4.
why it matters
This definition supplies the just-intonation reference that the downstream theorem third_quality compares against the equal-tempered majorThird to establish the 14-cent sharpness. It fills the module's prediction that the major third approximates 5/4 under φ-scaling for optimal consonance and circle-of-fifths closure. The setting connects to the Recognition framework's eight-tick octave and phi-ladder without introducing physical constants at this layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.