cert_inhabited
plain-language theorem explainer
The structural certificate for cosmology module 10 is inhabited: there exists a package asserting diagonal vanishing and nonnegativity of the domain cost plus positivity of the canonical threshold. Cosmology and calibration authors cite it to discharge the module's structural obligations. The proof is a one-line term witness via the packaged certificate value.
Claim. There exists a certificate asserting: (i) the domain cost of any nonzero real $r$ against itself is zero; (ii) the domain cost of any two positive reals is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_COS_Structural_010 is a structural cosmology package in Recognition Science. The module doc fixes the calibration stance: $E_{\mathrm{coh}}$ is set once from the electron mass, after which predictions are parameter-free, and the file is marked as a structural theorem (zero sorry, zero axiom).
The certificate structure bundles three elementary cost facts. Domain cost is the local cost functional on pairs of reals (imported from the Cost layer); the certificate requires it to vanish on the diagonal for nonzero arguments and to be nonnegative on the positive quadrant. The canonical threshold is a positive real scale used as a structural cutoff in the same module.
Upstream, the structure itself is the sole dependency: inhabiting it means exhibiting one value that packs those three propositions.
proof idea
One-line term proof. Nonempty is witnessed by the angle-bracket constructor applied to the already-built certificate value cert, which packages the three field proofs (diagonal vanishing, nonnegativity, threshold positivity). No tactics or further lemmas are invoked at this declaration.
why it matters
This is the inhabitance seal for the module-10 structural certificate. In the RS cosmology stack it records that the cost-side obligations of the structural package are discharged and available as a single nonempty type, consistent with the module claim of a parameter-free calibration after $E_{\mathrm{coh}}$ is fixed by the electron mass.
No downstream consumers are listed yet; the declaration mainly closes the local certificate API so later cosmology theorems can assume the bundle rather than re-prove the three cost facts. It does not itself touch the forcing chain (T0–T8), RCL, or the mass ladder, but it sits in the structural layer those later predictions rely on for cost hygiene.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.