superparticular_jcost
plain-language theorem explainer
The theorem supplies the explicit J-cost value for each superparticular interval (n+1)/n. Music theorists building consonance hierarchies inside Recognition Science cite this identity when ordering intervals by decreasing cost. The short tactic proof unfolds the interval and cost definitions then reduces the equality by field simplification followed by ring.
Claim. For every positive integer $n$, the J-cost of the superparticular ratio $(n+1)/n$ equals $1/(2n(n+1))$.
background
The superparticular function is defined in the HarmonicModes submodule as the ratio $(n+1)/n$ for positive integers $n$. Jcost is the Recognition Science cost function on positive reals, coinciding with $J(r) = (r + r^{-1})/2 - 1$ applied to a frequency ratio $r$, and is imported via the Cost module. The Consonance module uses these to rank musical intervals by their J-cost values.
proof idea
The tactic proof unfolds the definitions of superparticular and Jcost. It introduces the facts that $n$ and $n+1$ are nonzero reals, applies field_simp to normalize fractions, and finishes with the ring tactic to verify the resulting polynomial identity.
why it matters
The identity is invoked directly by the downstream theorem superparticular_jcost_decreasing to prove that J-cost decreases strictly with larger $n$, thereby ordering the superparticular family by increasing consonance. It supplies the concrete evaluation that connects the general J function of Recognition Science to the specific intervals used in the music-theory development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.