canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio is strictly positive. Physicists citing the RS QCD α_s module or any domain-cost comparison that needs a positive scale will invoke this. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < t$, where $t$ is the threshold scale defined from the golden ratio $\varphi$.
background
Physics RS Module 1 packages the structural claim that the QCD running coupling at the Z pole equals the J-cost of φ: $\alpha_s(M_Z)=J(\varphi)\approx 0.11803$, matching the PDG value 0.1180, with status STRUCTURAL THEOREM (zero sorry, zero axiom).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced by the Recognition chain (T6). The Cost import supplies the J-cost $J(x)=(x+x^{-1})/2-1$; the Constants import supplies $\varphi$ and the tighter lower bound $\varphi>1.5$ (from $\sqrt{5}>2$). The canonical threshold is the positive scale assembled from $\varphi$ that this module uses alongside domain-cost comparisons.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the single upstream fact $\varphi>1.5$. No case splits and no further lemmas.
why it matters
Positivity of the canonical threshold is a tiny but necessary arithmetic fact inside the RS Physics Module 1 certificate for the QCD $\alpha_s$ match. The module presents that match as a structural theorem with zero sorry and zero axiom; every comparison that treats the threshold as a positive yardstick needs this inequality first.
No downstream consumers are recorded in the current graph, so the lemma is local scaffolding for the module certificate rather than a shared library fact. It sits next to the φ-ladder and the Berry-scale landmark $\varphi^{-1}$, both of which are positive for the same reason ($\varphi>1$). It does not itself compute $\alpha_s$ or invoke the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.