totalCost

formal source

  34noncomputable def J_curv (lambda : ℝ) : ℝ := 2 * lambda ^ 2
  35
  36/-- Total cost functional. -/
  37noncomputable def totalCost (lambda : ℝ) : ℝ :=
  38  J_bit_normalized + J_curv lambda
  39
  40/-- Balance residual: vanishes at the optimal scale. -/
  41noncomputable def balanceResidual (lambda : ℝ) : ℝ :=
  42  J_curv lambda - J_bit_normalized
  43
  44/-- The balance point in RS-native dimensionless units. -/
  45noncomputable def lambda_0 : ℝ := 1 / Real.sqrt 2
  46
  47lemma lambda_0_pos : 0 < lambda_0 := by
  48  unfold lambda_0
  49  apply div_pos one_pos
  50  exact Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
  51
  52/-- lambda_0² = 1/2. -/
  53lemma lambda_0_sq : lambda_0 ^ 2 = 1 / 2 := by
  54  unfold lambda_0
  55  rw [div_pow]
  56  have h2 : (0 : ℝ) ≤ 2 := by norm_num
  57  rw [Real.sq_sqrt h2]
  58  norm_num
  59
  60/-- The balance residual vanishes at lambda_0. -/
  61theorem balance_at_lambda_0 : balanceResidual lambda_0 = 0 := by
  62  unfold balanceResidual J_curv J_bit_normalized
  63  rw [lambda_0_sq]
  64  ring
  65
  66/-- lambda_0 is the unique positive root of the balance residual. -/
  67theorem balance_unique_positive_root (lambda : ℝ) (hlambda : lambda > 0) :