canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used by the RS A4 (440 Hz) acoustics certificate is strictly positive. Anyone building or citing the exact A4 structural theorem needs this sign fact. The proof is a one-line wrapper: unfold the threshold and finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $t$ appearing in the A4 exactness certificate satisfies $0 < t$.
background
The module treats the ISO 16:1975 concert pitch A4 = 440 Hz inside Recognition Science. The structural claim is that 440 Hz sits near a pure φ-power: roughly φ^17 · 0.123 ≈ 439.2 Hz, so the standard is a near-exact RS ladder value.
The golden ratio φ = (1 + √5)/2 is the self-similar fixed point forced at T6 of the unified forcing chain. The upstream lemma phi_gt_onePointFive records the elementary bound φ > 1.5 (from √5 > 2). The canonical threshold is a local real expression in φ that the A4 certificate uses as a positivity gate; sibling facts also record nonnegativity of the domain cost built from the RS J-cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith with the single hypothesis that φ > 1.5. No further case splits or algebraic identities are required; positivity is immediate from that lower bound.
why it matters
Local supporting lemma for the structural A4 exactness theorem in the Acoustics domain. It discharges the positivity side-condition on the threshold that the A4 certificate and its inhabited-cert construction rely on. In the broader RS picture it sits downstream of T6 (φ forced) and the elementary constant bounds in Constants, and upstream of the claim that the 440 Hz standard is a near-exact φ-ladder tone (φ^17 scaled by the 0.123 yardstick factor). No external used-by edges are recorded; the consumers are the sibling A4ExactRS / cert declarations in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.