canonicalThreshold_pos
plain-language theorem explainer
The module's canonical threshold (an RS cutoff built from the golden ratio) is strictly positive. Anyone citing the structural pi–phi relation or its certificate needs this sign fact. The proof is a one-line wrapper: unfold the definition, then linear arithmetic from φ > 1.5.
Claim. The canonical threshold constant of the RS $\pi$–$\varphi$ module is strictly positive: $0 < t_{\mathrm{can}}$, where $t_{\mathrm{can}}$ is defined from the golden ratio $\varphi=(1+\sqrt{5})/2$.
background
This module records a structural RS relation approximating $\pi$ by $4/\sqrt{\varphi}$, with $\varphi$ the golden ratio. Status is a fully proved structural theorem (no sorry, no extra axioms).
The golden ratio satisfies the tighter real bound $\varphi>1.5$, proved from $\sqrt{5}>2$. That lemma is the sole upstream dependency. The canonical threshold is a named real constant in the same file (sibling of the domain cost and the $\pi$–$\varphi$ relation certificate); positivity is the elementary sign fact needed before any comparison or certificate that treats the threshold as a positive scale.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the upstream lemma $\varphi>1.5$. No case split and no further RS identities are required; positivity is pure real arithmetic once the definition is expanded.
why it matters
Positivity of the threshold is local infrastructure for the RS $\pi$–$\varphi$ structural package in this module (siblings include the domain cost, the relation predicate, and an inhabited certificate). The module doc frames the target approximation $\pi\sim 4/\sqrt{\varphi}$ (about 0.15% relative error). In the broader forcing chain, $\varphi$ itself is the self-similar fixed point (T6); a positive threshold built from $\varphi$ is the minimal sign hygiene before any cost or certificate comparison that uses that scale. No downstream edges are recorded yet; the lemma exists so later certificate and relation proofs can quote a proved positivity fact rather than re-deriving it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.