pith. machine review for the scientific record. sign in
theorem proved term proof

Lambda_no_fine_tuning

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 151theorem Lambda_no_fine_tuning : Omega_Lambda_RS = 11/16 - (alpha / Real.pi) := rfl

proof body

Term-mode proof.

 152
 153/-! ## C-010: Hubble Tension Connection -/
 154
 155/-- **THEOREM C-010.9**: H_0 is determined by Ω_Λ (via Friedmann equations).
 156
 157    If Ω_Λ is fixed by RS structure, then H_0 is also fixed.
 158    The Hubble tension may reflect:
 159    1. Calibration issues
 160    2. Local vs global structure differences
 161    3. Evolving vacuum energy (quintessence-like) -/

depends on (10)

Lean names referenced from this declaration's body.