pitchJND_one_band
plain-language theorem explainer
The theorem establishes that the just-noticeable-difference ratio at rung 1 of the phi-ladder satisfies 1.61 < pitchJND 1 < 1.62. Recognition theorists modeling auditory perception would cite it to anchor the coarsest resolution band to the golden ratio. The proof reduces the claim to the rung-1 definition and closes the interval via the quadratic identity for phi together with its explicit numerical bounds.
Claim. The rung-1 just-noticeable-difference ratio satisfies $1.61 < 1 + 1/φ < 1.62$, where $φ$ denotes the golden ratio.
background
The module derives pitch perception as a recognition operation on an auditory-cortex φ-rung ladder. Two pitches are perceived as distinct precisely when their J-cost separation exceeds the per-rung quantum Jcost(1 + 1/φ^k). The function pitchJND k is defined as the smallest discriminable frequency ratio above unison at resolved rung k, given explicitly by 1 + 1/φ^k; rung 1 corresponds to coarse perception such as untrained listeners or frequencies at the audible edges.
proof idea
The tactic proof first rewrites the goal using the sibling lemma pitchJND_one. It then establishes the identity 1 + 1/phi = phi by invoking phi_pos, phi_ne_zero, and phi_sq_eq, followed by field_simp and nlinarith. The interval is closed by direct application of the bounding lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo.
why it matters
This clause supplies the concrete numerical band for the coarsest rung inside the master certificate pitchPerceptionFromPhiLadderCert. It anchors the JND model to the golden ratio that arises as the self-similar fixed point in the Recognition Science forcing chain and supports the eight-clause certificate asserting that every JND is positive, strictly decreasing, and carries positive J-cost separation from unison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.