We study the function J(r) = 1/2(r + r⁻¹) - 1 as a universal cost measure for musical frequency ratios. The accompanying Lean formalization proves a uniqueness theorem for J on the positive reals under an explicit hypothesis bundle comprising inversion symmetry, unit normalization, strict convexity, log-coordinate calibration, continuity on (0, ∞), a cosh-add functional identity, and the regularity hypotheses used in the d'Alembert/ODE reduction. Applying J to standard just-intonation ratios produces a complete ordering of musical intervals—unison, minor third, major third, perfect fourth, tritone, perfect fifth, octave—that differs from traditional consonance rankings in specific, testable ways: notably, the perfect fifth has higher J-cost than the minor third, major third, and perfect fourth. We show that the fifth's structural importance arises instead from its role as the bridge ratio 12/8 = 3/2 linking the chromatic octave to an 8-slot oscillation basis, with the twelve-fifths walk closing the octave to within <2% (the Pythagorean comma). We introduce a signed asymmetry function σ(r) = r - r⁻¹ that serves as a comparative valence proxy: larger σ corresponds to brighter affect, and the major third has larger positive skew than the minor third. Finally, we extend J from intervals to chords via a directed pairwise aggregate, defining coherence as Coh(C) = 1/(1 + Conflict(C)), and prove that lower aggregate J-cost implies higher coherence. The core theorem surface cited explicitly in the paper has corresponding machine-checked proofs in the Lean 4 proof assistant.