cert_inhabited
plain-language theorem explainer
The structural certificate for RS cosmology module 8 is inhabited: there is a concrete witness packing diagonal vanishing of the domain cost, its nonnegativity on positive masses and energies, and positivity of the canonical threshold. Cosmology and ladder-spacing arguments cite this to obtain a single Nonempty package rather than three separate lemmas. The proof is a one-line term that injects the existing cert value into Nonempty.
Claim. The type of structural certificates for RS cosmology module 8 is nonempty: there exists a record packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) the canonical threshold is strictly positive.
background
Module RS_COS_Structural_008 packages the Recognition Science rung-spacing claim that adjacent rungs differ by the golden ratio factor $\varphi\approx 1.618$. Status is structural: zero sorry, zero axioms.
The certificate structure bundles three elementary cost facts. The domain cost is the local cost functional on mass/energy pairs (imported from the Cost layer); it vanishes on the diagonal and is nonnegative for positive arguments. The canonical threshold is the positive cutoff used to separate rung domains.
Upstream, the structure itself only declares the three fields; the concrete inhabitant cert is assembled from the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
proof idea
One-line term proof. The existing value cert : RSCOSStructural008Cert is injected into Nonempty by the anonymous constructor ⟨cert⟩. No tactics, no further lemmas.
why it matters
Gives a single inhabited certificate for the structural rung-spacing module rather than three loose lemmas. Downstream cosmology developments that need "the module-8 package exists" can pattern-match on Nonempty instead of re-proving diagonal vanishing, nonnegativity, and threshold positivity. Ties directly to the RS phi-ladder (T6: phi forced as self-similar fixed point) and the mass formula's rung index. No used_by edges are recorded yet; the declaration is the terminal existence seal for this structural file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.