canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold (an explicit real built from the golden ratio) is strictly positive. Structural arguments in the RS count-law module that need a positive cutoff cite this fact. The proof is a one-line wrapper: unfold the definition, then linear arithmetic from φ > 1.5.
Claim. The canonical threshold $t$, defined from the golden ratio $\varphi=(1+\sqrt{5})/2$, satisfies $0 < t$.
background
This module records structural facts for the RS count law: with configuration dimension $D=3$, one has $2^D-1=7$ independent channels. Status is a closed structural theorem (no sorry, no extra axioms).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the foundation chain. The canonical threshold is a named real constant in this file, built by unfolding from $\varphi$ (sibling of the nonnegativity and evaluation lemmas for the domain cost).
The only upstream input is the tighter bound $\varphi>1.5$, obtained from $\sqrt{5}>2$ so that $(1+\sqrt{5})/2>3/2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold to an explicit linear expression in $\varphi$, then discharge $0<\ldots$ by linarith using the lemma $\varphi>1.5$. No case split and no further RS identities.
why it matters
Keeps the structural certificate of this module on a positive cutoff rather than an unsigned constant. The module packages the RS count law $2^D-1=7$ forced by $D=3$ (forcing landmark T8). Positivity is the minimal arithmetic fact needed before any comparison against domain cost or channel counting can be stated with a strict inequality.
No downstream theorems are wired yet in the graph; the immediate consumers are the local certificate constructors in the same file. The result is pure real arithmetic on $\varphi$, not a new physical derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.