hierarchy_unison_lt_minorThird
plain-language theorem explainer
The theorem establishes that the J-cost of the unison interval is strictly less than the J-cost of the minor third. Researchers modeling musical consonance in the Recognition Science framework would cite this when ordering intervals by increasing cost. The proof is a one-line wrapper that substitutes the explicit J-cost values for each interval and verifies the resulting numerical inequality by direct computation.
Claim. $Jcost(1) < Jcost(6/5)$, where the minor third is the ratio $6/5$.
background
The MusicTheory.Consonance module assigns costs to musical intervals via the Jcost function derived from the Recognition Science J-function. The minor third interval is defined as the real number 6/5 in the HarmonicModes and Valence modules. Upstream lemmas establish that Jcost of the unison equals zero and Jcost of the minor third equals 1/60.
proof idea
This is a one-line wrapper. It rewrites the target inequality by applying the lemmas jcost_unison and jcost_minorThird, which reduce the claim to the numerical comparison 0 < 1/60. The tactic norm_num then discharges the inequality.
why it matters
The result is invoked by the consonance hierarchy theorem to build the chain of strict inequalities from unison through minor third, major third, fourth, fifth and octave. It also supports the extended ratio cost hierarchy that inserts the tritone. Within the Recognition Science framework this ordering contributes to the self-similar structure of intervals consistent with the eight-tick octave periodicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.