IndisputableMonolith.Foundation.CostFirstExistence

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Cost-First Existence: Pre-Big-Bang Selection Principle
   7
   8The pre-Big-Bang paper argues that existence is not posited but selected:
   9stable configurations are those with minimum recognition cost. This module
  10formalises the core structural claim:
  11
  12**Cost-first selection principle:** A pattern `x > 0` "exists" in the
  13recognition sense iff `J(x) = 0`, i.e., iff `x = 1` (the cost minimum).
  14All other positive values carry strictly positive J-cost and are
  15transiently unstable under R̂ evolution.
  16
  17This gives a clean RS definition of existence:
  18  RSExists(x) ↔ J(x) = 0 ↔ x = 1  (for x : ℝ, x > 0)
  19
  20The origin of law from cost-minimisation:
  21- Laws are the unique J-minimising configurations of the recognition lattice.
  22- Physics emerges from the constraint "the universe minimises J".
  23- The pre-Big-Bang "era" is the pre-geometric cost landscape.
  24
  25Lean status: 0 sorry, 0 axiom.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Foundation
  30namespace CostFirstExistence
  31
  32open Cost
  33
  34noncomputable section
  35
  36/-- Recognition existence: `x` exists iff J(x) = 0. -/
  37def RSExists (x : ℝ) : Prop := Jcost x = 0
  38
  39/-- RSExists iff x = 1 (the unique J-cost minimiser). -/
  40theorem rsExists_iff_one {x : ℝ} (hx : 0 < x) :
  41    RSExists x ↔ x = 1 := by
  42  unfold RSExists
  43  constructor
  44  · intro h
  45    by_contra hne
  46    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
  47  · rintro rfl
  48    exact Jcost_unit0
  49
  50/-- Non-existence costs more than zero. -/
  51theorem non_existence_has_positive_cost {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
  52    0 < Jcost x :=
  53  Jcost_pos_of_ne_one x hx hne
  54
  55/-- The unique "nothing" reference: cost is unbounded on (0,∞). -/
  56theorem divergence_at_zero_direction :
  57    ¬ ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → Jcost ε ≤ C := by
  58  intro ⟨C, hC⟩
  59  -- Pick ε = 1/(2*(|C|+2)); then J(ε) > |C|+1 > C
  60  -- Actual proof: pick ε = 1/4, then J(1/4) = (1/4-1)²/(2·1/4) = (9/16)/(1/2) = 9/8
  61  -- That only bounds J away from C when C < 9/8.
  62  -- For large C, pick ε = 1/(C+2):
  63  -- J(1/(C+2)) = (1/(C+2)-1)²/(2/(C+2)) = (C+1)²/(C+2)²·(C+2)/2 = (C+1)²/(2(C+2))
  64  -- For C ≥ 0: (C+1)²/(2(C+2)) > C ↔ (C+1)² > 2C(C+2) = 2C²+4C ↔ C²+2C+1 > 2C²+4C ↔ 0 > C²+2C-1
  65  -- This fails for C ≥ 1. Need a better choice. Use ε = 1/(2C+4):
  66  -- J(1/(2C+4)) = (1/(2C+4)-1)²/(2/(2C+4)) = ((2C+3)/(2C+4))²·(2C+4)/2 = (2C+3)²/(2(2C+4))
  67  -- Compare with C: (2C+3)²/(2(2C+4)) > C ↔ (2C+3)² > 2C(2C+4) = 4C²+8C
  68  -- = 4C²+12C+9 > 4C²+8C ↔ 4C+9 > 0, which holds for C > -9/4.
  69  -- For C ≤ -3, J(ε) ≥ 0 > C since C < 0. Done by cases.
  70  -- Use J(1) = 0 to handle C < 0, and a direct computation for C ≥ 0
  71  by_cases hC_neg : C < 0
  72  · linarith [hC 1 one_pos, Jcost_unit0]
  73  push_neg at hC_neg  -- C ≥ 0
  74  -- J(1/(2C+4)) = (2C+3)²/(2(2C+4)) > C for C ≥ 0
  75  have h2C4 : (0 : ℝ) < 2 * C + 4 := by linarith
  76  have hε := hC (1 / (2 * C + 4)) (div_pos one_pos h2C4)
  77  have hJval : Jcost (1 / (2 * C + 4)) = (2 * C + 3) ^ 2 / (2 * (2 * C + 4)) := by
  78    rw [Jcost_eq_sq (by positivity)]
  79    field_simp
  80    ring
  81  rw [hJval] at hε
  82  have hnum : 0 ≤ (2 * C + 3) ^ 2 := sq_nonneg _
  83  -- (2C+3)²/(2(2C+4)) ≤ C ↔ (2C+3)² ≤ 2C(2C+4) = 4C²+8C
  84  -- But (2C+3)² = 4C²+12C+9 > 4C²+8C = 2C(2C+4) for C ≥ 0 (since 4C+9 > 0)
  85  have hrewrite : (2 * C + 3) ^ 2 / (2 * (2 * C + 4)) ≤ C ↔
  86      (2 * C + 3) ^ 2 ≤ C * (2 * (2 * C + 4)) := by
  87    rw [div_le_iff₀ (by positivity : (0 : ℝ) < 2 * (2 * C + 4))]
  88  rw [hrewrite] at hε
  89  nlinarith [sq_nonneg (2 * C + 3)]
  90
  91structure CostFirstExistenceCert where
  92  rsExists_iff : ∀ {x : ℝ}, 0 < x → (RSExists x ↔ x = 1)
  93  non_existence_costly :
  94    ∀ {x : ℝ}, 0 < x → x ≠ 1 → 0 < Jcost x
  95  nothing_diverges :
  96    ¬ ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → Jcost ε ≤ C
  97
  98/-- Cost-first existence certificate. -/
  99def costFirstExistenceCert : CostFirstExistenceCert where
 100  rsExists_iff := @rsExists_iff_one
 101  non_existence_costly := @non_existence_has_positive_cost
 102  nothing_diverges := divergence_at_zero_direction
 103
 104end
 105end CostFirstExistence
 106end Foundation
 107end IndisputableMonolith
 108