majorThirdReference_below_phi
plain-language theorem explainer
The result shows that the just major third frequency ratio 5/4 lies strictly below the golden ratio phi. Researchers deriving modal preferences from J-cost rankings in the Recognition Science musicology track would cite it to locate the major third on the phi-rational ladder. The proof is a one-line term reduction that unfolds the constant definition, invokes the bound phi greater than 1.5, and closes via linear arithmetic.
Claim. The just major third frequency ratio satisfies $5/4 < phi$, where $phi = (1 + sqrt(5))/2$.
background
The ModalPreferenceFromPhi module derives cross-cultural preferences among the seven Greek modes from J-cost rankings of their interval ratios against a phi-rational reference scale. Lower J-cost predicts higher preference, reproducing the observed ranking with Ionian and Aeolian lowest and Locrian highest. The major third reference is introduced as the just intonation ratio 5/4, described as a phi-rational neighbor to 4 phi^{-2} approximately 1.528, with the discrepancy 5/4 minus 1 treated as the sigma-charge relative to the perfect fifth. The upstream lemma phi_gt_onePointFive supplies the concrete bound 1.5 less than phi, obtained from sqrt(5) greater than 2.
proof idea
The proof unfolds the definition of the major third reference to 5/4, applies the lemma establishing 1.5 less than phi, and invokes linarith to obtain the desired strict inequality.
why it matters
This placement of the major third below phi anchors the reference interval inside the phi-ladder used for J-cost calculations across the module. It directly supports the master certificate that ranks Ionian and Aeolian as the two lowest-cost modes. In the broader Recognition Science framework the result aligns with T6, the forcing of phi as the self-similar fixed point, and with the construction of phi-rational intervals for physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.