cert
plain-language theorem explainer
Packages three structural properties of the RS domain cost into a single baryon-density certificate: diagonal vanishing, nonnegativity for positive arguments, and a strictly positive canonical threshold. Cosmologists citing the RS Omega_b construction use this as the inhabited witness. The body is a pure structure assembly of three preexisting lemmas.
Claim. There is a baryon-density certificate consisting of: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
The module treats the cosmic baryon density parameter $\Omega_b\approx 0.0493$ in Recognition Science units. Candidate closed forms are built from the J-cost $J(x)=(x+x^{-1})/2-1$ evaluated at the golden ratio $\phi$, for example $J(\phi)(1-J(\phi))/2\approx 0.052$, which sits near the observed band. Status is structural: zero sorry, zero axiom.
The domain cost is the local cost functional on mass/energy pairs used to score recognition events in this cosmology layer. The certificate structure demands three elementary properties of that cost and of a fixed positive threshold against which densities are compared.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing: any recognition event has cost $\ge 0$ because $J$ is nonnegative on positive reals. The in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that picture to the baryon-density domain.
proof idea
One-line structure assembly. The three fields of BaryonDensityCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass and energy), and canonicalThreshold_pos (strict positivity of the threshold). No new algebra is performed; the definition is the inhabited witness that those three facts hold simultaneously.
why it matters
Gives the module a single named certificate that the RS baryon-density cost layer is well-posed: cost vanishes at matched arguments, never goes negative, and the comparison threshold is positive. That is the structural backbone behind the module claim that $\Omega_b$ can be read off J-cost expressions near $J(\phi)(1-J(\phi))/2\approx 0.049$.
No downstream consumers are wired yet (used_by is empty), so the certificate presently closes the local structural obligation rather than feeding a larger forcing step. It sits in the cosmology domain alongside the phi-ladder mass and density formulae, and is consistent with the global nonnegativity of J-cost from the forcing chain (T5 J-uniqueness). Open numerical question remains which exact closed form in $J(\phi)$ is selected as the physical $\Omega_b$; this certificate does not choose among them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.