pitchJND_gt_one
plain-language theorem explainer
The theorem shows that the just-noticeable-difference at every rung k of the phi-ladder satisfies 1 < pitchJND k. Recognition theorists and psychoacousticians modeling auditory resolution from the self-similar lattice would cite it to guarantee that no rung collapses to the trivial unison. The tactic proof unfolds the definition, chains positivity of phi and its powers with the positivity tactic, and closes via linarith.
Claim. For every natural number $k$, $1 < 1 + phi^{-k}$, where $phi$ is the golden-ratio fixed point of the recognition composition law and $pitchJND k$ denotes the rung-$k$ just-noticeable-difference $1 + phi^{-k}$.
background
The module derives pitch perception as a recognition operation on the auditory-cortex phi-rung ladder. Two pitches are perceived distinct precisely when their J-cost separation exceeds the per-rung quantum $Jcost(1 + 1/phi^k)$. The definition $pitchJND k := 1 + phi^{-k}$ supplies the smallest discriminable frequency ratio above unison at rung $k$; lower rungs give coarse resolution while higher rungs give finer resolution for trained listeners in the 1-4 kHz band.
proof idea
The proof unfolds the definition of pitchJND. It obtains $0 < phi$ from the upstream lemma phi_pos, deduces $0 < phi^k$ via pow_pos, establishes $0 < 1/phi^k$ by the positivity tactic, and concludes the strict inequality by linarith.
why it matters
The result is invoked directly by pitchJND_pos, pitchJND_jcost_pos, and the master certificate pitchPerceptionFromPhiLadderCert; it supplies the first conjunct of the one-statement theorem pitch_perception_one_statement. It anchors the discrete JND ladder forced by the phi self-similar fixed point (T6) and the eight-tick octave structure, confirming that every cortical-column resonance level resolves beyond unison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.