eulerScalarProxy

formal source

 170
 171This is no longer a placeholder constant: it is computed from the actual Euler
 172carrier value, derivative bound, and admissible strip radius of the sensor. -/
 173noncomputable def eulerScalarProxy (sensor : DefectSensor) (N : ℕ) : ℝ :=
 174  1 / (1 + eulerScalarGap sensor / (N + 1 : ℝ))
 175
 176/-- The concrete Euler scalar proxy stays positive at every refinement depth. -/
 177theorem eulerScalarProxy_pos (sensor : DefectSensor) (N : ℕ) :
 178    0 < eulerScalarProxy sensor N := by
 179  unfold eulerScalarProxy
 180  apply one_div_pos.mpr
 181  have hgap_nonneg : 0 ≤ eulerScalarGap sensor := le_of_lt (eulerScalarGap_pos sensor)
 182  have hfrac_nonneg : 0 ≤ eulerScalarGap sensor / (N + 1 : ℝ) := by
 183    exact div_nonneg hgap_nonneg (by positivity)
 184  linarith
 185
 186/-- Closed form of the T1 defect on the reciprocal-affine Euler scalar proxy. -/
 187private theorem defect_one_div_one_add (t : ℝ) (ht : 0 ≤ t) :
 188    IndisputableMonolith.Foundation.LawOfExistence.defect (1 / (1 + t)) =
 189      t ^ 2 / (2 * (1 + t)) := by
 190  unfold IndisputableMonolith.Foundation.LawOfExistence.defect
 191    IndisputableMonolith.Foundation.LawOfExistence.J
 192  have hden : (1 + t : ℝ) ≠ 0 := by linarith
 193  field_simp [hden]
 194  ring
 195
 196/-- The Euler scalar proxy has uniformly bounded T1 defect. -/
 197theorem eulerScalarProxy_defect_bounded (sensor : DefectSensor) :
 198    ∃ K : ℝ, ∀ N : ℕ,
 199      IndisputableMonolith.Foundation.LawOfExistence.defect
 200        (eulerScalarProxy sensor N) ≤ K := by
 201  refine ⟨(eulerScalarGap sensor) ^ 2 / 2, ?_⟩
 202  intro N
 203  let t : ℝ := eulerScalarGap sensor / (N + 1 : ℝ)