pitchJND_strict_anti
plain-language theorem explainer
The map sending rung index k to the just-noticeable pitch ratio 1 + φ^{-k} is strictly decreasing on the naturals. Auditory modelers using self-similar recognition lattices cite this to confirm that higher rungs deliver finer frequency discrimination. The short tactic proof unfolds the definition of pitchJND and reduces the claim to the already-proved strict decrease of the inverse-phi power via linear arithmetic.
Claim. The function $kmapsto 1+phi^{-k}$ from natural numbers to reals is strictly decreasing: if $a<b$ then $1+phi^{-a}>1+phi^{-b}$.
background
In this module pitch perception arises as a recognition operation on the φ-ladder. The rung-k just-noticeable difference is defined by pitchJND k := 1 + 1/φ^k, the smallest frequency ratio above unison that exceeds the per-rung J-cost quantum. The module derives this ladder from the Recognition Composition Law and the self-similar fixed point φ, with lower rungs corresponding to coarse perception and higher rungs to fine resolution in the 1-4 kHz band. The upstream lemma inv_phi_pow_strict_anti states that 1/φ^k is strictly decreasing because φ>1, supplying the monotonicity ingredient used here.
proof idea
Assume natural numbers a < b. Unfold pitchJND on both sides to obtain the expressions 1 + 1/φ^a and 1 + 1/φ^b. Apply the upstream result inv_phi_pow_strict_anti to the hypothesis a < b, yielding 1/φ^a > 1/φ^b. Linear arithmetic then concludes the desired strict inequality.
why it matters
This supplies the strict-decrease clause required by pitchJND_succ_lt, by the master certificate pitchPerceptionFromPhiLadderCert, and by the one-statement theorem pitch_perception_one_statement. It completes the ordering property of the JND ladder forced by the φ-self-similar recognition lattice (Track L6), consistent with the phi fixed point and the eight-tick octave in the broader framework. No open scaffolding remains on this specific monotonicity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.