Foundation Determinism Unique Minimizer Principle

The unique minimizer principle

Determinism is the claim that the future is fixed by the present. The Recognition Science framework's unique_minimizer_principle formalizes this for its own model of change. The framework models the universe as a ledger, a discrete record of events, where each update is the solution to a constrained optimization problem. The principle states that for any such problem with a convex set of feasible positive states, the minimizing state is unique. This means the next ledger state is uniquely determined by the current state plus the constraint; there is no choice in the matter.

The core of the proof is a property of the framework's cost function, J(x) = (x + 1/x)/2 - 1. This function is strictly convex on the positive reals, meaning its second derivative is always positive. A strictly convex function has exactly one minimum on any convex set. The machine-checked library of formal theorems proves this directly: the second derivative of J is x^-3, which is positive for all x > 0. From this, the unique_minimizer_principle follows as a theorem: if two points both minimize J over a convex feasible set, they must be equal.

This theorem is the first step in the framework's resolution of the determinism question. It establishes that the dynamics are deterministic at the level of the full ledger state. The framework then introduces the concept of a finite-resolution observer. Such an observer cannot access the full ledger state; they see a coarse-grained projection of it. The framework proves that this projection is lossy: multiple distinct ledger states map to the same observation. This is the origin of apparent randomness. A deterministic process, viewed through a lossy channel, appears random to the observer.

In Recognition Science, the principle does not claim that the universe is random. It claims the opposite: reality is deterministic, and what appears as randomness is a feature of the observer's limited resolution. The framework's library proves that the J-cost function has a unique positive minimum at x = 1, and that its defect, a measure of deviation from that minimum, is positive for all other positive x. This pins down the unique stable state of the ledger. The principle is a statement about the framework's model of reality, not a direct claim about the physical universe as described by any particular experiment.

The significance of the unique_minimizer_principle is that it provides a formal, machine-checked foundation for the determinism side of the debate. It does not, by itself, explain how the Born rule of quantum mechanics emerges from this deterministic substrate; that is a separate, more speculative step in the framework. The principle is a precise mathematical statement about a specific cost function, and its power lies in being the first link in a chain that the framework uses to derive further structure.

/-- **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

/-- J''(x) = x⁻³ > 0 for x > 0. This is the key strict convexity fact. -/
theorem Jcost_second_deriv_positive {x : ℝ} (hx : 0 < x) :
    0 < x⁻¹ ^ 3 := by positivity

/-- **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]

/-- **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⟩

What this page does not claim

This answer does not claim the unique_minimizer_principle is a proof that the physical universe is deterministic. This answer does not claim the framework's derivation of the Born rule is a proved theorem. This answer does not claim the framework's model of a ledger is the only possible model of physical reality.

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: