canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant is strictly positive. Researchers comparing domain costs or rung gaps on the phi ladder cite this as a basic positivity fact. The argument is a one-line wrapper: unfold the definition, then finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau$, where $\tau$ is the real constant defined (by unfolding) from the golden ratio $\varphi = (1+\sqrt{5})/2$.
background
Module 11 of the RS forcing chain treats rung spacing on the phi ladder: consecutive rungs differ by the fixed factor $\varphi \approx 1.618$. The module is marked structural (zero sorry, zero axioms) and imports the global constants and cost layers.
The golden ratio $\varphi$ is the unique positive root of $x^2 = x+1$. Upstream, phi_gt_onePointFive records the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a real constant built from $\varphi$ (unfolded in the proof); positivity of that constant is the local claim.
Sibling facts in the same file establish nonnegativity and evaluation identities for the associated domain cost, so this positivity lemma sits next to the cost comparison toolkit rather than inside the deep T0–T8 forcing chain.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, exposing an explicit real expression in $\varphi$. Then invoke linarith with the single hypothesis $\varphi > 1.5$ (from phi_gt_onePointFive). No case splits or further lemmas are required.
why it matters
Positivity of the canonical threshold is a structural hygiene fact for RS Module 11 (rung spacing). It guarantees that the threshold used when comparing consecutive phi-rungs or domain costs is a genuine positive scale, not a vacuous or sign-indefinite quantity.
No downstream consumers are recorded yet (used_by is empty), so the lemma presently serves the local certificate RSForcingChain011Cert and any later cost or spacing arguments that need $0 < \tau$. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those live in the T5–T8 segment of the unified forcing chain. It simply keeps the rung-spacing layer free of sign gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.