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

observational_tests

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)

 199def observational_tests : List String := [

proof body

Definition body.

 200  "Planck CMB: Ω = 1.0000 ± 0.0002",
 201  "BAO surveys confirm flatness",
 202  "Next-gen: 0.01% precision possible",
 203  "RS predicts exactly 1, not 1.0001 or 0.9999"
 204]
 205
 206/-! ## Connection to Inflation -/
 207
 208/-- RS and inflation are compatible:
 209
 210    1. Inflation is the MECHANISM for achieving flatness
 211    2. RS explains WHY flatness is the endpoint
 212    3. Together: Inflation is J-cost driven toward Ω = 1
 213
 214    The inflaton potential is constrained by J-cost optimization. -/

depends on (11)

Lean names referenced from this declaration's body.