pith. machine review for the scientific record. sign in
def definition def or abbrev

observationalStatus

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)

 193def observationalStatus : List String := [

proof body

Definition body.

 194  "Λ = (1.1 ± 0.01) × 10⁻⁵² m⁻²",
 195  "w = -1.03 ± 0.03",
 196  "No evidence for w evolution",
 197  "Future: 0.3% precision on w"
 198]
 199
 200/-! ## Alternative Theories -/
 201
 202/-- Other approaches to the Λ problem:
 203
 204    1. **Anthropic**: We observe small Λ because large Λ prevents life
 205    2. **Quintessence**: Dynamic dark energy field
 206    3. **Modified gravity**: f(R), MOND extensions
 207    4. **Holographic**: Λ from holographic bound
 208    5. **RS**: φ-ladder cancellation (this work)
 209
 210    RS is unique in providing a calculable mechanism. -/

depends on (7)

Lean names referenced from this declaration's body.