pitchJND_pos
plain-language theorem explainer
pitchJND_pos asserts that the just-noticeable difference at rung k on the phi-ladder is strictly positive for every natural number k. Psychoacoustics researchers modeling pitch discrimination via self-similar recognition lattices cite this to anchor threshold positivity. The proof is a one-line term wrapper applying lt_trans to zero_lt_one and the sibling inequality pitchJND_gt_one k.
Claim. For every natural number $k$, the rung-$k$ just-noticeable difference on the phi-ladder satisfies $0 < 1 + phi^{-k}$.
background
The module derives just-noticeable differences in pitch perception from the phi-ladder forced by the Recognition Science recognition lattice. pitchJND k stands for the smallest discriminable frequency ratio above unison at resolution level k and equals 1 + 1/phi^k. Two pitches are distinct precisely when their J-cost separation exceeds the per-rung quantum Jcost(1 + 1/phi^k); lower k gives coarse perception and higher k gives fine resolution in the 1-4 kHz band.
proof idea
The proof is a term-mode one-liner: lt_trans zero_lt_one (pitchJND_gt_one k). It chains the base inequality 0 < 1 with the fact that pitchJND k > 1 supplied by the sibling theorem pitchJND_gt_one, invoking the transitivity lemma lt_trans from ArithmeticFromLogic.
why it matters
This result supplies the strict positivity required by the master certificate PitchPerceptionFromPhiLadderCert and by pitchJND_jcost_pos. It completes the module claim that every rung resolves more than the trivial unison, supporting the phi-ladder JND structure (T6 self-similar fixed point, T7 eight-tick octave). The derivation touches the open question of quantitative match to empirical JND data reported by Wier-Jesteadt-Green and Moore.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.