cert
plain-language theorem explainer
Packages three elementary properties of the solar-metallicity domain cost into a single certificate: diagonal vanishing, non-negativity for positive mass/energy, and a positive canonical threshold. Cosmology auditors cite it as the inhabited witness that Module 10 is structurally well-formed. The body is a pure structure assembly from three sibling lemmas.
Claim. There exists a certificate asserting: (i) the domain cost of any nonzero ratio against itself is zero; (ii) for positive mass and energy parameters the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 10 targets the solar metallicity match $J(\varphi)^2 \approx 0.01393 \sim Z_\odot = 0.014$, recorded as a structural theorem with no sorries. The domain cost is the local cost functional on mass/energy ratios used to score that match; the canonical threshold is the positive cutoff against which the cost is compared.
The certificate structure RSCosmo010Cert bundles exactly three obligations: the cost vanishes on the diagonal $r\neq 0$, stays nonnegative for positive arguments, and the threshold is positive. Upstream, non-negativity of recognition cost is the standard $J$-cost fact that any recognition event has cost $\ge 0$ (from ObserverForcing / Cost), which the domain-cost non-negativity lemma specializes.
$ J$ is the unique cost from the forcing chain (T5): $J(x)=(x+x^{-1})/2-1$. Here it enters only through the metallicity identity quoted in the module header.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra or tactics: pure field assignment into RSCosmo010Cert.
why it matters
Gives Module 10 an inhabited structural certificate so downstream cosmology code can assume the domain-cost axioms without re-proving them. The module header frames the scientific claim as the solar-metallicity match $J(\varphi)^2\sim Z_\odot$; this definition does not prove the numerical match, only the cost-theoretic scaffolding around it.
No used_by edges are recorded yet, so the certificate is presently a leaf witness. It sits in the broader RS pattern of packing local cost axioms (diagonal zero, non-negativity, positive threshold) before quoting phenomenological equalities. Relates to the T5 $J$-uniqueness landmark only indirectly, via the metallicity formula in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.