each_fiber_nonempty
plain-language theorem explainer
Every outcome index v for a finite-resolution observer has a nonempty preimage under the projection map from underlying real states. Researchers deriving quantum probability from deterministic foundations cite this to ground apparent randomness in coarse-graining. The proof exhibits an explicit witness scaled by the resolution index and verifies membership via floor-modulo arithmetic.
Claim. For any observer obs with positive finite resolution N and any v in Fin N, the set { x ∈ ℝ | project(obs, x) = v } is nonempty.
background
The module PH-006 resolves probability interpretations by showing it equals J-cost projection weight from finite-resolution observers on deterministic dynamics. An Observer is the structure with resolution : ℕ and res_pos : 0 < resolution. The project map sends x to floor(x * N) mod N. Fiber(obs, v) is the set of x such that project(obs, x) = v. This rests on the Observer and project definitions from the Determinism module, which establish that distinct states can map to one observation.
proof idea
The proof picks the witness (v.val : ℝ) / (obs.resolution : ℝ). It unfolds Fiber and project, applies field_simp to cancel the division, then uses Int.floor_natCast, Int.toNat_natCast and Nat.mod_eq_of_lt to recover v exactly.
why it matters
This supplies the nonempty-fiber half of born_rule_structure, which combines with fibers_cover to feed ph006_probability_certificate. The certificate asserts probability equals J-cost projection weight with no ontic randomness. It closes the step showing how finite-resolution projections on deterministic J-minimizers produce epistemic probabilities and the Born rule structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.