minorThird_jcost
plain-language theorem explainer
The result fixes the J-cost of the minor third interval at exactly 1/60. Music theorists working inside the Recognition Science extension to harmonic analysis cite this when tabulating interval costs for consonance calculations. The proof is a one-line wrapper that unfolds the Jcost definition via simp then normalizes the resulting expression with ring.
Claim. $Jcost(6/5) = 1/60$
background
The HarmonicModes module introduces minorThird as the concrete ratio 6/5. Jcost is imported from the Cost module and applies the J function to interval ratios to produce a recognition cost. The same minorThird definition appears in the Valence module. This places the declaration inside the systematic cost assignment for standard musical intervals that later feeds consonance measures.
proof idea
The proof is a one-line wrapper. It calls simp on the Jcost definition to expand the cost expression, then applies ring to verify the numerical identity.
why it matters
This supplies the minor third cost value to the Consonance module, where it is re-exported as jcost_minorThird. It populates the interval cost table used to derive consonance relations inside the music theory layer of Recognition Science. The placement aligns with the J-uniqueness step and the eight-tick octave structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.