jcost_majorThird
plain-language theorem explainer
The J-cost of the major third interval at frequency ratio 5/4 equals exactly 1/40. Researchers ranking consonance levels via Recognition Science cost hierarchies cite this equality to anchor comparisons among common intervals. The proof is a direct reference to the already-computed result in the HarmonicModes module.
Claim. For the major third interval with frequency ratio $r = 5/4$, the J-cost satisfies $J(r) = 1/40$.
background
The Consonance module works inside the Recognition Science setting where interval consonance is quantified by the J-cost function imported from the Cost module. The major third is defined as the just ratio 5/4 in the HarmonicModes and Valence modules, matching the equal-temperament value 2^(4/12) only in the separate Aesthetics.MusicalScale definition. Upstream results supply the explicit majorThird definition and the prior theorem that evaluates its J-cost.
proof idea
This is a one-line wrapper that directly invokes the majorThird_jcost theorem from HarmonicModes, which itself reduces the claim by simplification of the J-cost definition followed by ring normalization.
why it matters
The equality supplies the concrete value required by the two downstream hierarchy theorems that order J-costs for the minor third, major third, and fourth. It contributes to the Recognition Science program of deriving musical structure from the J-function and the phi-ladder, consistent with the eight-tick octave and self-similar fixed point in the forcing chain. No open scaffolding questions are closed by this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.