fourth_jcost
plain-language theorem explainer
The J-cost of the musical fourth interval with frequency ratio 4/3 equals exactly 1/24. Music theorists working within Recognition Science cite this when evaluating consonance for harmonic modes built from superparticular ratios. The proof is a one-line wrapper that unfolds the Jcost definition and applies algebraic ring normalization.
Claim. $J(4/3) = 1/24$, where $J(x) = (x + x^{-1})/2 - 1$ is the Recognition Science cost function applied to the frequency ratio of the fourth.
background
The HarmonicModes module defines standard musical intervals as real numbers for frequency ratios. The fourth is introduced as the ratio 4/3. Jcost is the cost function imported from the Cost module; it evaluates the J function on a given ratio. This supplies the explicit numerical value needed for downstream consonance calculations. The result rests on the upstream definition of the fourth interval as 4/3.
proof idea
The proof is a one-line wrapper that applies the simp tactic to unfold the Jcost definition, followed by the ring tactic for algebraic simplification to the constant 1/24.
why it matters
This theorem is invoked directly by jcost_fourth in the Consonance module to supply the cost value for consonance measures. It contributes to the Recognition Science derivation of musical harmony from the J-uniqueness property and the phi-ladder of intervals. The computation confirms the cost for the superparticular ratio 4/3 inside the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.