PitchJNDCert
plain-language theorem explainer
The declaration defines a record type that certifies the pitch just-noticeable difference fraction equals phi to the minus eight, lies strictly between zero and one, and that the associated J-cost vanishes at equal frequencies while remaining nonnegative for positive arguments. Acoustics researchers working inside Recognition Science would cite it when connecting the eight-tick octave to measured discrimination thresholds. The definition simply assembles four already-proved sibling lemmas into a single structure.
Claim. Let $δ = φ^{-8}$. A certificate structure records that $0 < δ < 1$, that the J-cost $C(f,f) = 0$ for every nonzero frequency $f$, and that $C(m,r) ≥ 0$ whenever both frequencies are positive, where $C$ denotes the J-cost applied to the ratio of measured to reference frequency.
background
Recognition Science identifies the just-noticeable difference in musical pitch with the recognition quantum at the eighth tick of the octave. The pitch JND fraction is therefore defined as the reciprocal of phi raised to the eighth power, which lies near 0.0057 and corresponds to roughly 5.7 cents. The cost function is obtained by applying the general J-cost to the ratio of two frequencies. The structure bundles the positivity and upper-bound lemmas for this fraction with the zero-at-unison evaluation and the nonnegativity result imported from the theory of recognition events.
proof idea
The definition is a direct record construction that supplies the four fields from the sibling lemmas pitchJNDFraction_pos, pitchJNDFraction_lt_one, pitchCost_at_unison, and pitchCost_nonneg. No tactics or reductions are performed; the structure simply packages the already-established facts.
why it matters
The structure supplies the concrete certificate that the eight-tick octave produces a JND fraction inside the psychoacoustic window stated in the module. It is consumed by the cert definition and the subsequent inhabitedness theorem. The module doc presents the result as a structural theorem with zero sorries and gives the explicit falsifier: any study placing trained-listener pitch JND consistently outside the interval (3,20) cents. It thereby closes the link between the phi-ladder and auditory discrimination.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.