cert
plain-language theorem explainer
Packages three structural properties of the internet-traffic domain cost into one certificate: diagonal vanishing, non-negativity off the diagonal, and a positive canonical threshold. Anyone citing the RS claim that annual traffic growth tracks φ reaches for this bundle. The definition is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate asserting that the internet-traffic domain cost $C$ satisfies $C(r,r)=0$ for every $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold is strictly positive.
background
The module treats annual internet traffic growth as an RS information-domain observable. Historically the Cisco series (2010–2022) sits near $1.58\times$/yr; RS predicts growth at the golden ratio $\varphi\approx 1.618$, about $2.4%$ off. Status is structural: zero sorry, zero axioms.
The domain cost is the local cost functional comparing a measured rate $m$ to an expected rate $e$. Its diagonal vanishing and non-negativity mirror the global J-cost facts from the recognition layer: the upstream result cost_nonneg states that every recognition event has non-negative cost, via non-negativity of $J$. The canonical threshold is the positive cutoff used to decide when a growth mismatch is recognized as a defect.
InternetTrafficCert is the structure that packages exactly those three propositions. The present definition supplies one inhabited instance.
proof idea
Pure structure construction. The three fields of InternetTrafficCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra or tactics; the body is field assignment only.
why it matters
Gives a single named witness that the internet-traffic cost obeys the same structural axioms used elsewhere in the information layer (vanishing on match, non-negativity, positive threshold). That witness is what makes the module's "structural theorem" claim checkable: the certificate is inhabited and the three properties are proved, not assumed.
In the broader RS picture this sits under the information-domain reading of $\varphi$-scaling (primer: $\varphi$ forced at T6 as the self-similar fixed point). The module's numerical claim is that traffic multiplies by roughly $\varphi$ per year; the certificate does not prove the numerics, but it locks the cost side so downstream comparisons to $\varphi$ rest on a clean non-negative defect. No downstream consumers are wired yet; the immediate sibling is the inhabitedness lemma for the same type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.