canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio in the RS Standard Model structural layer is strictly positive. Structural-certificate authors for module 6 cite this sign fact when discharging nonnegativity or barrier checks. The proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $T_{\mathrm{can}}$ (the threshold constant defined from the golden ratio $\varphi$ in this module) satisfies $0 < T_{\mathrm{can}}$.
background
This module is Standard Model RS Structural Module 6: it records the structural theorem that $\varphi$ is the self-similar fixed point $\varphi = 1 + 1/(1+1/(1+\cdots))$, with status zero sorry and zero axioms. The local constants layer imports Mathlib together with the RS Constants and Cost modules.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the unique positive solution of $\varphi = 1 + 1/\varphi$. Upstream, the constants library supplies the tighter numerical bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a real quantity defined from $\varphi$ in this file (sibling of the domain-cost definitions); positivity is the elementary sign fact needed before any barrier or certificate packing that mentions it.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then run linear arithmetic with the single lemma $\varphi > 1.5$. After unfolding, the goal is an affine inequality in $\varphi$ that linarith closes from that strict lower bound.
why it matters
Module 6 sits on the phi-uniqueness landmark of the forcing chain (T6: $\varphi$ forced as the self-similar fixed point). This positivity lemma is the elementary sign gate for the structural certificate RSSTDStructural006Cert assembled in the same file. It does not itself prove uniqueness of $\varphi$; it only guarantees that the threshold constant used by that certificate is strictly above zero, so nonnegativity and barrier side-conditions do not collapse. No downstream dependents are recorded yet in the graph; the immediate consumer is the local certificate packing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.