pith. sign in
module module high

IndisputableMonolith.Acoustics.MusicPitchJNDFromJCost

show as:
view Lean formalization →

This module defines the just noticeable difference fraction for musical pitch as 1/φ^8, obtained by applying the J-cost to frequency ratios near unison. Acoustics and music-perception researchers working in RS-native units cite it for threshold modeling. The module supplies the core definition together with elementary positivity and boundedness lemmas.

claimThe pitch JND fraction of the octave is $1/φ^8$, where $φ$ is the golden-ratio fixed point of the J-cost function.

background

Recognition Science obtains all constants from the J-cost functional equation and the self-similar fixed point φ. The module imports the RS time quantum τ₀ = 1 tick from Constants and the J-cost definitions from the Cost module. It introduces pitchJNDFraction as the frequency-ratio deviation at the perceptual threshold, together with the associated pitchCost function.

proof idea

This is a definition module. It states pitchJNDFraction := 1/φ^8 and proves the three elementary properties pitchJNDFraction_pos, pitchJNDFraction_lt_one and the corresponding cost lemmas by direct substitution and the known inequalities for φ.

why it matters in Recognition Science

The module supplies the acoustic scale that enters higher-level Recognition Science statements on auditory perception and the eight-tick octave structure. It closes the link between the J-cost composition law and the numerical JND fraction used in music modeling.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)