canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the RS string-landscape comparison is strictly positive. Landscape and domain-cost arguments in this module cite it whenever a cutoff must sit above zero. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold (the real cutoff built from $\varphi$ in this module) is strictly positive: $0 < T_{\mathrm{can}}$.
background
This module sits in Foundation and treats the string-theory vacuum count (~$10^{500}$) as a structural comparison against an RS phi-power count. Status is a structural theorem (zero sorry, zero axioms). The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6; native constants and costs are built from it.
The only upstream fact used here is the tighter lower bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a local real constant defined from $\varphi$ (unfolded in the proof); sibling lemmas establish nonnegativity and evaluation identities for the related domain cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then close by linarith using the lemma $\varphi > 1.5$. No case split and no further Recognition identities are required; positivity is pure real arithmetic once the definition is expanded.
why it matters
Supplies the positivity half of the cutoff used by the RS string-landscape structural comparison in this file. The module frames the landscape cardinality question as a phi-power count versus the usual ~$10^{500}$ string vacua and marks the development as a structural theorem. Sibling certificates (cert, cert_inhabited) and domain-cost nonnegativity sit next to this fact; together they keep the landscape bookkeeping above zero. No downstream edges are recorded yet, so the lemma is presently a local positivity brick rather than a cited step in T0–T8 or the RCL chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.