obs_probability
plain-language theorem explainer
The definition assigns uniform probability 1/N to each of the N distinguishable outcomes seen by a finite-resolution observer. Foundations researchers working on epistemic interpretations of probability cite this when showing how deterministic dynamics plus coarse-graining yield classical probabilities. It is implemented as a direct one-line reciprocal of the resolution field.
Claim. Let $N$ be the resolution of observer obs. For each outcome index $v$ in the finite set of size $N$, the assigned probability is $1/N$.
background
In the Recognition Science treatment of probability (PH-006), an Observer is a structure equipped with a positive integer resolution $N$ that counts the number of distinguishable states. The module establishes that probability arises as the projection weight under finite resolution, with no ontic probability in the underlying deterministic J-minimizing dynamics. Upstream results supply the Observer definition from Determinism and ObserverForcing, along with lists of narrative, kinship, and modal structures that illustrate the finite discrete sets appearing throughout the framework.
proof idea
The definition is a direct one-line assignment: the probability for any outcome is the reciprocal of the observer resolution.
why it matters
This definition supplies the uniform measure used by the sibling theorems probability_nonneg and probability_sums_to_one to establish the basic properties of a probability distribution. It realizes the epistemic reading in the RS resolution of probability interpretations, where finite resolution induces the counting measure over fibers. The construction sits inside the broader forcing chain that derives spatial dimensions and constants from the J-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.