pitchJNDFraction_lt_one
plain-language theorem explainer
The theorem shows that the pitch just-noticeable difference fraction of the octave, defined as the reciprocal of the golden ratio to the eighth power, is strictly less than one. Psychoacoustics researchers applying Recognition Science to musical perception would reference this bound when confirming that the predicted JND remains a small fraction of the octave. The proof is a direct term reduction that unfolds the definition and applies the inequality for powers of a number greater than one.
Claim. The pitch just-noticeable difference fraction of the octave satisfies $phi^{-8} < 1$, where $phi$ denotes the golden ratio.
background
In the module on musical pitch JND derived from J-cost, the pitch JND fraction is introduced as $phi^{-8}$, corresponding to the auditory phi-step of one-eighth of a semitone in the eight-tick octave. This definition arises from the Recognition Science forcing chain where the period is $2^3$ and leads to the phi-ladder structure. The result depends on the established fact that the golden ratio phi exceeds one, proven via its quadratic equation in the Constants module. The local theoretical setting predicts the canonical pitch JND as approximately 5.7 cents for trained listeners, with a falsifier being any consistent observation outside the 3-20 cent range.
proof idea
The proof unfolds the definition of the pitch JND fraction to reveal the reciprocal of phi raised to the eighth power. It rewrites the goal using the inverse-less-than-one equivalence, reduces the claim to phi to the eighth exceeding one, and applies the power inequality lemma together with the fact that phi is greater than one, followed by numerical normalization.
why it matters
This theorem is invoked in the construction of the PitchJNDCert certificate, which collects the positivity, upper bound, and cost properties for the pitch JND. It fills the structural requirement in the acoustics module for the Recognition Science prediction of the JND as phi to the minus eight, aligning with the T7 eight-tick octave landmark. The module leaves open the precise psychoacoustic validation against the falsifier range of 3 to 20 cents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.