PitchPerceptionFromPhiLadderCert
plain-language theorem explainer
The structure collects eight properties of the just-noticeable-difference ratio function on the phi-ladder. Psychoacoustics researchers modeling perceptual resolution via recognition operations would cite this certificate when deriving JND ladders from self-similar lattices. It is assembled as a definition by enumerating clauses on positivity, strict decrease, geometric increments, and J-cost positivity, each backed by real-arithmetic lemmas on phi.
Claim. Let $p(k) = 1 + 1/φ^k$ denote the rung-$k$ just-noticeable frequency ratio above unison. The certificate asserts that for every natural number $k$, $p(k) > 1$, $p(k) > 0$, $p$ is strictly decreasing, $p(k+1) < p(k)$, the increment satisfies $(p(k+1)-1)φ = p(k)-1$, the J-cost of each ratio is positive, $p(1) = 1 + 1/φ$, and $1.61 < p(1) < 1.62$.
background
In the Recognition Science framework, pitch perception is a recognition operation on the auditory-cortex phi-rung ladder. The function pitchJND(k) gives the smallest perceptually distinct frequency ratio at rung k, defined explicitly as 1 + 1/φ^k. Lower rungs correspond to coarse perception for untrained listeners; higher rungs to fine resolution in the most-sensitive band. The J-cost quantifies separation from unison via the Cost.Jcost machinery imported from RSNative.Core.
proof idea
The declaration is a structure definition whose fields are the eight listed properties. Inhabitation is supplied downstream by pitchPerceptionFromPhiLadderCert, which directly assigns lemmas pitchJND_gt_one, pitchJND_pos, pitchJND_strict_anti, pitchJND_succ_lt, pitchJND_increment_geometric, pitchJND_jcost_pos, and the two rung-1 statements. Each lemma follows from real-arithmetic bounds on the geometric sequence generated by phi.
why it matters
This certificate supplies the master collection of JND properties for Track L6. It is the type of the downstream definition pitchPerceptionFromPhiLadderCert that asserts the master certificate is inhabited. The structure closes the derivation of perceptual resolution from the phi-ladder, connecting to the self-similar fixed point and eight-tick octave in the forcing chain. It leaves open the precise numerical match to empirical 5-cent JND data at specific rungs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.