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

FlatnessFalsifier

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)

 243structure FlatnessFalsifier where
 244  omega_not_one : Prop  -- Measured Ω ≠ 1 beyond uncertainty
 245  no_cost_minimum : Prop  -- J-cost doesn't favor flatness
 246  phi_relations_fail : Prop  -- No φ-structure in parameters
 247  falsified : omega_not_one ∨ no_cost_minimum ∨ phi_relations_fail → False
 248
 249end FlatnessProblem
 250end Cosmology
 251end IndisputableMonolith

depends on (2)

Lean names referenced from this declaration's body.