canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio is strictly positive. Foundation proofs that need a positive φ-scale (domain-cost bounds, recognition thresholds) cite this fact. The argument is a one-line wrapper: unfold the definition and finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the module's φ-dependent threshold constant.
background
This module records the algebraic identity $\varphi^2 = \varphi + 1$ and immediate consequences (the Fibonacci-style recurrence $\varphi^n = \varphi^{n-1} + \varphi^{n-2}$). Here $\varphi = (1+\sqrt{5})/2$ is the unique positive root of $x^2 - x - 1 = 0$, forced in the RS chain as the self-similar fixed point (T6).
The canonical threshold is a sibling definition in the same file, alongside the domain-cost functional. Its positivity is the elementary scale fact needed before cost nonnegativity and certificate packing.
The sole upstream input is the tighter lower bound $\varphi > 1.5$ (from $\sqrt{5} > 2$), stated as: "Tighter lower bound: φ > 1.5 (since √5 > 2, so (1 + √5)/2 > 1.5)."
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ from phi_gt_onePointFive. No further case splits or algebraic identities are required; positivity is immediate from the linear inequality after unfolding.
why it matters
Positivity of the canonical threshold is a structural lemma in the φ-square identity layer of Foundation. It underwrites the domain-cost nonnegativity siblings and the PhiSqIdentCert certificate inhabitation in the same module. In the broader forcing chain it sits under T6 (φ forced as the self-similar fixed point) and supplies a positive scale consistent with RS-native thresholds such as the Berry creation scale $\varphi^{-1}$. No downstream dependents are wired yet; the lemma is available for any later bound that needs $T_{\mathrm{can}} > 0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.