cert
plain-language theorem explainer
Packages a gas-viscosity domain certificate: the domain cost vanishes on equal arguments, is nonnegative for positive inputs, and the canonical threshold is positive. Anyone auditing the φ-ladder claim that each temperature step multiplies gas viscosity by √φ would cite this witness. It is a structure instance wiring three already-proved sibling lemmas into one record.
Claim. A gas-viscosity certificate exists: the domain cost of any nonzero ratio against itself is zero; the domain cost of positive mass and energy arguments is nonnegative; and the canonical threshold is strictly positive.
background
The module treats classical kinetic-theory gas viscosity $\eta\propto T^{1/2}$ inside Recognition Science units. The structural claim is that a single $\varphi$-step in temperature multiplies viscosity by $\sqrt{\varphi}\approx 1.272$: $\eta(\varphi T_{\mathrm{ref}})/\eta(T_{\mathrm{ref}})=\varphi^{1/2}$.
The certificate structure collects three elementary domain facts used by that scaling story: the domain cost vanishes on the diagonal (equal nonzero arguments), stays nonnegative for positive inputs, and the module's canonical threshold is positive. Upstream, nonnegativity of recognition cost is already forced by the J-cost minimum ($J(x)=(x+x^{-1})/2-1$), via the observer-forcing lemma that every recognition event has nonnegative cost.
Sibling lemmas supply exactly the three fields: diagonal vanishing, nonnegativity of the domain cost, and positivity of the threshold.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas already proved in-module: diagonal vanishing of the domain cost, nonnegativity of the domain cost on positive arguments, and positivity of the canonical threshold. No extra algebra is performed here.
why it matters
Gives a single inhabited certificate object for the gas-viscosity $\varphi$-ladder module (status: structural theorem, zero sorry). Downstream consumers can take the record rather than re-proving diagonal vanishing, cost nonnegativity, and threshold positivity separately. The module ties this to the kinetic-theory square-root temperature law rewritten as a pure $\varphi$-step: each temperature rung multiplies $\eta$ by $\sqrt{\varphi}$. That sits in the broader RS constants and ladder story ($\varphi$ forced at T6, J-cost uniqueness at T5) without yet deriving transport coefficients from the eight-tick or $D=3$ forcing steps. No external used-by edges are recorded yet; the immediate consumer is the in-module inhabitedness witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.