canonicalThreshold
plain-language theorem explainer
Defines the canonical cost threshold as φ − 3/2 for the RS human-voice-range certificate. Acoustics and RS-ladder workers cite it when checking that the domain cost stays below the acceptance band for the φ^9–φ^12 Hz window. It is a one-line real constant, not a proved inequality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by the self-similarity equation of Recognition Science.
background
The module treats the human fundamental voice band (roughly 80–300 Hz) as the RS octave window $\varphi^9$ through $\varphi^{12}$ Hz (about 76 Hz bass bottom to 322 Hz soprano top). Recognition Science forces $\varphi$ as the unique self-similar fixed point (forcing step T6) and builds costs from the J-functional $J(x)=(x+x^{-1})/2-1$.
Sibling definitions in the same file introduce a domain cost on that ladder and a non-negativity lemma for it. The present constant is the numerical cut used by those cost checks: values of the domain cost below $\varphi-3/2$ are treated as inside the certified voice range.
proof idea
Pure definitional abbreviation. The right-hand side is the real expression $\varphi - 3/2$ drawn from the Constants import; no tactic or lemma is applied.
why it matters
Supplies the single numeric gate for the structural human-voice-range certificate (module status: 0 sorry, 0 axiom). Downstream siblings such as the positivity lemma for this threshold and the inhabited certificate record rely on the constant being exactly $\varphi-3/2$ so that the $\varphi^9$–$\varphi^{12}$ band sits inside the accepted cost window. It is local scaffolding for the acoustics layer, not a step in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.