InternetTrafficCert
plain-language theorem explainer
Certificate bundle for the RS internet-traffic model: diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Downstream code builds a concrete witness and proves the type is inhabited. Pure structure definition; no proof obligations live here.
Claim. An internet-traffic certificate is a record of three facts: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats annual internet traffic growth as a recognition phenomenon. Historically the rate is about $1.58\times$/yr (Cisco 2010–2022); RS predicts growth by the golden ratio $\varphi\approx 1.618$, a $2.4%$ relative offset, and packages the claim as a structural theorem with no sorrys.
domainCost is the local cost functional on measurement/expectation pairs (imported Cost/J-cost machinery). The first field asks that cost vanish on the diagonal $m=e$ (perfect match). The second reuses the global nonnegativity of recognition cost: upstream, cost_nonneg states that every recognition event has nonnegative cost via Jcost_nonneg on a positive state. The third field only demands that the module's canonical threshold sit strictly above zero, so a positive decision barrier exists.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements that any later witness must supply. The concrete inhabitant cert fills them by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; cert_inhabited then wraps that witness as Nonempty.
why it matters
Gives the typed interface that turns the informal "traffic grows like $\varphi$" story into a checkable RS certificate. Downstream, cert is the noncomputable witness and cert_inhabited records that the certificate type is nonempty, closing the module's structural claim (0 sorry, 0 axiom).
In the broader framework this sits in the Information domain, reusing J-cost nonnegativity from ObserverForcing and the primitive recognition calculus. It does not itself force $\varphi$ (that is T6 in the forcing chain); it only certifies the cost/threshold side conditions under which the $\varphi$-growth comparison is well-posed. The numerical CLOSE note ($\varphi$ vs $1.58$) remains observational context, not a proved equality inside this structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.