superparticular
plain-language theorem explainer
Superparticular defines the ratio (n+1)/n for natural n as the generator of standard musical intervals. Harmonic analysts cite it when ordering intervals by J-cost in consonance hierarchies. The definition is a direct arithmetic expression with no lemmas or tactics.
Claim. For each natural number $n$, the superparticular ratio is $((n : ℝ) + 1) / (n : ℝ)$.
background
In the HarmonicModes module, superparticular ratios supply the primitive intervals whose recognition costs are computed via the J-cost function imported from the Cost module. J-cost applies the Recognition Science function J(x) = (x + x^{-1})/2 - 1 to a ratio r, yielding a positive real that decreases with simpler intervals. The module imports Mathlib for real arithmetic and Cost for the Jcost definition; no upstream lemmas are required because this is the base definition.
proof idea
The declaration is a one-line definition that casts the natural number n to real and returns the ratio (n+1)/n. No tactics, lemmas, or reductions are applied; downstream proofs such as superparticular_jcost unfold the definition and simplify the resulting algebraic expression for Jcost.
why it matters
This definition feeds the theorems fifth_eq_superparticular, fourth_eq_superparticular, superparticular_jcost, superparticular_jcost_decreasing, and extended_ratio_cost_hierarchy. It supplies the explicit ratios for the fifth (n=2) and fourth (n=3) that appear in the twelve_fifths_overshoot result and the consonance ordering. Within the Recognition framework it connects music intervals to the J-uniqueness step (T5) and the phi-ladder by allowing J-cost to be evaluated directly on superparticular sequences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.