pitch_perception_one_statement
plain-language theorem explainer
The theorem asserts that the just-noticeable-difference function on the auditory phi-ladder obeys five properties: every value exceeds 1, the function is strictly decreasing, adjacent rungs satisfy the geometric recurrence (pitchJND(k+1) - 1) phi = pitchJND(k) - 1, every value has positive J-cost separation from unison, and the rung-1 case equals 1 + phi inverse. Psychoacoustics modelers working with recognition lattices would cite this as the discrete JND structure forced by phi-self-similarity. The proof is a one-line wrapper that assembles a
Claim. Let $JND : ℕ → ℝ_{>1}$ be the just-noticeable-difference function on the φ-ladder. Then ∀k ∈ ℕ, 1 < JND(k), JND is strictly decreasing, ∀k, (JND(k+1) - 1) φ = JND(k) - 1, ∀k, 0 < J(JND(k)) where J denotes J-cost, and JND(1) = 1 + φ^{-1}.
background
The module derives pitch perception as a recognition operation on the auditory-cortex φ-rung ladder. Two frequencies are perceived distinct precisely when their J-cost separation exceeds the per-rung quantum Jcost(1 + 1/φ^k). The function pitchJND(k) = 1 + 1/φ^k supplies the smallest discriminable ratio above unison at rung k, with lower k corresponding to coarse perception and higher k to fine resolution in the sensitive band. J-cost is the cost of a recognition event, defined as Cost.Jcost e.state for RecognitionEvent e (ObserverForcing.cost). The rung function appears in multiple mass and spectroscopy contexts as an integer label on the φ-ladder (AnchorPolicy.rung, AsteroidOreSpectroscopy.rung).
proof idea
The proof is a one-line term wrapper that directly assembles the five sibling lemmas pitchJND_gt_one, pitchJND_strict_anti, pitchJND_increment_geometric, pitchJND_jcost_pos and pitchJND_one. No additional tactics or reductions are required; the conjunction is formed by tuple construction from the already-proved statements on the JND properties.
why it matters
This statement collects the core properties of the JND ladder into a single theorem (Track L6), supplying the discrete structure that any downstream model of pitch discrimination must respect. It sits inside the Recognition Science forcing chain at the level of phi-self-similarity (T6) and the eight-tick octave, with the geometric recurrence directly reflecting the multiplicative recognizer cost law. Because used_by is empty, the result functions as a terminal interface for psychoacoustic applications rather than feeding further internal theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.