finiteVolume_Jcost_bound

formal source

  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
 103/-- Abstract interface for the conditional-completion route.
 104
 105This isolates the heavy PDE part of the argument while making the logical bridge
 106fully explicit in Lean. -/
 107structure ConditionalCompletionRoute (α : Type) where
 108  FRC : α → Prop
 109  InjectionDamping : α → Prop