probability_meaning_from_ledger

formal source

  71
  72/-! ## Core Probability Claim -/
  73
  74def probability_meaning_from_ledger : Prop :=
  75  ∀ obs : Observer, ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y
  76
  77theorem probability_meaning_structure : probability_meaning_from_ledger := projection_lossy
  78
  79/-- Probability-meaning structure implies lossy projection for any observer. -/
  80theorem probability_meaning_implies_lossy (h : probability_meaning_from_ledger) (obs : Observer) :
  81    ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y :=
  82  h obs
  83
  84/-! ## Probability as Projection Weight -/
  85
  86/-- The fiber of outcome v: set of underlying states that project to v. -/
  87def Fiber (obs : Observer) (v : Fin obs.resolution) : Set ℝ :=
  88  { x | project obs x = v }
  89
  90/-- The fiber partition: every state belongs to exactly one fiber. -/
  91theorem fibers_cover (obs : Observer) (x : ℝ) :
  92    ∃! v : Fin obs.resolution, x ∈ Fiber obs v :=
  93  ⟨project obs x, rfl, fun v hv => hv.symm⟩
  94
  95/-- **Theorem (Probability from Projection)**:
  96    For any observer, distinct underlying states can be indistinguishable.
  97    "Probability" for outcome v = uncertainty about which state in fiber(v)
  98    produced the observation.
  99
 100    This is the RS operational definition of probability:
 101    prob(v) = measure of fiber(v) / total measure -/
 102theorem probability_from_projection (obs : Observer) :
 103    ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y :=
 104  projection_lossy obs