majorThirdReference_pos
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the ratio 5/4 from the Recognition functional equation.
- Does not compute the associated J-cost or σ-charge.
- Does not address empirical preference data or falsifiers.
formal statement (Lean)
107theorem majorThirdReference_pos : 0 < majorThirdReference := by
proof body
One-line wrapper that applies unfold.
108 unfold majorThirdReference; norm_num
109