close_conditional_loop

formal source

 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 :=
 123    route.injectionDamping_to_directionConstancy a hID
 124  have hRR : route.RigidRotationVeto a :=
 125    route.directionConstancy_to_rigidRotationVeto a hDC
 126  exact route.rigidRotationVeto_to_regularity a hRR
 127
 128/-- A regularity certificate obtained by running the conditional route on a
 129finite RS lattice profile. -/
 130structure LatticeRegularityCertificate
 131    (route : ConditionalCompletionRoute FiniteVolumeProfile)
 132    (profile : FiniteVolumeProfile) where
 133  frcBound : ℝ
 134  frcBound_nonneg : 0 ≤ frcBound
 135  frcProof : RSLatticeFRC profile
 136  injectionDamping : route.InjectionDamping profile
 137  directionConstancy : route.DirectionConstancy profile
 138  rigidRotationVeto : route.RigidRotationVeto profile
 139  regularity : route.Regularity profile
 140
 141/-- The lattice FRC theorem is enough to instantiate the conditional route. -/
 142theorem lattice_regular_via_direction_constancy
 143    (route : ConditionalCompletionRoute FiniteVolumeProfile)
 144    (profile : FiniteVolumeProfile)
 145    (hFRCBridge : ∀ s : FiniteVolumeProfile, RSLatticeFRC s → route.FRC s) :
 146    route.Regularity profile := by
 147  apply close_conditional_loop route
 148  exact hFRCBridge profile (frc_holds_on_RS_lattice profile)
 149