pitchJNDFraction_pos
plain-language theorem explainer
The declaration proves that the pitch just-noticeable difference fraction, defined as the reciprocal of the golden ratio to the eighth power, is strictly positive. Psychoacoustics researchers modeling auditory quanta in Recognition Science cite it when building certification records for JND properties. The proof is a term-mode reduction that unfolds the definition and applies the inverse-positivity and power-positivity lemmas in sequence.
Claim. $0 < phi^{-8}$, where $phi$ is the golden ratio constant supplied by the Constants bundle.
background
The Acoustics module derives the just-noticeable difference for musical pitch from the J-cost function. pitchJNDFraction is defined as the reciprocal of phi raised to the eighth power, representing the fraction of the octave for one auditory phi-step in the eight-tick octave. This construction relies on the Constants structure, which provides phi_pos asserting that the golden ratio is positive, and aligns with the module's RS prediction of a JND near 5.7 cents for trained listeners.
proof idea
The term proof first unfolds pitchJNDFraction to reveal (phi ^ 8)^{-1}. It then applies inv_pos.mpr to reduce the goal to phi ^ 8 > 0. Finally it invokes pow_pos using Constants.phi_pos to conclude that the power is positive.
why it matters
The result supplies the jnd_pos field in the PitchJNDCert record constructed later in the same module. It completes the structural theorem for the acoustics derivation and anchors the RS prediction that the canonical pitch JND lies in the trained-listener range of 3-20 cents. No open questions or scaffolding remain for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.