ConditionalCompletionRoute

formal source

 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 :=
 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