jcost_fifth
plain-language theorem explainer
The J-cost of the perfect fifth (frequency ratio 3/2) equals exactly 1/12. Researchers building cost hierarchies among musical intervals in the Recognition Science framework cite this equality to order consonance. The proof is a one-line wrapper delegating directly to the fifth_jcost computation in HarmonicModes.
Claim. $Jcost(3/2) = 1/12$, where the perfect fifth is the frequency ratio $3/2$ and $Jcost$ is the Recognition Science cost function derived from the $J$-functional.
background
The perfect fifth is defined as the real number $3/2$ in both the CircleOfFifths and HarmonicModes modules. The CircleOfFifths module notes that the ratio of musical semitones (12) to RS modes (8) is the perfect fifth. Jcost is the cost function imported from the Cost module and applied to intervals; the upstream fifth_jcost result obtains the value $1/12$ by simplification and ring arithmetic.
proof idea
This is a one-line wrapper that applies HarmonicModes.fifth_jcost. The upstream theorem itself proceeds by simp [Jcost] followed by the ring tactic to reduce the expression for the ratio $3/2$ to the numerical value $1/12$.
why it matters
This supplies the J-cost value for the fifth required by the three hierarchy theorems in the same module (hierarchy_fifth_lt_octave, hierarchy_fourth_lt_fifth, hierarchy_tritone_lt_fifth). It places the perfect fifth in the cost ordering of intervals. The result connects the 12-tone scale structure to the 8-mode RS framework via the $3/2$ ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.