born_rule_structure
plain-language theorem explainer
The declaration shows that for any finite-resolution observer the projection map from underlying deterministic states partitions the reals into nonempty fibers, one per distinguishable outcome. A researcher examining the origin of the Born rule in quantum mechanics would cite this result to ground probability in epistemic projection rather than ontic randomness. The proof is a one-line term that assembles the covering property and the nonemptiness property of the fibers.
Claim. For an observer $obs$ with finite resolution $N$, the sets $Fiber(obs, v) = { x : project(obs, x) = v }$ for $v = 0, dots, N-1$ satisfy: every real $x$ belongs to exactly one such set, and each set is nonempty.
background
In Recognition Science, probability arises as the J-cost-weighted measure of fibers under a finite-resolution projection. An Observer is a structure with positive finite resolution, the number of distinguishable outcomes. The Fiber of outcome v is the preimage under the projection map, the set of underlying states that map to v. The module establishes that reality is deterministic with unique J-minimizers, so probability is epistemic: it reflects the observer's coarse-graining. Upstream, the Observer structure from Determinism supplies the resolution parameter, while the J-cost landscape supplies the weights that later yield the Born rule.
proof idea
The proof is a term-mode one-liner that directly pairs the fibers_cover lemma, which establishes the partition property, with the each_fiber_nonempty lemma, which shows every outcome has at least one preimage state.
why it matters
This result sits inside the PH-006 resolution of probability interpretations by showing that the Born rule structure follows from the fiber partition alone. It feeds the subsequent development of probability axioms satisfied by the J-cost projection. The construction aligns with the framework's T5 J-uniqueness and the emergence of probability from the phi-ladder without separate postulates. No open questions are flagged here, but the specific weights remain to be derived from the J-cost landscape in downstream steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.