jcost_unison
plain-language theorem explainer
The result establishes that the J-cost of the unison interval (frequency ratio 1) equals zero. Music theorists applying Recognition Science to consonance would cite this as the zero baseline for interval hierarchies. The proof is a direct one-line invocation of the unit lemma for the J-cost function.
Claim. The J-cost of the frequency ratio 1 satisfies $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$.
background
The J-cost function is defined in the Cost module as the squared-ratio expression $J(x) = (x-1)^2/(2x)$, which is equivalent to the hyperbolic form appearing in the Recognition Composition Law. In the MusicTheory.Consonance module this function is applied to standard musical intervals (unison, minor third, etc.) to rank consonance. The upstream lemma Jcost_unit0 supplies the base case $J(1) = 0$ by direct simplification of the definition.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module (itself obtained by simp on the J-cost definition).
why it matters
This supplies the zero anchor for the consonance hierarchy theorems, notably the downstream result that unison cost is strictly less than minor-third cost. It aligns with the J-uniqueness step (T5) and the Recognition Composition Law by fixing the minimal cost point for interval analysis within the music-theory application of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.