cert_inhabited
plain-language theorem explainer
The certificate structure for Recognition Science Cosmology Module 001 is nonempty: it packages diagonal vanishing of the domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Cosmology auditors cite this to discharge existence obligations when wiring the Omega_Lambda match into larger developments. The proof is a one-line term that exhibits the prebuilt certificate instance.
Claim. There exists a certificate recording that the domain cost vanishes whenever its two arguments are equal and nonzero, that the domain cost is nonnegative for positive mass and energy arguments, and that the canonical threshold is strictly positive.
background
Recognition Science Cosmology Module 001 packages a structural match of the dark-energy density parameter. The module states that $\Omega_\Lambda$ equals $11/16 - \alpha/\pi$, numerically $0.685$, agreeing with the Planck value at $0.665\sigma$, and is marked RS_PASS as a structural theorem with zero sorry and zero axioms.
The certificate structure collects three elementary properties of the local cost and threshold: the domain cost of a nonzero ratio against itself is zero; the domain cost of positive mass and energy is nonnegative; and the canonical threshold is positive. These are the minimal positivity and normalization facts needed before any numerical comparison to cosmological data.
proof idea
Term-mode proof. The certificate structure is inhabited by the already-constructed instance packaged in the module, so Nonempty is witnessed by the anonymous constructor applied to that instance. No tactics or intermediate lemmas are required beyond the existence of that packaged certificate.
why it matters
This inhabitation lemma closes the structural side of Cosmology Module 001. The module's headline claim is the $\Omega_\Lambda$ identity $11/16 - \alpha/\pi$ matching Planck $0.685$ within $0.665\sigma$. Downstream consumers that require a nonempty certificate (when composing cosmology modules or discharging existence obligations) can invoke this fact. Within the broader Recognition framework it sits under the cosmology domain rather than the T0-T8 forcing chain, but it inherits the RS-native constants (including $\alpha$) used to form the numerical match. No open scaffolding remains: the module is marked fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.