LatticeFRC

formal source

  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
 110  DirectionConstancy : α → Prop
 111  RigidRotationVeto : α → Prop
 112  Regularity : α → Prop
 113  frc_to_injectionDamping : ∀ a, FRC a → InjectionDamping a
 114  injectionDamping_to_directionConstancy : ∀ a, InjectionDamping a → DirectionConstancy a
 115  directionConstancy_to_rigidRotationVeto : ∀ a, DirectionConstancy a → RigidRotationVeto a
 116  rigidRotationVeto_to_regularity : ∀ a, RigidRotationVeto a → Regularity a
 117
 118/-- Once FRC is known on the lattice, any conditional-completion route closes. -/
 119theorem close_conditional_loop {α : Type} (route : ConditionalCompletionRoute α) {a : α}
 120    (hFRC : route.FRC a) : route.Regularity a := by
 121  have hID : route.InjectionDamping a := route.frc_to_injectionDamping a hFRC
 122  have hDC : route.DirectionConstancy a :=