Foundation Determinism

Foundation Determinism

Foundation determinism is the Recognition Science answer to a long-standing question: is the universe deterministic or fundamentally random? The answer is both, but about different things. The ledger, the record of recognition events, is deterministic. Observation of that ledger is lossy, and the loss is where apparent randomness comes from. The framework forces the deterministic half and formalizes the lossy half; it does not claim to force that the observer's projection is the only source of randomness in every conceivable setting.

The deterministic half rests on a forced fact about the cost function. The cost function, the forced measure of mismatch in a recognition event, is strictly convex on positive numbers: its second derivative is positive everywhere above zero. A strictly convex function minimized over a convex set of feasible points has exactly one minimizer. The theorem unique_minimizer_principle states this for any constrained problem on positive reals. So for any ledger update, the next state is uniquely determined by the current state and the constraint. There is no choice in the dynamics.

The apparent-randomness half is a formal statement about observers. An observer is defined by a finite resolution, a positive natural number of distinguishable states. The projection map sends each real-valued state to one of those finitely many bins. The theorem projection_lossy forces that distinct states can land in the same bin. A finite-resolution observer looking at a deterministic process therefore sees a coarse-grained sequence that can look random. The Born rule, the squared-amplitude probability law of quantum mechanics, is identified in the framework's docstring as the projection of deterministic cost minimization onto an observer's resolution. That identification is stated in the module's commentary, not forced as a theorem in the formal file.

The resolution theorem, determinism_resolution, packages the whole picture. It forces two things together: every positive number other than 1 has a positive defect, and 1 is the unique positive number with defect zero. The defect is the mismatch the cost function measures, so this says the ledger has exactly one self-consistent resting point and every other state carries a positive cost that drives it toward that point. Determinism and the uniqueness of the fixed point are the same fact seen from two angles.

What this changes is the shape of the randomness debate. The framework does not choose sides between determinism and randomness; it assigns each word to a different object. Reality is deterministic because the cost minimizer is unique. Observation appears random because the projection is lossy. Both sides of the old debate are correct, but about different things. The open question is whether the physical bridge from recognition to observable quantum randomness can be made fully rigorous, since the module states the Born-rule identification as commentary rather than as a forced theorem.

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

The Born rule is not forced in this module; it is identified in commentary only. The physical bridge from recognition to observable quantum randomness is not established here. The module does not claim that every apparent randomness in nature is fully explained by finite resolution.

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: