canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the Module 9 cost setup is strictly positive. Anyone comparing domain costs against that threshold, or assembling the Module 9 structural certificate, cites this fact. The proof is a one-line wrapper: unfold the definition and close positivity by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the threshold quantity defined from the golden ratio in this module.
background
Module 9 records the structural fact that Recognition cost is ratio-symmetric: the J-cost satisfies $J(x)=J(1/x)$. In RS units the cost is built from the unique generator $J(x)=(x+x^{-1})/2-1$ forced at T5, and the self-similar scale $\varphi=(1+\sqrt{5})/2$ forced at T6.
The sibling definition canonicalThreshold packages the positive scale cut used when comparing domain costs in this module. Its positivity is not automatic from $\varphi>1$ alone; the proof relies on the tighter Constants bound $\varphi>1.5$, which follows because $\sqrt{5}>2$, hence $(1+\sqrt{5})/2>3/2$.
Upstream, phi_gt_onePointFive states exactly that tighter lower bound and is the sole dependency.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, exposing an arithmetic expression in $\varphi$ whose sign is controlled by $\varphi>1.5$. Discharge the resulting linear inequality with linarith, feeding the lemma phi_gt_onePointFive ($1.5<\varphi$). No further case splits or cost identities are required.
why it matters
Module 9 is marked STRUCTURAL THEOREM (0 sorry, 0 axiom) and packages J-cost ratio symmetry together with the nonnegativity and threshold facts needed for the local certificate RSForcingChain009Cert. Positivity of the canonical threshold is the elementary arithmetic hinge that lets domain-cost comparisons sit above zero rather than float as a signed quantity.
In the broader forcing chain this sits under T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point): once $\varphi$ is forced and bounded below by $1.5$, the threshold cut used by the cost layer is automatically positive. No downstream consumers are recorded yet (used_by is empty), so the lemma presently serves the in-module certificate and any later cost-comparison arguments that import Module 9.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.