pitchJND_increment_geometric
plain-language theorem explainer
pitchJND_increment_geometric establishes the geometric scaling of just-noticeable-difference increments on the phi-ladder. Researchers modeling auditory recognition cite the relation to confirm self-similar contraction by 1/phi per rung. The tactic proof unfolds the definition of pitchJND, invokes phi non-zero, and reduces both sides via field_simp and ring.
Claim. For each natural number $k$, $(pitchJND(k+1) - 1) phi = pitchJND(k) - 1$, where $pitchJND(k) = 1 + phi^{-k}$ is the smallest frequency ratio distinguishable from unison at rung $k$.
background
The Pitch Perception from the φ-Ladder module derives pitch resolution as a recognition operation on an auditory phi-rung ladder. The just-noticeable difference at rung $k$ is the minimal frequency ratio above unison, given explicitly by $pitchJND(k) = 1 + phi^{-k}$. This structure follows from the J-cost of a recognition event exceeding the per-rung quantum induced by the multiplicative recognizer cost function.
proof idea
The tactic proof unfolds pitchJND to expose the explicit form $1 + 1/phi^{k+1}$. It obtains $phi$ non-zero from phi_ne_zero and the relevant powers non-zero via pow_ne_zero. A rewrite with pow_succ followed by field_simp equates the scaled term at rung $k+1$ to the term at rung $k$. Ring tactics then simplify both sides to finish the equality.
why it matters
This result supplies the geometric improvement property required by pitchPerceptionFromPhiLadderCert, which assembles the full set of JND properties into a single certificate. It also appears in pitch_perception_one_statement, the one-statement theorem that collects the complete pitch perception claim for track L6. The relation confirms the self-similar scaling forced by the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.