cert
plain-language theorem explainer
This definition constructs an explicit PitchJNDCert record for the pitch just-noticeable difference fraction derived from the J-cost. Acoustics researchers modeling auditory discrimination in Recognition Science would cite it to certify that the fraction lies in (0,1) and that the associated cost function meets the required non-negativity and zero-at-unison conditions. The construction proceeds by direct assignment of four previously established theorems to the structure fields.
Claim. Let $p$ denote the pitch JND fraction derived from the J-cost. The definition cert is the structure PitchJNDCert asserting $0 < p < 1$, that the pitch cost vanishes at unison ($pitchCost(f,f)=0$ for $f ≠ 0$), and that the pitch cost is non-negative ($pitchCost(m,r) ≥ 0$ whenever $m>0$ and $r>0$).
background
In the Recognition Science treatment of acoustics the just-noticeable difference for musical pitch is obtained by applying the J-cost to frequency ratios on the phi-ladder. The module isolates the eighth-tick step (one-eighth semitone) as the canonical JND, yielding the fraction $φ^{-8}$ of the octave. The structure PitchJNDCert packages the four properties required to certify this fraction as a valid recognition threshold: strict positivity, strict upper bound below unity, vanishing cost at equal frequencies, and non-negative cost for positive arguments.
proof idea
The definition is a direct record literal that populates the four fields of PitchJNDCert. It assigns pitchJNDFraction_pos and pitchJNDFraction_lt_one to the bound fields, pitchCost_at_unison to the unison condition, and pitchCost_nonneg to the non-negativity condition; the last of these unfolds to the general cost_nonneg lemma from ObserverForcing applied to the ratio argument.
why it matters
This definition closes the structural theorem of the Acoustics module by exhibiting a concrete inhabitant of PitchJNDCert. It supports the Recognition Science prediction that the pitch JND equals the phi^{-8} octave step (approximately 5.7 cents) and lies inside the observed 3-20 cent band for trained listeners. The module falsifier is any psychoacoustic study placing trained-listener JND consistently outside that interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.