Pith. sign in
module module moderate

IndisputableMonolith.Acoustics.MusicConsonanceFromJCost

show as:
view Lean formalization →

Packages musical interval consonance as nonnegativity and threshold facts for the Recognition J-cost on frequency ratios. Acoustics and RS workers cite it for the certificate that pure intervals sit under a canonical cost bound. The module is mostly definitions (domain cost, threshold, MusicConsonanceCert) plus elementary positivity and equilibrium lemmas from Cost.

claimOn frequency ratios $r>0$, set domain cost $C(r)=J(r)$ with $J(x)=\frac{x+x^{-1}}{2}-1$. Record $C(1)=0$ and $C\ge 0$, fix a positive canonical threshold $\theta$, and package a MusicConsonanceCert that the consonance criterion is the $J$-cost bound relative to $\theta$.

background

Recognition Science forces a unique nonnegative cost on positive reals, $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), vanishing only at equilibrium $x=1$ (forcing step T5). Musical intervals are positive frequency ratios; unison is that equilibrium.

The Cost import supplies $J$ and its elementary calculus; Constants supplies RS-native units (including the tick $\tau_0$). This acoustics module specializes those objects to pitch ratios: a domain cost, a fixed positive threshold, and a small certificate type that packages the consonance claim for downstream use.

proof idea

Definition-and-lemma module, not a deep derivation. domainCost is $J$ on the ratio; equilibrium at $1$ and nonnegativity are one-line transfers from Cost. canonicalThreshold is a fixed positive constant with a positivity lemma. MusicConsonanceCert is a structure bundling the criterion; cert and cert_inhabited witness that the bundle is inhabited. No multi-step tactic argument beyond those elementary facts.

why it matters in Recognition Science

Puts music consonance inside the J-cost forcing chain instead of an empirical psychoacoustic table. Thematic link to T7 (eight-tick octave) via the octave ratio $2$, though the module itself is cost-threshold packaging, not a tick-counting argument. The graph shows no used_by edges yet; it is the acoustics-side interface for T5 on intervals, ready for later scale or tuning results to import the certificate.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)