cert_inhabited
plain-language theorem explainer
The cosmology module-5 certificate structure is inhabited: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the r-tensor consistency check (2/(44 φ²) ≈ 0.0174 below the Planck bound 0.036) uses this witness. Proof is a one-line term inhabitant via the packaged certificate.
Claim. There exists a certificate packing three facts: for every nonzero real $r$, the domain cost at $(r,r)$ is zero; for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Module RS_Cosmo_Module_005 is a structural cosmology check in Recognition Science: the r-tensor value $2/(44\phi^2)\approx 0.0174$ lies below the Planck bound $0.036$, marked CONSISTENT with zero sorry and zero axioms.
The certificate structure packages three elementary cost properties. Domain cost is the local cost functional on mass/energy pairs (imported from the Cost layer and Constants, where $\phi$ is the golden ratio forced by T6). Canonical threshold is the positive cutoff used in the module's consistency comparison.
Upstream, the structure itself only records the three propositions; the sibling cert assembles concrete proofs of diagonal vanishing, nonnegativity, and threshold positivity into one value.
proof idea
One-line term proof. Nonempty is inhabited by the anonymous constructor applied to the sibling value cert, which already has type RSCosmo005Cert. No tactics, no further lemmas.
why it matters
Gives a single inhabited certificate that the module-5 cost layer is well-formed before the r-tensor numerical comparison is trusted. Downstream use is currently empty in the graph, so this is a leaf witness rather than a stepping stone to a larger theorem.
In the RS forcing chain it sits under the cosmology side-conditions that keep derived dimensionless ratios inside observational bands (here Planck). It does not itself derive $D=3$, the eight-tick octave, or the J-cost uniqueness (T5–T8); it only certifies that the local cost and threshold used in this module obey the expected algebraic sign and diagonal identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.