module module high

`IndisputableMonolith.MusicTheory.PitchPerceptionFromPhiLadder`

The module defines the just-noticeable pitch ratio at rung k on the phi-ladder as 1 + φ^{-k}. Auditory perception researchers in Recognition Science cite it to ground musical intervals in the J-cost function. The module supplies the core definition together with lemmas proving the ratio exceeds one, remains positive, and decreases strictly with rung index.

claimThe rung-$k$ just-noticeable pitch ratio above unison is $1 + φ^{-k}$.

background

Recognition Science obtains all scales from the J-cost obeying the Recognition Composition Law. The phi-ladder is the discrete orbit under the self-similar fixed point φ of J. Constants supplies the native time unit τ₀ = 1 tick while Cost supplies the J-function. The module introduces pitchJND(k) as the smallest frequency ratio distinguishable from 1 at rung k.

proof idea

This is a definition module. It states the pitchJND definition and proves elementary properties (positivity, strict decrease, geometric increments) from the ordering properties of powers of φ.

why it matters in Recognition Science

The definitions feed the PitchPerceptionFromPhiLadderCert sibling and supply the perceptual layer for music theory constructions. They link the phi-ladder (T6) to auditory discrimination, preparing the ground for octave-based interval recognition (T7).

scope and limits

Does not compute numerical JND values in Hertz.
Does not compare the model to experimental psychoacoustic thresholds.
Does not extend to timbre or loudness perception.
Does not address non-octave intervals or harmony.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (14)

def pitchJND L84
theorem pitchJND_gt_one L88
theorem pitchJND_pos L96
theorem pitchJND_ne_zero L100
theorem inv_phi_pow_strict_anti L106
theorem pitchJND_strict_anti L119
theorem pitchJND_succ_lt L126
theorem pitchJND_increment_geometric L133
theorem pitchJND_jcost_pos L151
theorem pitchJND_one L158
theorem pitchJND_one_band L165
structure PitchPerceptionFromPhiLadderCert L195
def pitchPerceptionFromPhiLadderCert L207
theorem pitch_perception_one_statement L230