Cosmology Baryogenesis From Jcost Asymmetry Positive Cost

The asymmetry theorem

In cosmology, the baryon-to-photon ratio η ≈ 6.1 × 10⁻¹⁰ measures the tiny surplus of matter over antimatter left over from the early universe. The standard account of how that surplus arose is the Sakharov conditions: baryon number violation, C and CP violation, and departure from thermal equilibrium. Recognition Science (RS) maps those three conditions onto properties of a single mathematical object, the cost function J, a number that measures the price a recognition event pays when the ratio of two quantities moves away from one.

The declaration asymmetry_positive_cost is a proved theorem about that cost function. It states that for any positive real number r not equal to 1, the cost J(r) is strictly greater than zero. In plain words: whenever the ratio of matter to antimatter is not exactly balanced, the cost is positive. The theorem also includes the equilibrium case: when r equals 1, meaning perfect matter-antimatter balance, the cost is exactly zero. These two facts together say that the cost function has a unique zero at balance, and any departure from balance carries positive cost.

The theorem is proved in the framework's machine-checked library of formal theorems, with no unproved assumptions. It is a formal consequence of the cost function's defining properties, not an empirical claim. The library also defines a structure called BaryogenesisCert that packages this asymmetry statement together with a count of five standard baryogenesis mechanisms (leptogenesis, electroweak, Affleck-Dine, cold, GUT), and a proof that the count is exactly five. The certificate is a way of collecting these formal facts in one place.

What the theorem does not claim is essential. It does not say that the cost function causes the matter-antimatter asymmetry, nor that any particular baryogenesis mechanism is correct. It does not derive the measured value of η from first principles. It establishes only a formal correspondence: imbalance implies positive cost, balance implies zero cost. The physical bridge from this mathematical fact to the actual early universe remains an open question, not a proved result.

/-- Asymmetry = J > 0 when matter ≠ antimatter. -/
theorem asymmetry_positive_cost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < Jcost r := Jcost_pos_of_ne_one r hr hne

/-- Equilibrium = matter-antimatter balance (J=0). -/
theorem matter_balance_equilibrium : Jcost 1 = 0 := Jcost_unit0

theorem baryogenesisMechanismCount : Fintype.card BaryogenesisMechanism = 5 := by decide

def baryogenesisCert : BaryogenesisCert where
  five_mechanisms := baryogenesisMechanismCount
  equilibrium := matter_balance_equilibrium
  asymmetry := asymmetry_positive_cost

What this page does not claim

The theorem does not claim that positive cost causes the matter-antimatter asymmetry. It does not derive the measured value of η ≈ 6.1 × 10⁻¹⁰ from the cost function. It does not assert that any particular baryogenesis mechanism is physically correct.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/BaryogenesisFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: