pitchJND_one
plain-language theorem explainer
The rung-1 just-noticeable-difference equals 1 plus the reciprocal of the golden ratio. Psychoacoustics researchers deriving pitch resolution from the phi-ladder would cite this base case. The proof is a term-mode reduction that unfolds the pitchJND definition and simplifies the unit exponent.
Claim. The just-noticeable pitch ratio at rung 1 satisfies $1 + 1/φ = pitchJND(1)$.
background
The Pitch Perception from the φ-Ladder module treats pitch resolution as a recognition operation on the auditory-cortex φ-rung ladder. The definition pitchJND(k) := 1 + 1/φ^k supplies the smallest frequency ratio distinguishable at integer rung k, with lower rungs corresponding to coarser perception. The Rung abbreviation from Support.RungFractions provides the integer indexing on the ladder. Upstream results include the band operation on stable states from PreLogicalCost and the fifth ratio 3/2 from both CircleOfFifths and HarmonicModes, which anchor the musical interpretation of the ladder.
proof idea
The proof is a one-line wrapper that unfolds the pitchJND definition, applies congruence to align the expressions, and rewrites the power using pow_one to reduce φ^1 to φ.
why it matters
This base case supplies the explicit value at the coarsest rung for the pitchPerceptionFromPhiLadderCert certificate and the pitch_perception_one_statement theorem. It anchors the rung-1 case in the perfect-fifth band via the downstream pitchJND_one_band theorem. Within the Recognition Science framework it realizes the phi fixed point at the first level of the ladder, consistent with the self-similar forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.