bayesian_vindicated

formal source

 162
 163    This is the formal content of Bayesian subjectivism: same underlying state,
 164    different probabilities, because different observers have different resolutions. -/
 165theorem bayesian_vindicated :
 166    -- Every observer conflates distinct states (information is lost)
 167    -- This means probability depends on the observer's information state
 168    ∀ (obs : Observer),
 169    ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y := by
 170  intro obs
 171  exact projection_lossy obs
 172
 173/-- **Theorem (Resolution Increases Precision)**:
 174    Both a low-resolution and a high-resolution observer are lossy,
 175    but the high-resolution observer has finer fiber structure.
 176    This is the Bayesian "learning = refinement" claim.
 177
 178    Formalization: Both observers conflate some states, but the number of
 179    distinct fibers (= distinct probabilities) is different. -/
 180theorem higher_resolution_finer_distinctions (obs₁ obs₂ : Observer)
 181    (h : obs₁.resolution < obs₂.resolution) :
 182    -- obs₁ conflates some states (it's lossy)
 183    (∃ x y : ℝ, x ≠ y ∧ project obs₁ x = project obs₁ y) ∧
 184    -- obs₂ is also lossy, but has more distinct outcomes
 185    (∃ x y : ℝ, x ≠ y ∧ project obs₂ x = project obs₂ y) ∧
 186    -- obs₂ has strictly more resolution (more probability bins)
 187    obs₁.resolution < obs₂.resolution :=
 188  ⟨projection_lossy obs₁, projection_lossy obs₂, h⟩
 189
 190/-- **Theorem (Probability is Relational)**:
 191    The probability of an outcome is NOT a property of the underlying state alone.
 192    It depends on the relation between the state and the observer's resolution.
 193    Two observers with different resolutions partition the state space differently.
 194
 195    Formal content: The fiber count (= number of distinct probability bins)