ConstrainedProblem

formal source

  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)