theorem
proved
omega_lambda_lt_one
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.EarlyUniverse on GitHub at line 58.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
modes -
alphaLock -
alphaLock_pos -
alphaLock_pos -
omega_lambda -
of -
is -
of -
from -
is -
of -
is -
of -
Resolution -
is -
density -
Resolution -
Resolution -
constant -
vacuum
used by
formal source
55 linarith
56
57/-- Ω_Λ < 1 (subunitary). -/
58theorem omega_lambda_lt_one : omega_lambda < 1 := by
59 unfold omega_lambda
60 have h_alpha := alphaLock_pos
61 have h_pi := Real.pi_pos
62 linarith [show (0 : ℝ) < alphaLock / Real.pi from div_pos h_alpha h_pi]
63
64/-! ## Cosmological Constant Problem Resolution -/
65
66/-- **D-003 Resolution**: The cosmological constant is NOT the vacuum energy
67 of QFT. It is the fraction of vacuum modes in the ledger.
68
69 The "10^120 discrepancy" dissolves because:
70 1. QFT vacuum energy is a misidentification (not a physical observable)
71 2. The actual Ω_Λ comes from ledger mode counting: 11/16 − α/π
72 3. This is a NUMBER, not an energy density requiring renormalization
73
74 There is no fine-tuning because there is no parameter to tune. -/
75theorem cosmological_constant_resolution :
76 0 < omega_lambda ∧ omega_lambda < 1 :=
77 ⟨omega_lambda_pos, omega_lambda_lt_one⟩
78
79/-! ## EU-001: No Singularity -/
80
81/-- **EU-001 Resolution**: There is no Big Bang singularity.
82
83 1. The initial state is the zero-defect configuration (all entries = 1)
84 2. This state has ZERO total defect (minimum energy)
85 3. Defect = 0 means "nothing to recognize" — the null ledger
86 4. The "Big Bang" is the first tick: when the first nonzero defect appears
87 5. There is no infinite density, no singularity, no breakdown of physics
88