canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold attached to RS rung spacing is a strictly positive real. Structural arguments in Mathematics RS Module 8 that compare domain costs against this cutoff cite the fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau$, where $\tau$ is the real constant defined in this module from the golden ratio $\varphi=(1+\sqrt{5})/2$ (the self-similar rung factor).
background
Mathematics RS Structural Module 8 records rung-spacing facts: adjacent rungs on the Recognition ladder differ by the fixed factor $\varphi\approx 1.618$. The module is marked structural (zero sorry, zero axiom).
The golden ratio enters from Constants. A tight elementary bound used here is $\varphi>1.5$, proved from $\sqrt{5}>2$, hence $(1+\sqrt{5})/2>3/2$. The canonical threshold is the module-local real built from $\varphi$ against which domain-cost comparisons are stated; siblings package nonnegativity of the domain cost and an equality form at evaluation points.
No deeper forcing-chain machinery is required at this declaration: positivity is pure real arithmetic once the definition is opened.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (exposing an affine expression in $\varphi$), then invoke linarith with the upstream lemma $\varphi>1.5$. Linear arithmetic closes the strict inequality $0<\tau$ immediately; no case splits or nonlinear estimates appear.
why it matters
Fills the positivity half of the structural certificate for Module 8 (rung spacing by $\varphi$). Downstream the module assembles RSMTHStructural008Cert / cert_inhabited so the whole file can be cited as a closed structural block.
In the broader framework this sits under the $\varphi$-ladder: T6 forces $\varphi$ as the self-similar fixed point, and adjacent-rung separation by $\varphi$ is the discrete skeleton behind mass rungs and threshold comparisons (Berry-scale cutoffs live on the same ladder). The lemma itself is elementary, but without it the certificate cannot claim a usable positive cutoff.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.