cert_inhabited

This module is the RS Cosmology structural layer (session 3). Its standing claim is that the vacuum equation of state is exactly $w=-1$ from the RS cost structure; any DESI Y3 deviation from $w=-1$ at $2\sigma$ would falsify RS. Current DESI BAO numbers ($w_0\approx -0.95$, $w_a\approx -0.27$) sit in mild tension but not yet at that threshold.

The certificate structure packages three elementary cost facts used as the deep-4 EOS gate: domain cost is zero when mass equals energy (on-shell diagonal, nonzero scale), domain cost is nonnegative for positive arguments, and the canonical threshold is positive. Domain cost is the local cost functional imported from the Cost layer and specialized to cosmological mass/energy pairs; the canonical threshold is the positive cutoff against which that cost is compared.

Upstream, the structure itself is only a Prop-carrying record. Inhabitation is what turns those three fields into a usable certificate object rather than an empty interface.

One-line term proof. The sibling value cert already assembles the three field proofs into an EOSDeep4Cert term; the theorem is just the standard Nonempty introduction ⟨cert⟩. No tactics, no further lemmas.

In the RS Cosmology stack this is the existence seal on the deep-4 EOS certificate: without Nonempty, downstream cosmology arguments cannot assume the cost-diagonal, nonnegativity, and positive-threshold package as a single object. The module frames the parent physics claim as structural and sorry-free: $w=-1$ exactly from the RS vacuum, with DESI Y3 at $2\sigma$ as the external falsifier. No further used-by edges are recorded yet, so the theorem presently closes the certificate layer rather than feeding a named parent theorem. It sits under the broader RS forcing picture only indirectly (cost nonnegativity and on-shell vanishing are Cost-layer consequences of the J-cost calculus), not as a T0–T8 step.