cert
plain-language theorem explainer
Packages three elementary properties of the baryogenesis domain cost into a single certificate: vanishing on the diagonal, non-negativity for positive mass and energy, and positivity of the canonical threshold. Cosmology workers citing the J-cost baryogenesis sketch use this as the inhabited witness that the cost side of the story is well-posed. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats baryon asymmetry as a structural consequence of the Recognition Science J-cost. The observed ratio $\eta_B = (n_B - n_{\bar B})/n_\gamma \sim 6\times 10^{-10}$ is approached by expressions built from $J(\varphi)$ and powers of $\varphi$, with residual suppression still under calibration.
Domain cost is the local cost functional on mass-energy pairs used in that sketch. The certificate structure records exactly the three properties needed downstream: the cost vanishes when the two arguments coincide (identity events sit at the J-minimum), stays nonnegative for positive arguments, and the canonical threshold that gates asymmetry production is positive.
Upstream, non-negativity of recognition-event cost is already forced by $J$-cost non-negativity on positive states. The present certificate specializes that discipline to the baryogenesis domain cost and adds the diagonal and threshold facts.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas that already prove diagonal vanishing of domain cost, non-negativity of domain cost on positive arguments, and positivity of the canonical threshold. No extra algebra is performed here.
why it matters
Gives an inhabited, zero-sorry witness that the cost side of the Plan-v7 baryogenesis sketch is structurally sound. The module frames baryogenesis as a J-cost theorem rather than an ad-hoc CP-phase story, tying $\eta_B$ estimates to $J(\varphi)$ and the $\varphi$-ladder (with an acknowledged residual suppression factor still open). No downstream consumers are wired yet; the certificate is the local closure point for the three cost axioms before any numerical $\eta_B$ derivation is attached. It sits in the cosmology layer that inherits T5 J-uniqueness and the RCL from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.