canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold in the RS internet-traffic model is strictly positive. Anyone assembling or citing the structural certificate that annual traffic growth tracks φ needs this fact. The proof is a one-line wrapper: unfold the threshold definition, then finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold $t$ built from the golden ratio $\varphi$ in the RS internet-traffic model satisfies $0 < t$.
background
The module treats historical internet traffic growth (Cisco 2010–2022, about 1.58×/yr) against the RS prediction that the natural annual growth factor is the golden ratio $\varphi = (1+\sqrt{5})/2 \approx 1.618$. The comparison is packaged as a structural certificate with no sorry and no extra axioms.
The golden ratio enters through Constants and the cost layer. The only upstream fact used here is the tighter lower bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. That bound is stronger than the usual $\varphi > 1$ and is exactly what linear arithmetic needs after the threshold definition is unfolded.
Sibling definitions in the module introduce a domain cost, the canonical threshold itself, and an InternetTrafficCert record that packages the comparison.
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 cost identities are required; positivity is pure arithmetic once the definition is open.
why it matters
Positivity of the canonical threshold is a tiny but necessary lemma inside the structural internet-traffic certificate: without $t > 0$ the certificate record and its inhabited instance cannot be assembled cleanly. The module frames the claim as a structural theorem (0 sorry, 0 axiom) comparing observed ~1.58×/yr growth to the RS value $\varphi \approx 1.618$ (about 2.4% relative gap).
In the broader framework this sits on the information side rather than the T0–T8 forcing chain; it re-uses $\varphi$ as the self-similar fixed point (T6) and the same constant layer that supplies $c$, $\hbar$, and $G$ in RS-native units. No downstream theorems currently depend on it outside this module, so its role is local scaffolding for the traffic certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.