each_fiber_nonempty
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive explicit probability weights or J-cost measures on fibers.
- Does not treat the infinite-resolution limit.
- Does not embed the J functional or defectDist inside the fiber definition.
- Does not prove fibers have equal cardinality or measure.
Lean usage
theorem use_fiber_nonempty (obs : Observer) (v : Fin obs.resolution) : (Fiber obs v).Nonempty := each_fiber_nonempty obs vformal statement (Lean)
108theorem each_fiber_nonempty (obs : Observer) (v : Fin obs.resolution) :
109 (Fiber obs v).Nonempty := by
proof body
Tactic-mode proof.
110 -- Use x = v.val / obs.resolution as witness
111 use (v.val : ℝ) / (obs.resolution : ℝ)
112 unfold Fiber project
113 simp only [Set.mem_setOf_eq, Fin.ext_iff, Fin.val_mk]
114 have hN : (obs.resolution : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp obs.res_pos)
115 have hmul : (v.val : ℝ) / obs.resolution * obs.resolution = v.val := by
116 field_simp
117 simp only [hmul]
118 simp only [Int.floor_natCast, Int.toNat_natCast]
119 exact Nat.mod_eq_of_lt v.isLt
120
121/-! ## Probability is Epistemic -/
122
123/-- **Theorem (Probability is Epistemic)**:
124 The "randomness" seen by a finite-resolution observer arises from
125 finite information capacity, not from ontological indeterminism.
126
127 Proof: The deterministic structure (unique J-minimizer) is real;
128 the probabilistic appearance is a consequence of the projection. -/