universalSensitivity_eq

formal source

  66    equilibrium is 1/2. This is the meta-claim referenced in C7. -/
  67noncomputable def universalSensitivity : ℝ := 1 / 2
  68
  69theorem universalSensitivity_eq : universalSensitivity = 1 / 2 := rfl
  70
  71/-- The leading-order J-cost is sensitivity × δ². -/
  72theorem leading_order (δ : ℝ) :
  73    universalSensitivity * δ^2 = δ^2 / 2 := by
  74  unfold universalSensitivity
  75  ring
  76
  77/-- For small symmetric perturbations, J(1+δ) and J(1-δ) match at leading
  78    order: their sum equals δ²/2 · (1/(1+δ) + 1/(1-δ)) which → δ² as δ→0.
  79    Concretely we prove the algebraic identity. -/
  80theorem jcost_symmetric_pair (δ : ℝ) (hδ : 0 < 1 - δ) (hδ' : 0 < 1 + δ) :
  81    Jcost (1 + δ) + Jcost (1 - δ) =
  82    δ^2 / (2 * (1 + δ)) + δ^2 / (2 * (1 - δ)) := by
  83  rw [jcost_at_one_plus_delta δ hδ']
  84  have h : Jcost (1 - δ) = δ^2 / (2 * (1 - δ)) := by
  85    have := jcost_at_one_plus_delta (-δ) (by linarith)
  86    -- 1 + (-δ) = 1 - δ, so this gives J(1 - δ) = δ²/(2(1-δ))
  87    have heq : (1 : ℝ) + (-δ) = 1 - δ := by ring
  88    rw [heq] at this
  89    rw [this]
  90    have hsq : (-δ)^2 = δ^2 := by ring
  91    rw [hsq]
  92  rw [h]
  93
  94structure JConvexityUniversalityCert where
  95  squared_form : ∀ {r : ℝ}, 0 < r → Jcost r = (r - 1)^2 / (2 * r)
  96  upper_bound : ∀ {r : ℝ}, 1 ≤ r → Jcost r ≤ (r - 1)^2 / 2
  97  at_equilibrium : Jcost 1 = 0
  98  log_symmetry : ∀ {r : ℝ}, 0 < r → Jcost r = Jcost r⁻¹
  99  sensitivity_constant : universalSensitivity = 1 / 2