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
proof body
Term-mode proof.
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. -/
depends on (22)
Lean names referenced from this declaration's body.