pith. machine review for the scientific record. sign in
theorem proved term proof

frequentist_vindicated

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 149theorem frequentist_vindicated (obs : Observer) (x : ℝ) :
 150    -- The projection is deterministic: same input → same output
 151    ∀ y : ℝ, x = y → project obs x = project obs y := by

proof body

Term-mode proof.

 152  intro y hxy
 153  rw [hxy]
 154
 155/-- **Theorem (Bayesian Vindicated)**:
 156    The Bayesian insight is correct: probability is about information states.
 157
 158    Formalization: For any two observers with DIFFERENT resolutions, there
 159    exists a state x such that the two observers project x to DIFFERENT outcomes.
 160    This means their "probability assignments" differ — probability depends on
 161    the observer's information state (resolution), not just on reality.
 162
 163    This is the formal content of Bayesian subjectivism: same underlying state,
 164    different probabilities, because different observers have different resolutions. -/

depends on (17)

Lean names referenced from this declaration's body.