Cosmology Bbnheliium Exact3 From Jcost

A template, not a result

Primordial helium-4 is the helium forged in the first minutes after the Big Bang, when protons and neutrons fused as the universe cooled. Its abundance is a classic test of cosmology: measurements place the mass fraction at about 0.245, meaning roughly a quarter of ordinary matter by mass ended up as helium-4. The module BBNHeliiumExact3FromJCost carries that number in its name and in a research note, but the machine-checked content does not derive it.

The formal part defines a cost function, a measure of how far a ratio sits from unity, as Jcost (m / e), where m and e are real numbers. It then proves three general facts about this function: it equals zero when the two inputs are equal, it is never negative for positive inputs, and the golden-ratio constant phi exceeds 1.5. These are true for any positive real numbers, with no reference to helium, nucleosynthesis, or cosmology.

The research note above the code sketches the intended connection: it claims Y_p = J(phi) * 2 * phi^0.6 ≈ 0.118 * 2.077 = 0.245, matching the measured value. That arithmetic is a hypothesis about how the cost function might scale to a physical abundance. The note itself says the module proves nothing specific to the subject, because the cost function is defined without any physical input. The same text appears in 2,383 sibling modules; the shared template lives in DomainCostTemplate.

In plain language, the module is a scaffold. It sets up a certificate structure that packages the three general theorems, and proves the certificate exists. What would turn it into a theorem about helium is a definition of m and e in terms of nuclear physics, such as neutron-proton mass ratios or reaction rates. Until that definition exists, the helium match is a research aspiration recorded in a comment, not a derived result.

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)

What this page does not claim

The module does not prove the helium abundance equals 0.245. The module does not define m or e in physical terms. The research note's arithmetic is not a machine-checked result.

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