jcost_octave
plain-language theorem explainer
The theorem states that the J-cost of the octave frequency ratio equals exactly 1/4. Music theorists constructing consonance orderings inside the Recognition Science framework cite it to anchor interval comparisons. The proof is a one-line wrapper delegating directly to the computation in HarmonicModes.
Claim. $Jcost(2) = 1/4$, where $Jcost$ is the recognition cost on frequency ratios and the octave is the ratio 2.
background
Jcost is the cost function on frequency ratios imported from the Cost module and specialized in HarmonicModes. The octave is defined there as the real number 2, matching the ratio in MusicalScale and the 8-tick period in Constants. Upstream results establish the octave as $2^D$ in CoherenceExponent and as a FrequencyRatio in UniversalForcing.Strict.Music. The local module Cononance imports these to build interval hierarchies.
proof idea
The proof is a one-line wrapper that applies HarmonicModes.octave_jcost. That upstream theorem reduces the claim by simp on the Jcost definition followed by ring normalization.
why it matters
The result is invoked by hierarchy_fifth_lt_octave to show the fifth lies below the octave in the cost ordering. It supplies the base case for consonance comparisons inside the Recognition framework, consistent with the eight-tick octave and the phi-ladder structure. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.