OmegaBaryon4Cert
plain-language theorem explainer
Certificate bundling three structural properties used in the RS baryon density fraction: diagonal domain-cost vanishes, domain-cost is nonnegative on positive arguments, and the canonical threshold is positive. Cosmology derivations that pin Omega_b near J(phi)/2 cite this bundle. Pure structure definition; no proof body.
Claim. A baryon-Omega certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module Cosmology.OmegaBaryon4 treats the baryon density fraction as a structural consequence of the phi-ladder. The module status line records Omega_b = 0.049 and notes the RS comparison J(phi)/2 ≈ 0.059, treated as consistent with the observed band.
Domain cost is the local cost functional on a pair of positive reals (mass- and energy-like arguments). The diagonal identity domainCost(r,r) = 0 encodes a zero-defect matched pair. Nonnegativity of domain cost mirrors the global recognition-cost law: upstream, ObserverForcing.cost_nonneg states that the cost of any recognition event is nonnegative, via Jcost_nonneg on a positive state.
The canonical threshold is the positive cutoff against which the baryon fraction is read off; its positivity is part of the certificate interface rather than a numerical evaluation of Omega_b itself.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing, nonnegativity on positive arguments, positive threshold). Inhabitation is supplied downstream by packing the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos into the concrete value cert.
why it matters
Gives the typed interface that the module's Omega_b story must satisfy before any numerical claim is attached. Downstream, cert assembles the three sibling proofs into one inhabitant, and cert_inhabited records Nonempty of the certificate type, closing the structural layer with zero sorry and zero axiom.
In the broader RS chain this sits under cosmology rather than the T0–T8 forcing core, but it reuses the J-cost nonnegativity culture (T5 J-uniqueness background) and the phi-ladder mass/yardstick language. The module explicitly ties the target to J(phi)/2 ≈ 0.059 versus Omega_b ≈ 0.049, so the certificate is the gate that keeps that comparison honest: cost geometry first, number second.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.