Pith. sign in
def

canonicalThreshold

definition
show as:
module
IndisputableMonolith.Acoustics.Middle_C_Frequency_RS
domain
Acoustics
line
20 · github
papers citing
none yet

plain-language theorem explainer

Defines the canonical acoustic cost threshold as the golden ratio minus three-halves. Acoustics and RS-constants workers cite it when fixing the acceptance band for middle-C frequency matching on the phi ladder. The body is a one-line real constant definition.

Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by the Recognition self-similarity equation.

background

Recognition Science forces the golden ratio $\varphi$ as the unique self-similar fixed point of the cost functional (forcing step T6). In the acoustics module the same $\varphi$ supplies the frequency ladder: candidate pitches are of the form $\varphi^k$ Hz, scaled by a small dimensionless factor so that middle C lands near 261.63 Hz.

The module works in RS-native units imported from Constants and Cost. Domain cost is the non-negative J-cost evaluated on frequency ratios; a threshold on that cost decides whether a ladder rung is accepted as an audible match. The present constant is the numerical cut used for that decision.

proof idea

Pure definition: the real constant is introduced by the single arithmetic expression $\varphi - 3/2$. No proof obligations arise at the definition site; positivity and later inequalities are discharged by sibling lemmas.

why it matters

Supplies the fixed numerical gate that the middle-C frequency certificate (MiddleCFreqRS and its cert) must clear. Without an explicit threshold the structural claim that $\varphi^{14}$ scaled by a small factor reproduces 261.63 Hz would remain informal. The value sits downstream of T6 ($\varphi$ uniqueness) and upstream of the zero-sorry acoustics certificate that the module advertises as a structural theorem.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.