canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the RS middle-C frequency construction is strictly positive. Anyone citing the acoustics ladder match (φ-powers against 261.63 Hz) needs this positivity side condition. The proof is a one-line unfold-plus-linarith wrapper off the bound φ > 1.5.
Claim. The canonical threshold $\tau$ appearing in the RS middle-C frequency module satisfies $0 < \tau$.
background
This module fixes middle C at 261.63 Hz and compares it to an RS φ-ladder frequency of the form φ^k (Hz), with a numerical match near φ^14 scaled by a small factor (~0.31). The golden ratio φ = (1+√5)/2 is the self-similar fixed point forced at T6 in the Recognition forcing chain.
The local object canonicalThreshold is a real scalar built from φ that gates or normalizes the acoustics cost comparison. Its only upstream dependency here is the tighter lower bound φ > 1.5 (from √5 > 2), which is stronger than the elementary φ > 1 and is enough for linear arithmetic to conclude positivity after unfolding the definition.
The module is marked structural (zero sorry, zero axiom) and sits in the Acoustics domain of the RS mirror, importing Constants and Cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith with the single lemma φ > 1.5. No case splits, no nonlinear rewriting: after unfold the goal is a linear inequality in φ that follows immediately from that bound.
why it matters
Positivity of the canonical threshold is a hygiene lemma for the RS middle-C frequency certificate: downstream constructions that treat the threshold as a scale, gap, or cost floor need 0 < τ before they can compare φ-ladder rungs to the observed 261.63 Hz. The module doc frames the target match as φ^14 · 0.31 Hz ≈ 261.3 Hz against middle C.
No used_by edges are recorded yet, so this is presently a leaf positivity fact inside the acoustics certificate stack (siblings include the domain cost, the middle-C frequency RS value, and the inhabited certificate). It anchors the φ-ladder acoustics story to the same φ forced at T6, rather than an ad-hoc positive constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.