superparticular_jcost_decreasing
plain-language theorem explainer
The J-cost of superparticular intervals (n+1)/n strictly decreases as the parameter n increases. Music theorists and physicists working in Recognition Science would cite this to rank consonance via the same cost function that governs physical recognition. The proof rewrites both sides with the explicit superparticular J-cost formula, introduces real casts and positivity facts, then applies div_lt_div_of_pos_left together with nlinarith and linarith on the quadratic denominators.
Claim. For positive integers $m < n$, let $s_k = (k+1)/k$. Then $J(s_n) < J(s_m)$, where $J(x) = (x + x^{-1})/2 - 1$ is the J-cost function induced by the multiplicative recognizer.
background
In the MusicTheory.Consonance module, superparticular intervals are ratios of consecutive integers, $s_k = (k+1)/k$. The J-cost is the cost function induced by a multiplicative recognizer: derivedCost applied to its comparator, which reduces to the J-function on positive ratios. The module comment states that consonance IS low J-cost with no separate function or free parameters; the same cost that drives all of physics determines musical beauty. Upstream results include the cost definition in MultiplicativeRecognizerL4 and the ledger factorization structure in DAlembert.LedgerFactorization.
proof idea
The proof is tactic-mode. It rewrites both Jcost terms via the sibling lemma superparticular_jcost, introduces positivity via Nat.cast_pos and linarith, casts the ordering m < n to reals, and applies div_lt_div_of_pos_left. The remaining inequality m(m+1) < n(n+1) is discharged by nlinarith followed by linarith.
why it matters
This result supports the identification of consonance with low J-cost by showing that superparticular intervals closer to unison incur strictly lower cost. It feeds the hierarchy lemmas (hierarchy_unison_lt_minorThird and siblings) in the same module. In the Recognition framework it illustrates how J-uniqueness (T5) and the cost function extend directly to musical intervals. No open scaffolding questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.