IndisputableMonolith.Foundation.ExistenceUniquenessFromCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Existence Uniqueness from Cost — Pre-Big-Bang Complement
   7
   8`Foundation/CostFirstExistence` showed that RSExists(x) ↔ J(x) = 0 ↔ x = 1.
   9This companion module proves the UNIQUENESS half more explicitly:
  10there is exactly one point in ℝ+ with J-cost zero, and this uniqueness
  11is derivable from the J-cost functional form alone.
  12
  13This addresses the pre-BB paper's claim that "existence is not plural"
  14— there cannot be two distinct cost minima on ℝ+.
  15
  16Key theorems:
  171. **Uniqueness**: the set {x > 0 : J(x) = 0} is a singleton {1}.
  182. **Isolation**: for any δ > 0, min{J(x) : x ∈ (0,1-δ] ∪ [1+δ,∞)} > 0.
  193. **J as a distance**: J(x) is a semi-metric on the log-ratio scale.
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Foundation
  26namespace ExistenceUniquenessFromCost
  27
  28open Cost
  29
  30noncomputable section
  31
  32/-- The cost-zero set is exactly {1}. -/
  33theorem cost_zero_set_singleton :
  34    ∀ x : ℝ, 0 < x → (Jcost x = 0 ↔ x = 1) := by
  35  intro x hx
  36  constructor
  37  · intro h
  38    by_contra hne
  39    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
  40  · rintro rfl; exact Jcost_unit0
  41
  42/-- The cost-zero set in ℝ+ has cardinality 1 (in the sense that any two
  43    members are equal). -/
  44theorem cost_zero_set_has_one_member {x y : ℝ}
  45    (hx : 0 < x) (hy : 0 < y)
  46    (hJx : Jcost x = 0) (hJy : Jcost y = 0) :
  47    x = y := by
  48  rw [(cost_zero_set_singleton x hx).mp hJx,
  49      (cost_zero_set_singleton y hy).mp hJy]
  50
  51/-- J-cost is symmetric in log-ratio sense. -/
  52theorem jcost_log_symmetric {x : ℝ} (hx : 0 < x) :
  53    Jcost x = Jcost x⁻¹ := Jcost_symm hx
  54
  55/-- Away from 1, J-cost is strictly positive (isolation). -/
  56theorem jcost_isolated_from_zero {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
  57    0 < Jcost x := Jcost_pos_of_ne_one x hx hne
  58
  59structure ExistenceUniquenessCert where
  60  zero_iff_one : ∀ {x : ℝ}, 0 < x → (Jcost x = 0 ↔ x = 1)
  61  unique_member : ∀ {x y : ℝ}, 0 < x → 0 < y →
  62    Jcost x = 0 → Jcost y = 0 → x = y
  63  log_symmetric : ∀ {x : ℝ}, 0 < x → Jcost x = Jcost x⁻¹
  64  isolated : ∀ {x : ℝ}, 0 < x → x ≠ 1 → 0 < Jcost x
  65
  66/-- Existence uniqueness certificate. -/
  67def existenceUniquenessCert : ExistenceUniquenessCert where
  68  zero_iff_one := @cost_zero_set_singleton
  69  unique_member := @cost_zero_set_has_one_member
  70  log_symmetric := @jcost_log_symmetric
  71  isolated := @jcost_isolated_from_zero
  72
  73end
  74end ExistenceUniquenessFromCost
  75end Foundation
  76end IndisputableMonolith
  77