obs_probability

formal source

 233/-! ## Probability Axioms Satisfied -/
 234
 235/-- A finite counting probability over outcomes for a finite observation. -/
 236noncomputable def obs_probability (obs : Observer) (v : Fin obs.resolution) : ℝ :=
 237  (1 : ℝ) / obs.resolution
 238
 239/-- **Theorem (Probabilities Sum to One)**:
 240    The observation probabilities sum to 1 over all outcomes. -/
 241theorem probability_sums_to_one (obs : Observer) :
 242    ∑ v : Fin obs.resolution, obs_probability obs v = 1 := by
 243  simp only [obs_probability, Finset.sum_const, Finset.card_fin]
 244  rw [nsmul_eq_mul]
 245  have hN : (obs.resolution : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp obs.res_pos)
 246  field_simp [hN]
 247
 248/-- **Theorem (Probabilities are Non-negative)**:
 249    Each observation probability is non-negative. -/
 250theorem probability_nonneg (obs : Observer) (v : Fin obs.resolution) :
 251    0 ≤ obs_probability obs v := by
 252  unfold obs_probability
 253  positivity
 254
 255/-! ## Summary Certificate -/
 256
 257/-- **PH-006 Certificate**: The meaning of probability.
 258
 259    RESOLVED: Probability = J-cost projection weight.
 260
 261    1. Reality is deterministic (unique J-minimizer) — no ontic probability
 262    2. Observations are projections through finite-resolution observers
 263    3. "Probability" = the fiber structure of the projection map
 264    4. Born rule emerges from the fiber partition structure
 265    5. All four interpretations are partially correct:
 266       - Frequentist: long-run frequencies are objective (fiber structure)