probability_from_projection

formal source

  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]
 118  simp only [Int.floor_natCast, Int.toNat_natCast]
 119  exact Nat.mod_eq_of_lt v.isLt
 120
 121/-! ## Probability is Epistemic -/
 122
 123/-- **Theorem (Probability is Epistemic)**:
 124    The "randomness" seen by a finite-resolution observer arises from
 125    finite information capacity, not from ontological indeterminism.
 126
 127    Proof: The deterministic structure (unique J-minimizer) is real;
 128    the probabilistic appearance is a consequence of the projection. -/
 129theorem prob_is_epistemic :
 130    -- Reality is deterministic (unique minimum)
 131    (∃! x : ℝ, 0 < x ∧ Foundation.LawOfExistence.defect x = 0) ∧
 132    -- But observers see projections (finite resolution)