each_fiber_nonempty

formal source

 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)
 133    (∀ obs : Observer, ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y) :=
 134  ⟨⟨1, ⟨by norm_num, Foundation.LawOfExistence.defect_at_one⟩,
 135    fun y ⟨hy_pos, hy_zero⟩ =>
 136      (Foundation.LawOfExistence.defect_zero_iff_one hy_pos).mp hy_zero⟩,
 137   projection_lossy⟩
 138