Encyclopedia Foundation Foundation Determinism Determinism Resolution

ARTICLE 4 claims 4 theorems

Foundation Determinism Determinism Resolution

A machine-checked theorem says the universe's next state is uniquely forced, and apparent randomness is a property of observers with limited resolution.

Verify this page

The resolution

Determinism is the view that every event has a unique cause and a unique outcome. Its opposite, indeterminism, holds that some outcomes are genuinely undecided. The debate is old, but it usually runs on intuition. The Recognition Science framework tries to settle it with a precise cost function: a ledger, a discrete record of events, updates by minimizing a fixed cost, and the cost function J(x) = (x + 1/x)/2 - 1 is strictly convex, meaning its graph curves upward everywhere. A strictly convex function has at most one lowest point. The framework's library, a machine-checked collection of formal theorems, proves that for any constrained minimization of J-cost over a convex set of positive reals, the minimizer is unique. In plain terms: given the current ledger state and the constraint, the next state is forced. There is no choice, no coin flip, no hidden dice. The theorem, named determinism_resolution, also proves that the only positive number with zero defect is 1, and every other positive number has positive defect. Defect here is the cost of being away from the ideal state, so the unique zero-defect state is exactly 1.

The framework then explains why the world still looks random. An observer with finite resolution cannot see the full ledger state; the observer sees only a coarse-grained projection, a bucket label instead of the exact real number. The library proves that this projection is lossy: there exist two distinct states that map to the same observation. So the same observed outcome can come from different underlying realities. A deterministic process, viewed through such a lossy channel, produces a sequence that appears random to the observer. The framework's conclusion, stated in its determinism theorem, is that the universe is deterministic at the level of the ledger, while apparent randomness, including what physics calls quantum randomness, is a feature of the observer's finite resolution, not of reality itself. Both sides of the old debate are right about different things: reality is deterministic, and observations appear random.

In Recognition Science, this dissolves the determinism-versus-randomness question rather than picking one side. The resolution is a formal theorem, not a philosophical preference. The framework models the observer's resolution as a finite positive integer, the number of distinguishable states, and the projection map as a floor-and-modulo operation. The theorem projection_lossy proves that distinct real states can collide to the same observation. The uniqueness theorem, unique_minimizer_principle, requires the feasible set to be convex and nonempty, and the cost function to be J-cost. Under those conditions, two minimizers must be equal. The framework does not claim to have proved the Born rule, the squared-amplitude probability rule of quantum mechanics, as a theorem; its docstring says the Born rule emerges as the projection of deterministic J-cost minimization, but the library contains no formal proof of that emergence. The framework also does not claim that every physical system obeys this exact cost function; the cost function is the framework's definitional choice, not a derived law for all of physics. And the theorem does not say that observers cannot improve their resolution; it only says that any finite resolution is lossy.

THEOREM unique_minimizer_principle · IndisputableMonolith/Foundation/Determinism.lean
unique_minimizer_principle · IndisputableMonolith/Foundation/Determinism.lean:54 
/-- **Theorem (Determinism core)**: For any constrained minimization of J-cost
    over a convex set of positive reals, the minimizer is unique.

    This means the next ledger state is uniquely determined by the current
    state plus the constraint. There is no "choice" — the dynamics are
    deterministic. -/
theorem unique_minimizer_principle (p : ConstrainedProblem)
    (h_convex : Convex ℝ p.feasible)
    (x_min : ℝ) (hx_feas : x_min ∈ p.feasible)
    (hx_min : ∀ y ∈ p.feasible, Jcost x_min ≤ Jcost y)
    (y_min : ℝ) (hy_feas : y_min ∈ p.feasible)
    (hy_min : ∀ z ∈ p.feasible, Jcost y_min ≤ Jcost z) :
    x_min = y_min := by
  by_contra h_ne
  have hx := hx_min y_min hy_feas
  have hy := hy_min x_min hx_feas
  have h_eq : Jcost x_min = Jcost y_min := le_antisymm hx hy
  -- Strict convexity: Jcost is strictly convex on (0,∞), so equal cost at two points forces equality.
  have hJ_pos : StrictConvexOn ℝ p.feasible Jcost :=
    StrictConvexOn.subset Jcost_strictConvexOn_pos
      (fun z hz => Set.mem_Ioi.mpr (p.positive z hz)) h_convex
  have h_mid_mem : (x_min + y_min) / 2 ∈ p.feasible := by
    have hsmul := h_convex hx_feas hy_feas (by norm_num : (0 : ℝ) ≤ 1/2) (by norm_num : (0 : ℝ) ≤ 1/2)
      (by norm_num : (1/2 : ℝ) + (1/2 : ℝ) = 1)
    simp only [smul_eq_mul] at hsmul
    convert hsmul using 1
    ring
  have h_strict : Jcost ((x_min + y_min) / 2) < (1/2) * Jcost x_min + (1/2) * Jcost y_min := by
    have heq : (1/2 : ℝ) • x_min + (1/2 : ℝ) • y_min = (x_min + y_min) / 2 := by
      simp only [smul_eq_mul]; ring
    rw [← heq]
    exact hJ_pos.2 hx_feas hy_feas h_ne (by norm_num : (0 : ℝ) < 1/2) (by norm_num : (0 : ℝ) < 1/2)
      (by norm_num : (1/2 : ℝ) + (1/2 : ℝ) = 1)
  -- RHS = Jcost y_min since Jcost x_min = Jcost y_min
  rw [h_eq, show (1/2 : ℝ) * Jcost y_min + (1/2) * Jcost y_min = Jcost y_min by ring] at h_strict
  have h_min := hx_min ((x_min + y_min) / 2) h_mid_mem
  rw [h_eq] at h_min
  linarith
