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

ph006_probability_certificate

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)

 273theorem ph006_probability_certificate :
 274    -- Reality is deterministic
 275    (∃! x : ℝ, 0 < x ∧ Foundation.LawOfExistence.defect x = 0) ∧
 276    -- Probability arises from projection
 277    (∀ obs : Observer, ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y) ∧
 278    -- Fibers cover all states
 279    (∀ obs : Observer, ∀ x : ℝ, ∃! v : Fin obs.resolution, x ∈ Fiber obs v) ∧
 280    -- Each outcome is possible
 281    (∀ obs : Observer, ∀ v : Fin obs.resolution, (Fiber obs v).Nonempty) :=

proof body

Term-mode proof.

 282  ⟨⟨1, ⟨by norm_num, Foundation.LawOfExistence.defect_at_one⟩,
 283    fun y ⟨hy_pos, hy_zero⟩ =>
 284      (Foundation.LawOfExistence.defect_zero_iff_one hy_pos).mp hy_zero⟩,
 285   projection_lossy,
 286   fibers_cover,
 287   each_fiber_nonempty⟩
 288
 289end ProbabilityMeaningStructure
 290end Philosophy
 291end IndisputableMonolith

depends on (19)

Lean names referenced from this declaration's body.