probability_is_relational

formal source

 195    Formal content: The fiber count (= number of distinct probability bins)
 196    equals the observer's resolution — it is a property of the observer, not
 197    just of the underlying state. -/
 198theorem probability_is_relational :
 199    -- The number of probability bins equals the observer's resolution
 200    ∀ (obs : Observer),
 201    Fintype.card (Fin obs.resolution) = obs.resolution := by
 202  intro obs
 203  simp
 204
 205/-- **Theorem (Propensity Vindicated)**:
 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) ∧