THEOREM unique_minimizer_principle · IndisputableMonolith/Foundation/Determinism.lean
unique_minimizer_principle · IndisputableMonolith/Foundation/Determinism.lean:54 
/-- **Theorem (Determinism core)**: For any constrained minimization of J-cost
    over a convex set of positive reals, the minimizer is unique.

    This means the next ledger state is uniquely determined by the current
    state plus the constraint. There is no "choice" — the dynamics are
    deterministic. -/
theorem unique_minimizer_principle (p : ConstrainedProblem)
    (h_convex : Convex ℝ p.feasible)
    (x_min : ℝ) (hx_feas : x_min ∈ p.feasible)
    (hx_min : ∀ y ∈ p.feasible, Jcost x_min ≤ Jcost y)
    (y_min : ℝ) (hy_feas : y_min ∈ p.feasible)
    (hy_min : ∀ z ∈ p.feasible, Jcost y_min ≤ Jcost z) :
    x_min = y_min := by
  by_contra h_ne
  have hx := hx_min y_min hy_feas
  have hy := hy_min x_min hx_feas
  have h_eq : Jcost x_min = Jcost y_min := le_antisymm hx hy
  -- Strict convexity: Jcost is strictly convex on (0,∞), so equal cost at two points forces equality.
  have hJ_pos : StrictConvexOn ℝ p.feasible Jcost :=
    StrictConvexOn.subset Jcost_strictConvexOn_pos
      (fun z hz => Set.mem_Ioi.mpr (p.positive z hz)) h_convex
  have h_mid_mem : (x_min + y_min) / 2 ∈ p.feasible := by
    have hsmul := h_convex hx_feas hy_feas (by norm_num : (0 : ℝ) ≤ 1/2) (by norm_num : (0 : ℝ) ≤ 1/2)
      (by norm_num : (1/2 : ℝ) + (1/2 : ℝ) = 1)
    simp only [smul_eq_mul] at hsmul
    convert hsmul using 1
    ring
  have h_strict : Jcost ((x_min + y_min) / 2) < (1/2) * Jcost x_min + (1/2) * Jcost y_min := by
    have heq : (1/2 : ℝ) • x_min + (1/2 : ℝ) • y_min = (x_min + y_min) / 2 := by
      simp only [smul_eq_mul]; ring
    rw [← heq]
    exact hJ_pos.2 hx_feas hy_feas h_ne (by norm_num : (0 : ℝ) < 1/2) (by norm_num : (0 : ℝ) < 1/2)
      (by norm_num : (1/2 : ℝ) + (1/2 : ℝ) = 1)
  -- RHS = Jcost y_min since Jcost x_min = Jcost y_min
  rw [h_eq, show (1/2 : ℝ) * Jcost y_min + (1/2) * Jcost y_min = Jcost y_min by ring] at h_strict
  have h_min := hx_min ((x_min + y_min) / 2) h_mid_mem
  rw [h_eq] at h_min
  linarith
THEOREM determinism_resolution · IndisputableMonolith/Foundation/Determinism.lean
determinism_resolution · IndisputableMonolith/Foundation/Determinism.lean:118 
/-- **The Determinism Theorem (F-007 Resolution)**:

    1. The universe is deterministic: unique J-cost minimizer at each step.
    2. Apparent randomness arises from finite-resolution observation.
    3. "Quantum randomness" is a feature of the OBSERVER, not reality.

    This dissolves the determinism-vs-randomness debate:
    - Reality IS deterministic (unique cost minimizer)
    - Observations APPEAR random (projection through finite resolution)
    - Both sides of the debate are correct, about different things -/
theorem determinism_resolution :
    (∀ x : ℝ, 0 < x → x ≠ 1 → 0 < LawOfExistence.defect x) ∧
    (∃! x : ℝ, 0 < x ∧ LawOfExistence.defect x = 0) := by
  constructor
  · intro x hx hne
    exact LawOfExistence.defect_pos_of_ne_one hx hne
  · exact ⟨1, ⟨by norm_num, LawOfExistence.defect_one⟩,
      fun y ⟨hy_pos, hy_zero⟩ =>
        (LawOfExistence.defect_zero_iff_one hy_pos).mp hy_zero⟩
THEOREM projection_lossy · IndisputableMonolith/Foundation/Determinism.lean
projection_lossy · IndisputableMonolith/Foundation/Determinism.lean:107 
/-- **Theorem**: Multiple distinct states map to the same observation.
    This is the origin of "apparent randomness." -/
theorem projection_lossy (obs : Observer) :
    ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y := by
  use 0, 1
  constructor
  · norm_num
  · simp [project]

What this page does not claim

The Born rule is not proved as a theorem in the library; it is only described in a docstring as emerging from the projection. The framework does not claim that all physical systems obey the J-cost function; it is a definitional choice, not a derived law for all of physics. The theorem does not claim that observers cannot improve their resolution, only that any finite resolution is lossy.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/Determinism.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND