Jcost_le_self_of_one_le

formal source

  69
  70This is the simple estimate needed for the finite-volume FRC bound:
  71`J(x) = (x + x⁻¹)/2 - 1 ≤ x` whenever `x ≥ 1`. -/
  72theorem Jcost_le_self_of_one_le {x : ℝ} (hx : 1 ≤ x) : Jcost x ≤ x := by
  73  unfold Jcost
  74  have hinv_one : x⁻¹ ≤ 1 := inv_le_one_of_one_le₀ hx
  75  have hinv_le : x⁻¹ ≤ x := le_trans hinv_one hx
  76  linarith
  77
  78/-- The explicit finite-volume recognition-cost bound on the RS lattice. -/
  79theorem finiteVolume_Jcost_bound (s : FiniteVolumeProfile) :
  80    Jcost (normalizedRatio s) ≤ Real.sqrt s.siteCount := by
  81  have h₁ : 1 ≤ normalizedRatio s := normalizedRatio_ge_one s
  82  have h₂ : Jcost (normalizedRatio s) ≤ normalizedRatio s :=
  83    Jcost_le_self_of_one_le h₁
  84  exact le_trans h₂ (normalizedRatio_le_sqrt_siteCount s)
  85
  86/-- Strong lattice FRC: the cost is bounded by the explicit finite-volume constant
  87`sqrt(siteCount)`. -/
  88def RSLatticeFRC (s : FiniteVolumeProfile) : Prop :=
  89  Jcost (normalizedRatio s) ≤ Real.sqrt s.siteCount
  90
  91/-- Weak lattice FRC: there exists some finite bound. -/
  92def LatticeFRC (s : FiniteVolumeProfile) : Prop :=
  93  ∃ B : ℝ, Jcost (normalizedRatio s) ≤ B
  94
  95theorem frc_holds_on_RS_lattice (s : FiniteVolumeProfile) : RSLatticeFRC s :=
  96  finiteVolume_Jcost_bound s
  97
  98theorem frc_holds_on_RS_lattice_exists (s : FiniteVolumeProfile) : LatticeFRC s :=
  99  ⟨Real.sqrt s.siteCount, frc_holds_on_RS_lattice s⟩
 100
 101/-! ## Abstract conditional-completion route -/
 102