theorem
proved
tactic proof
each_fiber_nonempty
show as:
view Lean formalization →
formal statement (Lean)
108theorem each_fiber_nonempty (obs : Observer) (v : Fin obs.resolution) :
109 (Fiber obs v).Nonempty := by
proof body
Tactic-mode proof.
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. -/