bayesian_vindicated
plain-language theorem explainer
Any finite-resolution observer maps distinct real states to the same observed value under its projection, so probability assignments depend on the observer's information state rather than the underlying deterministic ledger alone. Foundations researchers in quantum mechanics or statistical mechanics cite this to anchor Bayesian credence in Recognition Science's deterministic J-cost dynamics. The proof is a one-line wrapper applying the projection_lossy result directly to an arbitrary observer.
Claim. For every observer with finite positive resolution, there exist distinct real numbers $x$ and $y$ such that the observer's coarse-graining map sends $x$ and $y$ to the same observed state: $x$ and $y$ lie in the same fiber of the projection.
background
The module establishes that probability equals J-cost projection weight on a deterministic ledger. Reality admits a unique J-minimizer at each step, yet any observer with finite resolution (a structure containing a positive natural number for distinguishable states) applies a coarse-graining map that sends each real number to an element of a finite set of size equal to the resolution. The projection is defined by scaling the input by the resolution, taking the floor, and reducing modulo the resolution, producing a lossy map whose fibers contain multiple preimages. The upstream projection_lossy theorem states that for any such observer there exist distinct reals mapped to the same output, which is the formal source of apparent randomness.
proof idea
The proof is a one-line wrapper that applies the projection_lossy theorem directly to the supplied observer. After introducing the observer, the exact tactic instantiates the existential witness already constructed in projection_lossy.
why it matters
This result supplies the formal content of the Bayesian interpretation inside the Recognition Science unification of probability meanings. It shows that credence is projection uncertainty given finite resolution, while the underlying dynamics remain deterministic with a unique J-minimizer. The declaration sits in the Philosophy.ProbabilityMeaningStructure module that resolves Frequentist, Bayesian, Propensity, and Logical views; it directly supports the claim that probability is epistemic rather than ontic and feeds the downstream unification that Born-rule distributions arise from J-cost landscape structure rather than separate postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.