cert_inhabited
plain-language theorem explainer
The structural cosmology certificate for module 002 is inhabited: domain cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is positive. Cosmology proofs that need this package as a single witness cite it. The proof is a one-line term inhabitant built from the concrete certificate record.
Claim. There exists a 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 packages structural facts about the Recognition Science J-cost in a cosmology setting. The module doc fixes the landmark value $J(\varphi)=\varphi-3/2\approx 0.11803$, the golden-ratio recognition cost minimum. Status is structural: zero sorry, zero axioms.
The certificate structure bundles three properties of the local domain cost and threshold. Domain cost is the in-module cost functional on mass-energy pairs; it is required to vanish when the two arguments agree (nonzero), and to be nonnegative on the positive orthant. The canonical threshold is a positive real cutoff used by later structural comparisons.
Upstream, the structure itself only declares those three fields. Sibling lemmas supply the concrete equalities and inequalities that fill a record of that type.
proof idea
Term-mode one-liner. The concrete record cert already inhabits the certificate structure, so Nonempty is witnessed by the anonymous constructor ⟨cert⟩. No tactics, no further lemmas.
why it matters
Gives a single Nonempty witness that the structural package for cosmology module 002 is realized. Downstream consumers can assume the certificate exists without unpacking the three field proofs. The module sits in the RS cosmology layer tied to the J-cost minimum at $\varphi$ (forcing-chain T5/T6: J-uniqueness and the golden fixed point). No used-by edges are recorded yet; the declaration is the inhabitance hook for any later theorem that takes the certificate as a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.