born_rule_structure

formal source

 223    This is formalized as: the fiber partition is complete (covers all states)
 224    and each fiber is nonempty. The specific probability weights come from
 225    the J-cost landscape, giving rise to the Born rule. -/
 226theorem born_rule_structure (obs : Observer) :
 227    -- The fibers partition the state space
 228    (∀ x : ℝ, ∃! v : Fin obs.resolution, x ∈ Fiber obs v) ∧
 229    -- Each fiber is nonempty (every outcome is possible)
 230    (∀ v : Fin obs.resolution, (Fiber obs v).Nonempty) :=
 231  ⟨fibers_cover obs, each_fiber_nonempty obs⟩
 232
 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