cert
plain-language theorem explainer
Packages a structural certificate for the first cosmology module: domain cost vanishes on the diagonal, stays non-negative for positive mass/energy arguments, and the canonical threshold is strictly positive. Cosmology and RS auditors cite it as the inhabited witness that the module's cost axioms hold. The body is a three-field structure instance wiring existing lemmas.
Claim. There is a structural certificate asserting: (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
This module records the first RS structural cosmology package: the cost is the standard J-cost $J(x)=\frac12(x+1/x)-1$, with $\varphi$ the golden ratio and $D=3$ forced upstream. Status is structural (zero sorry, zero axiom).
Domain cost is the local cost functional on pairs of positive reals (mass/energy style arguments). The certificate structure demands three properties: diagonal vanishing (cost of matching arguments is zero), nonnegativity off the identity for positive inputs, and a strictly positive canonical threshold used as a comparison scale.
Upstream, nonnegativity of recognition cost is already known from observer forcing: every recognition event has nonnegative cost via $J$-cost nonnegativity on positive states. The diagonal and threshold facts are discharged by sibling lemmas in this file.
proof idea
One-line structure instance. Fill cost_at_eq with the sibling domainCost_at_eq, cost_nonneg with domainCost_nonneg, and threshold_pos with canonicalThreshold_pos. No new algebra; pure packaging of three already-proved field obligations.
why it matters
Gives an inhabited value of the structural certificate type for Cosmology RS Structural Module 1, so downstream cosmology developments can assume diagonal vanishing, cost nonnegativity, and a positive threshold without re-proving them. Aligns with the forcing-chain landmarks T5 (J-uniqueness as $\cosh(\log x)-1$), T6 ($\varphi$ fixed point), and T8 ($D=3$). No used_by edges are recorded yet; the declaration is the module's exportable witness rather than a step inside a larger proof. Closes the certificate interface for this structural block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.