`Observer`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.Determinism
domain: Foundation
line: 96 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.Determinism on GitHub at line 96.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  93/-! ## Finite-Resolution Observers -/
  94
  95/-- An observer with finite resolution sees a coarse-grained state. -/
  96structure Observer where
  97  /-- Number of distinguishable states -/
  98  resolution : ℕ
  99  /-- Resolution is finite and positive -/
 100  res_pos : 0 < resolution
 101
 102/-- The projection map: a deterministic state maps to an observed state. -/
 103noncomputable def project (obs : Observer) (x : ℝ) : Fin obs.resolution :=
 104  ⟨(Int.toNat (Int.floor (x * obs.resolution))) % obs.resolution,
 105   Nat.mod_lt _ obs.res_pos⟩
 106
 107/-- **Theorem**: Multiple distinct states map to the same observation.
 108    This is the origin of "apparent randomness." -/
 109theorem projection_lossy (obs : Observer) :
 110    ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y := by
 111  use 0, 1
 112  constructor
 113  · norm_num
 114  · simp [project]
 115
 116/-! ## Determinism Resolution -/
 117
 118/-- **The Determinism Theorem (F-007 Resolution)**:
 119
 120    1. The universe is deterministic: unique J-cost minimizer at each step.
 121    2. Apparent randomness arises from finite-resolution observation.
 122    3. "Quantum randomness" is a feature of the OBSERVER, not reality.
 123
 124    This dissolves the determinism-vs-randomness debate:
 125    - Reality IS deterministic (unique cost minimizer)
 126    - Observations APPEAR random (projection through finite resolution)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.