higher_resolution_finer_distinctions
plain-language theorem explainer
Higher-resolution observers distinguish strictly more states than lower-resolution ones in a deterministic system, although both projections remain lossy. Researchers working on epistemic interpretations of probability in deterministic foundations cite this result to formalize how increased resolution refines probability bins without altering the underlying determinism. The proof is a direct term that invokes the general lossiness of any finite-resolution projection twice and retains the supplied resolution ordering.
Claim. Let $obs_1$ and $obs_2$ be observers with resolutions $r_1 < r_2$. Then there exist distinct reals $x,y$ such that the projection map of $obs_1$ sends $x$ and $y$ to the same bin, and likewise for $obs_2$, together with the inequality $r_1 < r_2$.
background
An Observer is a structure with a positive natural number resolution counting distinguishable states. The project function maps any real to one of the resolution bins via floor and modulo. The upstream theorem projection_lossy states that for any finite-resolution observer the map is many-to-one, which is the source of apparent randomness from coarse-graining of deterministic states.
proof idea
The proof is a one-line term that constructs the required conjunction by applying the projection_lossy lemma to obs₁, applying it again to obs₂, and pairing the results with the hypothesis h that supplies the strict inequality on resolutions.
why it matters
This declaration supports the Bayesian interpretation within the probability module by showing that refinement of resolution corresponds to finer distinctions in the fiber structure. It reinforces the framework claim that probability depends on the observer's resolution rather than solely on the state. The result closes part of the argument that learning corresponds to moving to higher-resolution observers in the deterministic ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.