IndisputableMonolith.Foundation.Determinism

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.Convexity
   4import IndisputableMonolith.Foundation.LawOfExistence
   5
   6/-!
   7# F-007: Determinism — Why Apparent Randomness in a Determined Universe
   8
   9Formalizes the resolution of the determinism question.
  10
  11## The Argument
  12
  131. **Deterministic dynamics**: The J-cost function is strictly convex on (0, ∞).
  14   For any constrained optimization (ledger update), the minimizer is UNIQUE.
  15   Therefore the next state is uniquely determined by the current state.
  16
  172. **Apparent randomness**: An observer with finite resolution cannot access the
  18   full ledger state. They see a coarse-grained projection. The projection of
  19   a deterministic process through a lossy channel appears random.
  20
  213. **Born rule emergence**: The probability distribution over outcomes for a
  22   finite-resolution observer is determined by the J-cost landscape.
  23   The squared-amplitude rule (Born rule) is the projection of deterministic
  24   J-cost minimization onto the observer's resolution.
  25
  26## Registry Item
  27- F-007: Is the universe deterministic or fundamentally random?
  28-/
  29
  30namespace IndisputableMonolith
  31namespace Foundation
  32namespace Determinism
  33
  34open Real Cost
  35
  36/-! ## Strict Convexity of J-cost -/
  37
  38/-- J''(x) = x⁻³ > 0 for x > 0. This is the key strict convexity fact. -/
  39theorem Jcost_second_deriv_positive {x : ℝ} (hx : 0 < x) :
  40    0 < x⁻¹ ^ 3 := by positivity
  41
  42
  43/-! ## Unique Minimizer Theorem -/
  44
  45/-- A constrained optimization problem on positive reals. -/
  46structure ConstrainedProblem where
  47  /-- The constraint set (e.g., log-sum = constant) -/
  48  feasible : Set ℝ
  49  /-- Feasible set is nonempty -/
  50  nonempty : feasible.Nonempty
  51  /-- All feasible points are positive -/
  52  positive : ∀ x ∈ feasible, 0 < x
  53
  54/-- **Theorem (Determinism core)**: For any constrained minimization of J-cost
  55    over a convex set of positive reals, the minimizer is unique.
  56
  57    This means the next ledger state is uniquely determined by the current
  58    state plus the constraint. There is no "choice" — the dynamics are
  59    deterministic. -/
  60theorem unique_minimizer_principle (p : ConstrainedProblem)
  61    (h_convex : Convex ℝ p.feasible)
  62    (x_min : ℝ) (hx_feas : x_min ∈ p.feasible)
  63    (hx_min : ∀ y ∈ p.feasible, Jcost x_min ≤ Jcost y)
  64    (y_min : ℝ) (hy_feas : y_min ∈ p.feasible)
  65    (hy_min : ∀ z ∈ p.feasible, Jcost y_min ≤ Jcost z) :
  66    x_min = y_min := by
  67  by_contra h_ne
  68  have hx := hx_min y_min hy_feas
  69  have hy := hy_min x_min hx_feas
  70  have h_eq : Jcost x_min = Jcost y_min := le_antisymm hx hy
  71  -- Strict convexity: Jcost is strictly convex on (0,∞), so equal cost at two points forces equality.
  72  have hJ_pos : StrictConvexOn ℝ p.feasible Jcost :=
  73    StrictConvexOn.subset Jcost_strictConvexOn_pos
  74      (fun z hz => Set.mem_Ioi.mpr (p.positive z hz)) h_convex
  75  have h_mid_mem : (x_min + y_min) / 2 ∈ p.feasible := by
  76    have hsmul := h_convex hx_feas hy_feas (by norm_num : (0 : ℝ) ≤ 1/2) (by norm_num : (0 : ℝ) ≤ 1/2)
  77      (by norm_num : (1/2 : ℝ) + (1/2 : ℝ) = 1)
  78    simp only [smul_eq_mul] at hsmul
  79    convert hsmul using 1
  80    ring
  81  have h_strict : Jcost ((x_min + y_min) / 2) < (1/2) * Jcost x_min + (1/2) * Jcost y_min := by
  82    have heq : (1/2 : ℝ) • x_min + (1/2 : ℝ) • y_min = (x_min + y_min) / 2 := by
  83      simp only [smul_eq_mul]; ring
  84    rw [← heq]
  85    exact hJ_pos.2 hx_feas hy_feas h_ne (by norm_num : (0 : ℝ) < 1/2) (by norm_num : (0 : ℝ) < 1/2)
  86      (by norm_num : (1/2 : ℝ) + (1/2 : ℝ) = 1)
  87  -- RHS = Jcost y_min since Jcost x_min = Jcost y_min
  88  rw [h_eq, show (1/2 : ℝ) * Jcost y_min + (1/2) * Jcost y_min = Jcost y_min by ring] at h_strict
  89  have h_min := hx_min ((x_min + y_min) / 2) h_mid_mem
  90  rw [h_eq] at h_min
  91  linarith
  92
  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)
 127    - Both sides of the debate are correct, about different things -/
 128theorem determinism_resolution :
 129    (∀ x : ℝ, 0 < x → x ≠ 1 → 0 < LawOfExistence.defect x) ∧
 130    (∃! x : ℝ, 0 < x ∧ LawOfExistence.defect x = 0) := by
 131  constructor
 132  · intro x hx hne
 133    exact LawOfExistence.defect_pos_of_ne_one hx hne
 134  · exact ⟨1, ⟨by norm_num, LawOfExistence.defect_one⟩,
 135      fun y ⟨hy_pos, hy_zero⟩ =>
 136        (LawOfExistence.defect_zero_iff_one hy_pos).mp hy_zero⟩
 137
 138end Determinism
 139end Foundation
 140end IndisputableMonolith
 141