Fiber

formal source

  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
 111  use (v.val : ℝ) / (obs.resolution : ℝ)
 112  unfold Fiber project
 113  simp only [Set.mem_setOf_eq, Fin.ext_iff, Fin.val_mk]
 114  have hN : (obs.resolution : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp obs.res_pos)
 115  have hmul : (v.val : ℝ) / obs.resolution * obs.resolution = v.val := by
 116    field_simp
 117  simp only [hmul]