superparticular_pos
plain-language theorem explainer
The superparticular ratio for positive integer n is strictly positive. Music theorists building harmonic modes from Recognition primitives would cite this to guarantee interval ratios stay positive in mode derivations. The proof is a direct unfolding of the ratio definition followed by an application of the division positivity lemma from Mathlib.
Claim. For every positive integer $n$, the ratio $(n+1)/n$ is positive.
background
In the HarmonicModes module the superparticular function is defined by the explicit formula ((n : ℝ) + 1) / (n : ℝ). This supplies the basic interval ratios from which the module derives the octave, fifth, fourth and other named intervals via sibling equalities. The module sits inside the Recognition Science development, importing Cost and Mathlib to embed these ratios in the larger framework that derives physical constants from the J-functional equation and the phi-ladder.
proof idea
The term proof first unfolds the definition of superparticular to obtain the division expression. It then applies the Mathlib lemma div_pos, discharging the numerator positivity subgoal with the positivity tactic and the denominator positivity subgoal with Nat.cast_pos.mpr applied to the hypothesis 0 < n.
why it matters
This result supplies the elementary positivity fact required for all superparticular-based interval constructions in the module. It therefore supports the chain of equalities that identify the octave, fifth and fourth with specific superparticular ratios, feeding the Recognition Science treatment of harmonic modes as instances of the underlying forcing chain and RCL. No open scaffolding is closed here; the lemma is a terminal positivity check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.