majorThirdReference_pos
plain-language theorem explainer
The declaration proves positivity of the major third reference ratio in the phi-rational scale. Musicologists modeling cross-cultural modal preferences via J-cost would cite it to ensure interval ratios remain positive when computing discrepancies against the perfect fifth. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
Claim. The major-third reference frequency ratio satisfies $0 < 5/4$.
background
The Musicology module derives modal preferences from J-cost rankings of the seven Greek modes against phi-rational reference intervals. majorThirdReference is defined as the just-intonation major third 5/4, identified as the phi-rational neighbor 4·φ^{-2} ≈ 1.528 whose discrepancy from 1 measures the σ-charge relative to the perfect fifth 3/2. This positivity result is a prerequisite for all subsequent cost calculations under the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that unfolds majorThirdReference to the literal value 5/4 and invokes norm_num to discharge the strict inequality.
why it matters
The result anchors the modal-preference derivations by guaranteeing that the reference interval lies in the positive reals, consistent with the J-uniqueness and phi-ladder steps of the forcing chain. It supports the module's claim that Ionian and Aeolian modes occupy the two lowest cost ranks while Locrian occupies the highest. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.