cert
plain-language theorem explainer
Packages three structural facts about the baryon-domain cost into a single certificate: diagonal vanishing, non-negativity, and a positive canonical threshold. Cosmologists citing the RS Omega_b ≈ 0.049 match (via J(φ)/2) use this as the inhabited witness. The body is a pure structure constructor wiring three sibling lemmas.
Claim. There exists a certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{cost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module derives the baryon density parameter $\Omega_b\approx 0.049$ from the $\varphi$-ladder. Recognition Science compares this to half the J-cost at the golden ratio, $J(\varphi)/2\approx 0.059$, treated as a structural consistency check rather than a fitted parameter.
Domain cost is the local cost functional on mass/energy-like coordinates used in this cosmology layer; the certificate demands it be a true cost (zero on matched arguments, non-negative off-diagonal). The canonical threshold is the positive cutoff against which the baryon-sector cost is compared.
Upstream, non-negativity of recognition cost is already forced in ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost non-negativity for positive states. The present certificate specializes that discipline to the baryon domain.
proof idea
One-line structure inhabitant. Fields are filled by three in-module lemmas: diagonal vanishing (domainCost_at_eq), non-negativity for positive arguments (domainCost_nonneg), and positivity of the canonical threshold (canonicalThreshold_pos). No extra tactics or algebraic work.
why it matters
Gives the inhabited OmegaBaryon4Cert that the module's structural theorem rests on: $\Omega_b=0.049$ aligned with $J(\varphi)/2\approx 0.059$. In the RS forcing chain this sits downstream of T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point), since the numerical comparison is meaningless without those identifications.
No downstream dependents are recorded yet; the certificate is the local closure object for the baryon-omega v4 pass (Plan v7, 119th). It keeps the module at 0 sorry / 0 axiom by packaging the three cost axioms the cosmology argument needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.