Fiber
The Fiber definition partitions the real line into preimages under an observer's finite-resolution projection map, collecting all underlying states that register as the same observed outcome. Researchers deriving the epistemic character of probability from deterministic J-cost dynamics cite this when showing that apparent randomness is produced solely by coarse-graining. The definition is introduced by a direct set comprehension that unfolds the project map.
claimFor an observer with positive integer resolution $N$ and outcome index $v$ in the finite set of size $N$, the fiber is the set of real numbers $x$ such that the projection map sends $x$ to $v$.
background
In the PH-006 module an observer is a structure equipped with a positive integer resolution that fixes the number of distinguishable outcomes. The associated projection map sends each real state $x$ to the bin index obtained by scaling, flooring, and reducing modulo the resolution; this map is total and surjective onto the finite set of outcomes. The module establishes that probability is epistemic: it equals the relative measure of states that collapse to the same observed bin under this coarse-graining.
proof idea
The definition is a one-line set comprehension that collects every real number whose image under the project map equals the supplied outcome index. No lemmas are applied; the construction simply substitutes the explicit formula for project inside the set-builder notation.
why it matters in Recognition Science
Fiber supplies the partition sets required by the PH-006 certificate and by the theorems fibers_cover, each_fiber_nonempty, and born_rule_structure. Those results together show that the fibers cover the entire state space, that every outcome is realized, and that the Born-rule weights arise from the J-cost landscape restricted to each fiber. The definition therefore closes the step from deterministic J-minimizer dynamics to observed statistics without postulating ontic randomness.
scope and limits
- Does not assign any measure or probability to the fibers.
- Does not invoke the explicit form of the J-cost function.
- Does not distinguish continuous from discrete underlying state spaces.
- Does not compute numerical values such as the fine-structure constant.
formal statement (Lean)
87def Fiber (obs : Observer) (v : Fin obs.resolution) : Set ℝ :=
proof body
Definition body.
88 { x | project obs x = v }
89
90/-- The fiber partition: every state belongs to exactly one fiber. -/