pitchJND_succ_lt
plain-language theorem explainer
The just-noticeable-difference threshold on the phi-ladder is strictly decreasing: the resolution at rung k+1 is finer than at rung k for any natural number k. Music theorists and psychoacoustics researchers working within Recognition Science cite this to establish the ordering of perceptual thresholds along the ladder. The proof is a one-line wrapper that applies the strict anti-monotonicity lemma to the successor relation on natural numbers.
Claim. For every natural number $k$, the just-noticeable difference at rung $k+1$ is strictly less than the just-noticeable difference at rung $k$: $1 + 1/φ^{k+1} < 1 + 1/φ^k$.
background
This theorem belongs to the module that derives pitch perception from the phi-ladder as Track L6 of Plan v7. The just-noticeable-difference at rung $k$ is the smallest frequency ratio $1 + 1/φ^k$ distinguishable by a cortical-column resonance network; two pitches are perceived as distinct precisely when their J-cost separation exceeds the rung-specific quantum. The module treats pitch perception as a recognition operation on this ladder, with lower rungs corresponding to coarse perception and higher rungs to fine resolution in the 1-4 kHz band.
proof idea
The proof is a one-line wrapper that applies the strict anti-monotonicity of the just-noticeable-difference function to the fact that $k$ is strictly less than its successor.
why it matters
The result populates the strictly-decreasing field inside the master certificate PitchPerceptionFromPhiLadderCert. It supplies the ordering property required by the phi-ladder model of pitch perception, consistent with the self-similar fixed point phi (T6) and the eight-tick octave. The ordering aligns the derived thresholds with empirical JND values near 5 cents for trained listeners in the sensitive band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.