canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant is strictly positive. Structural lemmas in the eight-tick RS mathematics module cite this to keep threshold comparisons well-defined and oriented. The proof is a one-line unfold of the definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \mathrm{canonicalThreshold}$.
background
Module RS_MTH_Structural_005 records structural facts for the RS eight-tick: one full traversal of the binary recognition lattice has period $2^D = 8$ (with $D = 3$ from the forcing chain). Status is a pure structural theorem block (no sorry, no axioms).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. The sibling definition canonicalThreshold is a real constant built from $\varphi$ (unfolded in the proof). Upstream, phi_gt_onePointFive supplies the tighter numerical bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$.
proof idea
One-line wrapper: unfold the definition of the canonical threshold, then discharge $0 < \cdots$ by linarith using the lemma $\varphi > 1.5$. No case split or induction; pure real linear arithmetic on the unfolded expression.
why it matters
Keeps the canonical threshold on the positive side of the reals so later comparisons, cost lower bounds, and eight-tick structural certificates in this module remain oriented. Fits the T6/T7 landmark pair: $\varphi$ forced, then the eight-tick octave $2^3 = 8$. No downstream users are wired yet in the graph; the result is local scaffolding for the module certificate RSMTHStructural005Cert and related nonnegativity facts (e.g. domain cost).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.