pitchJND_ne_zero
plain-language theorem explainer
The just-noticeable difference at rung k on the phi-ladder equals 1 plus phi to the minus k and is nonzero for every natural number k. Psychoacoustics researchers modeling frequency discrimination thresholds from self-similar recognition lattices would cite this when establishing that every rung exceeds the unison case. The proof is a one-line wrapper applying the positivity lemma for the identical quantity.
Claim. For every natural number $k$, the just-noticeable difference at rung $k$, defined by $1 + 1/φ^k$, is nonzero.
background
The module derives pitch perception as a recognition operation on the phi-rung ladder forced by the Recognition Composition Law. The just-noticeable difference at rung $k$ is the smallest frequency ratio above unison that exceeds the per-rung J-cost quantum, given explicitly by $1 + φ^{-k}$. Lower rungs correspond to coarse discrimination while higher rungs yield finer resolution in the sensitive band near 5φ Hz.
proof idea
The proof is a one-line wrapper that applies the positivity result for the just-noticeable difference at the same rung, which already shows the quantity exceeds 1 and therefore cannot be zero.
why it matters
This result completes the basic non-degeneracy properties of the JND ladder inside the MusicTheory module, confirming every rung resolves more than the trivial unison case. It supports the numerical examples at canonical rungs (k=1 yields the perfect fifth; k=5 yields the syntonic comma) and aligns with the phi self-similar fixed point (T6) and the eight-tick octave structure. No downstream uses appear yet, but the lemma underpins the falsifier on psychoacoustic JND data stated in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.