IndisputableMonolith.ILG.NOfRMono

   1import Mathlib
   2import IndisputableMonolith.ILG.ParamsKernel
   3
   4namespace IndisputableMonolith
   5namespace ILG
   6
   7noncomputable section
   8
   9/-- Internal guard to keep square-roots well-defined (WIP stub). -/
  10noncomputable def εr : ℝ := 1e-12
  11
  12/-– Analytic global radial shape factor: reuse canonical def. -/
  13@[simp] noncomputable def n_of_r (A r0 p : ℝ) (r : ℝ) : ℝ :=
  14  IndisputableMonolith.ILG.n_of_r A r0 p r
  15
  16/-- Monotonicity in A under nonnegative exponent (delegates to canonical proof). -/
  17lemma n_of_r_mono_A_of_nonneg_p {A1 A2 r0 p r : ℝ}
  18  (hp : 0 ≤ p) (hA12 : A1 ≤ A2) :
  19  n_of_r A1 r0 p r ≤ n_of_r A2 r0 p r := by
  20  dsimp [n_of_r]
  21  exact IndisputableMonolith.ILG.n_of_r_mono_A_of_nonneg_p (hp:=hp) (hA12:=hA12)
  22
  23end
  24end ILG
  25end IndisputableMonolith
  26