canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the golden-angle module is strictly positive. Anyone comparing domain costs or certifying the golden-angle threshold cites this fact. The proof is a one-line unfold of the definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold (the real constant defined from the golden ratio $\varphi$ in this module) satisfies $0 < \tau_{\mathrm{can}}$.
background
The module fixes the golden angle in Recognition Science units: $\theta_G = 2\pi(1-1/\varphi) = 2\pi,\varphi^{-2}$, the classical phyllotaxis angle (about $137.508^\circ$). Status is structural: zero sorry, zero axioms.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is imported from Constants. The only upstream fact used here is the tighter lower bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. Sibling definitions introduce a domain cost and the canonical threshold built from $\varphi$; nonnegativity and positivity of those quantities are the local lemmas of the file.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ supplied by phi_gt_onePointFive. No further case splits or algebraic identities are required once the definition is expanded.
why it matters
Positivity of the canonical threshold is the elementary gate that lets later golden-angle certificates treat the threshold as a genuine positive scale rather than a formal symbol. The module pairs it with domain-cost nonnegativity and the inhabited certificate GoldenAngleCert / cert. In the broader RS chain it sits under the forced self-similar fixed point $\varphi$ (T6) and the geometric constants built from powers of $\varphi$; it does not itself advance T5–T8, but keeps the golden-angle layer free of sorry. No downstream theorems currently depend on it in the graph, so it is infrastructure for the local certificate rather than a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.