cert
plain-language theorem explainer
Inhabited certificate for Cosmology Module 001 packing three domain-cost facts: diagonal vanishing, nonnegativity, and a positive canonical threshold. Cosmology auditors citing the structural RS_PASS for Ω_Λ ≃ 0.685 use this bundle. The definition is a pure structure assembly wiring three sibling lemmas into the certificate fields.
Claim. There is a certificate whose three fields assert: (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
Module RS_Cosmo_Module_001 is the first cosmology structural unit in the Recognition Science mirror. Its header claim is the dark-energy density match $\Omega_\Lambda = 11/16 - \alpha/\pi \approx 0.685$, reported at $0.665\sigma$ versus Planck and marked RS_PASS with zero sorry and zero axioms.
The certificate structure RSCosmo001Cert packages three elementary cost properties that any later numerical or forcing argument in this module is allowed to assume: the domain cost vanishes on the diagonal away from zero, stays nonnegative on the positive quadrant, and sits above a strictly positive canonical threshold. Domain cost is the local cost functional used in this cosmology layer; nonnegativity is the same qualitative fact as the foundation lemma that every recognition-event cost is $\ge 0$ (via $J$-cost nonnegativity at positive state).
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos already discharge those three propositions; this definition only names a single inhabited witness.
proof idea
Pure structure construction, not a tactic proof. The three fields of RSCosmo001Cert are filled by direct assignment:
cost_at_eqfrom the siblingdomainCost_at_eq,cost_nonnegfrom the siblingdomainCost_nonneg(aligned with foundationcost_nonneg/ $J$-cost nonnegativity),threshold_posfrom the siblingcanonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives the module a single named certificate object so downstream cosmology developments can depend on one inhabitant rather than three scattered lemmas. The module doc frames this layer as the structural theorem behind the $\Omega_\Lambda$ match $11/16 - \alpha/\pi \approx 0.685$ (Planck-compatible, RS_PASS). In the broader RS chain the cost nonnegativity field is the cosmology-side echo of $J$-cost nonnegativity from the forcing/observer layer (T5 $J$-uniqueness lineage). No used_by edges are recorded yet; the immediate consumer in-module is the inhabitedness witness cert_inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.