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

born_rule_structure

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)

 226theorem born_rule_structure (obs : Observer) :
 227    -- The fibers partition the state space
 228    (∀ x : ℝ, ∃! v : Fin obs.resolution, x ∈ Fiber obs v) ∧
 229    -- Each fiber is nonempty (every outcome is possible)
 230    (∀ v : Fin obs.resolution, (Fiber obs v).Nonempty) :=

proof body

Term-mode proof.

 231  ⟨fibers_cover obs, each_fiber_nonempty obs⟩
 232
 233/-! ## Probability Axioms Satisfied -/
 234
 235/-- A finite counting probability over outcomes for a finite observation. -/

depends on (16)

Lean names referenced from this declaration's body.