cert
plain-language theorem explainer
Packages three structural facts about the cosmology domain cost into a single certificate: the cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cosmology and forcing-chain readers cite it as the inhabited witness for RS structural module 5. The body is a pure field assembly of three sibling lemmas.
Claim. There is a certificate recording that (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; and (iii) the canonical threshold is strictly positive.
background
Module 5 sits in the RS cosmology structural layer tied to the eight-tick octave: one full traversal of the binary recognition lattice has period $2^D = 8$ (forcing landmark T7, with $D=3$ from T8). Status is structural: zero sorry, zero axiom.
The certificate type bundles three properties of a domain cost functional on pairs of reals. That cost is the local stand-in for the RS J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), which is nonnegative and vanishes only at the identity $x=1$. Upstream, ObserverForcing records that every recognition event has nonnegative cost via $J$-nonnegativity.
Sibling facts supply the three fields: diagonal vanishing of domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold used as a comparison scale in the module.
proof idea
One-line structure instance. Each field of the certificate is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra tactics or rewriting.
why it matters
Gives an inhabited structural certificate for cosmology module 5, so downstream code can depend on a single object rather than three separate lemmas. The module frames the eight-tick lattice traversal (period $2^3=8$), a core RS landmark linking T7 (octave) to T8 ($D=3$). The cost fields echo the global J-cost minimum and nonnegativity used throughout the forcing chain (T5 J-uniqueness and the Recognition Composition Law). No used_by edges are recorded yet; the natural consumer is any cosmology theorem that needs a packaged witness that domain cost is a genuine cost with a positive threshold. Closes the certificate side of a 0-sorry structural module rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.