majorThirdReference
plain-language theorem explainer
majorThirdReference supplies the just-intonation major-third frequency ratio 5/4 as the baseline constant for J-cost calculations on Greek modes. Musicologists and Recognition Science researchers cite it when comparing interval ratios to the phi-rational neighbor 4 phi^{-2}. The declaration is a direct constant definition with no proof steps or auxiliary lemmas.
Claim. The reference frequency ratio for the major third is defined as $5/4$.
background
The module models cross-cultural modal preference by assigning J-cost to each of the seven Greek modes relative to a canonical major reference. J-cost is the Recognition Science cost function derived from the J-functional on positive reals, with lower values predicting higher preference; the ranking reproduces the Ionian-Aeolian top cluster and Locrian bottom observed in Huron 2006 surveys. The local setting treats frequency ratios as elements of the multiplicative group of positive reals equipped with the J-cost metric, calibrated against phi-forced structures imported from PhiForcingDerived and LedgerFactorization.
proof idea
The declaration is a direct constant definition that assigns the real number 5/4 to majorThirdReference.
why it matters
It supplies the numerical anchor for the two immediate downstream theorems majorThirdReference_pos and majorThirdReference_below_phi, which establish that the reference lies strictly between 0 and phi. These facts close the comparison between the just major third and its phi-rational neighbor 4 phi^{-2} inside the modal-preference ranking. The definition therefore participates in Track I10 by fixing the zero point of the J-cost scale for interval ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.