Cosmology Cosmology

The module's scope

In physics, cosmology is the study of the universe's origin, large-scale structure, and evolution. The module IndisputableMonolith/Cosmology/Cosmology.lean does not attempt that. Its own docstring says so plainly: the file proves three general facts about a cost function, and nothing specific to any physical subject.

The central object is domainCost, defined as the recognition cost (a measure of mismatch between two quantities) of the ratio m / e, where m and e are real numbers. The three proved facts are: the cost is zero when m = e, the cost is never negative for positive inputs, and the number phi - 3/2 (where phi is the golden ratio) is positive. These are general properties of the cost function itself, not claims about the universe.

The module also defines a structure EOSDeep4Cert that packages those three facts, and proves that such a certificate exists. The docstring notes that the same body is shared verbatim with 2383 sibling modules; the content is stated once, universally quantified, in a template file. The module would become a theorem about cosmology only if m and e were defined in cosmological terms, which they are not.

The docstring includes a research note: it records that the intended direction was to relate the cost to the dark energy equation of state, with w = -1 exactly from the framework's vacuum. It also states a falsifiable prediction: any DESI Y3 deviation from w = -1 at 2 sigma would falsify the framework's cosmological application. Current DESI data show mild tension, not yet at that threshold. This is a hypothesis, not a proved 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]

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)

structure EOSDeep4Cert where
  cost_at_eq : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  threshold_pos : 0 < canonicalThreshold

What this page does not claim

The module does not prove any cosmological fact, such as the expansion rate or dark energy density. The module does not derive w = -1; it only records a research note and a falsifiable prediction. The module does not establish that the golden ratio appears in cosmology; it only proves phi - 3/2 is positive.

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