octave_jcost
plain-language theorem explainer
The J-cost of the octave frequency ratio equals one quarter. Music theorists working inside the Recognition framework cite this baseline when ranking other interval costs such as the fifth. The proof is a one-line wrapper that unfolds the Jcost definition and normalizes the resulting algebraic identity.
Claim. $Jcost(2) = 1/4$, where the argument 2 denotes the octave frequency ratio and Jcost is the cost induced by the J-functional $J(x) = (x + x^{-1})/2 - 1$.
background
In HarmonicModes the octave is introduced as the real number 2, the frequency ratio of one octave. This matches the ratio definition in MusicalScale and the period definition 8 times tick in Constants, which itself equals 2^D for spatial dimension D = 3. The Jcost function, drawn from the Cost module, applies the J-functional directly to positive real ratios that represent musical intervals.
proof idea
The proof is a one-line wrapper. It applies simp to unfold Jcost at the octave ratio, then invokes ring to confirm the resulting expression equals 1/4.
why it matters
The result supplies the explicit octave cost used by fifth_cost_lt_octave_cost to prove the fifth costs strictly less than the octave and re-exported verbatim by jcost_octave. It anchors cost calculations for the chromatic scale inside the music-theory layer and aligns with the eight-tick octave of the T7 forcing-chain step. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.