fibers_cover
plain-language theorem explainer
Every real number belongs to exactly one fiber of the projection map defined by a finite-resolution observer. Researchers deriving epistemic interpretations of probability from deterministic dynamics cite this partition to ground apparent randomness in coarse-graining. The proof is a direct term construction that supplies the projected index as witness and uses equality symmetry for uniqueness.
Claim. For any observer with finite positive resolution $N$ and any real number $x$, there exists a unique $v$ in the finite set of $N$ outcomes such that $x$ lies in the preimage set under the projection map, where the preimage of $v$ consists of all reals that the observer maps to $v$.
background
The PH-006 module resolves probability interpretations by showing that probability equals J-cost projection weight in a deterministic setting. An Observer is a structure with a positive integer resolution $N$ and a proof that $N > 0$. The project function maps each real $x$ to an element of Fin $N$ by taking the integer part of $x$ scaled by $N$ and reducing modulo $N$. The Fiber of outcome $v$ is the set of all reals that project to $v$ under this map.
proof idea
The proof is a term-mode construction. It supplies the value of the project function applied to the given observer and state as the unique witness. Reflexivity establishes membership in the fiber. Uniqueness is obtained by symmetry of the equality hypothesis on the projected index.
why it matters
This supplies the covering half of the fiber partition required by born_rule_structure, which combines it with each_fiber_nonempty to produce the full statement that fibers partition the state space and are nonempty. That result in turn feeds ph006_probability_certificate, which certifies that probability is epistemic J-cost weight rather than ontic. The partition therefore grounds the emergence of the Born rule from projection structure without additional postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.