IndisputableMonolith.MusicTheory.PitchPerceptionFromPhiLadder
The module defines the rung-k just-noticeable pitch ratio above unison as 1 + φ^{-k}. Researchers connecting Recognition Science forcing steps to auditory thresholds would cite it. The module supplies the core definition plus lemmas on positivity, monotonicity, and geometric increment using the imported constants and cost function.
claimThe rung-$k$ just-noticeable pitch ratio above unison is $1 + \phi^{-k}$.
background
Recognition Science derives the phi-ladder from J-uniqueness (T5) and the self-similar fixed point (T6). The Constants module supplies the base time quantum τ₀ = 1 tick. The Cost module supplies the J-cost function whose fixed point yields φ. This module applies the same ladder to the smallest perceptually distinct frequency ratio.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the pitch-perception layer of the Recognition Science music-theory component. It extends the phi-ladder (T6) and eight-tick octave (T7) to sensory JNDs, providing a direct link from the forcing chain to auditory discrimination. No downstream theorems are recorded yet.
scope and limits
- Does not derive the phi-ladder or golden ratio from the J-cost equation.
- Does not supply numerical JND values in physical frequency units.
- Does not model consonance, harmony, or multi-note intervals.
depends on (2)
declarations in this module (14)
-
def
pitchJND -
theorem
pitchJND_gt_one -
theorem
pitchJND_pos -
theorem
pitchJND_ne_zero -
theorem
inv_phi_pow_strict_anti -
theorem
pitchJND_strict_anti -
theorem
pitchJND_succ_lt -
theorem
pitchJND_increment_geometric -
theorem
pitchJND_jcost_pos -
theorem
pitchJND_one -
theorem
pitchJND_one_band -
structure
PitchPerceptionFromPhiLadderCert -
def
pitchPerceptionFromPhiLadderCert -
theorem
pitch_perception_one_statement