probability_meaning_implies_lossy

formal source

  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
 105
 106/-- **Theorem (Each fiber is nonempty)**:
 107    Every possible outcome has at least one underlying state that produces it. -/
 108theorem each_fiber_nonempty (obs : Observer) (v : Fin obs.resolution) :
 109    (Fiber obs v).Nonempty := by
 110  -- Use x = v.val / obs.resolution as witness