canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio in the RS structural foundation is strictly positive. Structural certificates and domain-cost arguments in this module cite it as a positivity lemma. The proof is a one-line wrapper: unfold the definition, then linear arithmetic from φ > 1.5.
Claim. The canonical threshold $t$ (the module's fixed threshold built from the golden ratio $\varphi$) satisfies $0 < t$.
background
This module is Foundation RS Structural Module 1: it records the structural package $J(x)=\frac12(x+1/x)-1$, $\varphi$ the golden ratio, and $D=3$ forced, with status STRUCTURAL THEOREM (0 sorry, 0 axiom).
The golden ratio is $\varphi=(1+\sqrt5)/2$. The only upstream fact used here is the tighter lower bound $\varphi>1.5$, proved from $\sqrt5>2$ (since $2^2<5$). After unfolding, the canonical threshold is an explicit real expression in $\varphi$ whose positivity is then elementary from that bound.
Sibling material in the same file defines domain cost, nonnegativity of that cost, and the threshold itself; this lemma is the positivity half of that local package.
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 RS-specific identities are needed once the definition is open.
why it matters
Keeps the structural foundation free of floating positivity obligations: any later argument that needs the canonical threshold as a strictly positive scale can cite this rather than re-deriving $\varphi>3/2$. The module's certificate objects (RSFDNStructural001Cert, cert_inhabited) sit alongside it as the packaged structural claim.
In the broader Recognition chain this sits under the foundation layer that forces $J$, $\varphi$, the eight-tick octave, and $D=3$ (T5–T8). It does not itself force those landmarks; it only discharges positivity of the local threshold once $\varphi$ is fixed. Currently no downstream theorems list it as a dependency, so its role is local hygiene inside the structural certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.