Cosmology Baryon Density Exact2 From Jcost

Baryon density and the cost function

In cosmology, the baryon density parameter Ω_b measures how much ordinary matter (protons, neutrons, electrons) fills the universe, relative to the critical density needed to halt expansion. It is usually quoted as Ω_bh², where h is the Hubble constant in units of 100 km/s/Mpc. The standard measured value from the Planck satellite is about 0.0224.

Recognition Science (RS) attempts to derive such physical constants from a single cost function J(x) = (x + 1/x)/2 - 1, which it proves is the unique function satisfying five plain conditions. The module called BaryonDensityExact2FromJCost defines a cost (a measure of how far two quantities are from being equal) as J(m/e), where m and e are two masses. The machine-checked library of formal theorems proves three general facts about this cost: it vanishes when m equals e, it is never negative for positive inputs, and the golden-ratio-related constant φ - 3/2 is positive.

These three facts are true for any positive numbers m and e. The module proves nothing specific to cosmology, because the definition of the cost does not reference any particular mass, electron mass, or baryon density. The docstring itself states this plainly: it proves nothing specific to this subject. The paragraph above the code is a research note recording where the idea was meant to go, not a result.

The research note attempts a numerical match: it computes J(φ)² × 1/φ = 0.00866, which is off from the measured 0.0224 by a factor of about 2.6. The note labels this "Structural." This is an honest admission that the exact prediction does not land on the measured value. The module therefore establishes only the general properties of the cost function, not the baryon density itself.

What the module does provide is a template. It shows how a cosmological claim would be certified: define m and e in terms of physical quantities, then the same three theorems would apply. Until that definition is made, the baryon density number remains a target, not a derivation. The framework's contribution here is a proof of principle, not a measurement.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The baryon density Ω_b h² = 0.0224 is not derived by this module. The cost function J is not proven to be the unique cost for cosmological baryon density. The value 0.00866 is not a prediction of the framework; it is a research note with an acknowledged 2.6x discrepancy.

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/BaryonDensityExact2FromJCost.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: