IndisputableMonolith.NavierStokes.FRCBridge

   1import Mathlib
   2import IndisputableMonolith.NavierStokes.PhiLadderCutoff
   3
   4/-!
   5# Lattice FRC Bridge
   6
   7This module closes the logical loop between the lattice φ-ladder cutoff result
   8and the conditional-completion route from the Navier--Stokes regularity paper.
   9
  10The key point is that on a finite RS lattice the normalized vorticity ratio
  11`ω_max / ω_rms` is automatically finite-volume controlled. This supplies a
  12finite recognition-cost bound, which can then be fed into any abstract
  13conditional-completion route of the form
  14
  15`FRC -> injection_damping -> direction_constancy -> rigid_rotation_veto -> regularity`.
  16
  17The PDE-heavy steps remain external to this module; what is formalized here is
  18the exact logical bridge from the lattice cutoff theorem to the hypothesis used
  19by the conditional paper.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace NavierStokes
  24namespace FRCBridge
  25
  26open PhiLadderCutoff
  27
  28noncomputable section
  29
  30/-! ## Finite-volume lattice profile -/
  31
  32/-- A finite-volume vorticity profile on an RS lattice.
  33
  34`siteCount` is the number of active lattice sites in the finite window.
  35`omegaMax` and `omegaRms` package the relevant scale information.
  36The field `finiteVolumeControl` is the finite-volume norm-equivalence input:
  37on a finite lattice, pointwise amplitude is controlled by `sqrt(siteCount)` times
  38the RMS scale. -/
  39structure FiniteVolumeProfile where
  40  siteCount : ℕ
  41  siteCount_pos : 0 < siteCount
  42  omegaMax : ℝ
  43  omegaRms : ℝ
  44  omegaRms_pos : 0 < omegaRms
  45  omegaRms_le_max : omegaRms ≤ omegaMax
  46  finiteVolumeControl : omegaMax ≤ Real.sqrt siteCount * omegaRms
  47
  48/-- The normalized ratio used by the lattice FRC bridge. -/
  49def normalizedRatio (s : FiniteVolumeProfile) : ℝ :=
  50  s.omegaMax / s.omegaRms
  51
  52theorem normalizedRatio_pos (s : FiniteVolumeProfile) : 0 < normalizedRatio s := by
  53  unfold normalizedRatio
  54  exact div_pos (lt_of_lt_of_le s.omegaRms_pos s.omegaRms_le_max) s.omegaRms_pos
  55
  56theorem normalizedRatio_ge_one (s : FiniteVolumeProfile) : 1 ≤ normalizedRatio s := by
  57  unfold normalizedRatio
  58  exact (one_le_div s.omegaRms_pos).2 s.omegaRms_le_max
  59
  60theorem normalizedRatio_le_sqrt_siteCount (s : FiniteVolumeProfile) :
  61    normalizedRatio s ≤ Real.sqrt s.siteCount := by
  62  unfold normalizedRatio
  63  rw [div_le_iff₀ s.omegaRms_pos]
  64  simpa [mul_comm, mul_left_comm, mul_assoc] using s.finiteVolumeControl
  65
  66/-! ## Bounding J-cost on the lattice -/
  67
  68/-- On the half-line `[1, ∞)`, the canonical cost is bounded by the identity.
  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
 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 :=
 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
 150/-! ## Packaged certificate -/
 151
 152/-- The full logical closure package for the lattice-to-conditional bridge. -/
 153structure FRCBridgeCert where
 154  frc_on_lattice :
 155    ∀ s : FiniteVolumeProfile, RSLatticeFRC s
 156  frc_exists_bound :
 157    ∀ s : FiniteVolumeProfile, LatticeFRC s
 158  conditional_loop :
 159    ∀ (route : ConditionalCompletionRoute FiniteVolumeProfile)
 160      (profile : FiniteVolumeProfile),
 161      (∀ s : FiniteVolumeProfile, RSLatticeFRC s → route.FRC s) →
 162      route.Regularity profile
 163
 164/-- The lattice FRC bridge certificate. -/
 165def frcBridgeCert : FRCBridgeCert where
 166  frc_on_lattice := frc_holds_on_RS_lattice
 167  frc_exists_bound := frc_holds_on_RS_lattice_exists
 168  conditional_loop := fun route profile hFRCBridge =>
 169    lattice_regular_via_direction_constancy route profile hFRCBridge
 170
 171end
 172
 173end FRCBridge
 174end NavierStokes
 175end IndisputableMonolith
 176