IndisputableMonolith.Gravity.ReggeCubicLatticeLimit

   1import Mathlib
   2import IndisputableMonolith.Geometry.ReggeActionSecondVariation
   3import IndisputableMonolith.Gravity.CubicReggeConvergence
   4
   5/-!
   6# Cubic-Lattice Limit for the Second-Order Regge Action
   7
   8The general CMS theorem gives a weak curvature-measure convergence statement,
   9not a plain `O(a^2)` action estimate.  The `O(a^2)` statement belongs to the
  10regular weak-field cubic-lattice case.  This module isolates that special
  11case for the canonical second-order Regge action.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Gravity
  16namespace ReggeCubicLatticeLimit
  17
  18open Geometry.ReggeTriangulation3D
  19open Geometry.ReggeHessian3D
  20open Geometry.Triangulation3DConsistency
  21open Geometry.ReggeActionConcrete
  22
  23noncomputable section
  24
  25/-- A regular cubic-lattice comparison model for the canonical second-order
  26Regge action. -/
  27structure RegularCubicLatticeModel
  28    (K : Triangulation3D) (hK : IncidenceConsistent K) where
  29  latticeSpacing : ℝ
  30  spacing_pos : 0 < latticeSpacing
  31  continuumAction : VertexPotential K → ℝ
  32  errorConstant : ℝ
  33  errorConstant_nonneg : 0 ≤ errorConstant
  34  secondOrder_action_error :
  35    ∀ ξ : VertexPotential K,
  36      |reggeActionSecondOrder K hK (canonicalReggeHessian K hK) ξ -
  37        continuumAction ξ| ≤ errorConstant * latticeSpacing ^ (2 : ℕ)
  38
  39/-- The second-order Regge action has an `O(a^2)` cubic-lattice continuum
  40limit in the supplied regular lattice model. -/
  41def ReggeSecondOrderCubicLatticeLimit
  42    (K : Triangulation3D) (hK : IncidenceConsistent K)
  43    (M : RegularCubicLatticeModel K hK) : Prop :=
  44  ∀ ξ : VertexPotential K,
  45    |reggeActionSecondOrder K hK (canonicalReggeHessian K hK) ξ -
  46      M.continuumAction ξ| ≤ M.errorConstant * M.latticeSpacing ^ (2 : ℕ)
  47
  48/-- Named input connecting a concrete regular triangulation model to the
  49canonical second-order Regge action. -/
  50structure ReggeCubicLatticeLimitInput
  51    (K : Triangulation3D) (hK : IncidenceConsistent K) where
  52  model : RegularCubicLatticeModel K hK
  53  limit_estimate : ReggeSecondOrderCubicLatticeLimit K hK model
  54
  55/-- Physical six-tet cubic Dirichlet model data.  This is the target class
  56for the real cubic-lattice instance: prove that the canonical second-order
  57Regge action on the six-tetrahedra-per-cube triangulation is the finite-
  58difference Dirichlet action, then supply the O(a^2) estimate. -/
  59structure PhysicalSixTetCubicDirichletModel
  60    (K : Triangulation3D) (hK : IncidenceConsistent K) where
  61  regularModel : RegularCubicLatticeModel K hK
  62  sixTetCubicDecomposition : Prop
  63  canonicalHessian_is_dirichlet : Prop
  64  finiteDifferenceEstimate :
  65    ReggeSecondOrderCubicLatticeLimit K hK regularModel
  66
  67def cubicLatticeLimitInput_of_physicalSixTetModel
  68    (K : Triangulation3D) (hK : IncidenceConsistent K)
  69    (M : PhysicalSixTetCubicDirichletModel K hK) :
  70    ReggeCubicLatticeLimitInput K hK where
  71  model := M.regularModel
  72  limit_estimate := M.finiteDifferenceEstimate
  73
  74/-- Phase-G cubic-lattice `O(a^2)` continuum-limit theorem for the canonical
  75second-order Regge action. -/
  76theorem reggeActionSecondOrder_cubic_lattice_limit
  77    (K : Triangulation3D) (hK : IncidenceConsistent K)
  78    (h_limit : ReggeCubicLatticeLimitInput K hK) :
  79    ReggeSecondOrderCubicLatticeLimit K hK h_limit.model :=
  80  h_limit.limit_estimate
  81
  82/-- A family of cubic-lattice comparison models converges pointwise whenever
  83its certified `O(a^2)` error envelope tends to zero along the refinement
  84parameter. -/
  85theorem reggeSecondOrderCubicLatticeLimit_error_vanishes_along_models
  86    {α : Type*} {l : Filter α}
  87    (K : Triangulation3D) (hK : IncidenceConsistent K)
  88    (M : α → RegularCubicLatticeModel K hK)
  89    (hLimit : ∀ t : α, ReggeSecondOrderCubicLatticeLimit K hK (M t))
  90    (hEnvelope :
  91      Filter.Tendsto
  92        (fun t : α => (M t).errorConstant * (M t).latticeSpacing ^ (2 : ℕ))
  93        l (nhds 0))
  94    (ξ : VertexPotential K) :
  95    Filter.Tendsto
  96      (fun t : α =>
  97        |reggeActionSecondOrder K hK (canonicalReggeHessian K hK) ξ -
  98          (M t).continuumAction ξ|)
  99      l (nhds 0) := by
 100  apply squeeze_zero
 101  · intro t
 102    exact abs_nonneg _
 103  · intro t
 104    exact hLimit t ξ
 105  · exact hEnvelope
 106
 107/-- The existing one-dimensional finite-difference theorem is the analytic
 108ingredient used in the cubic-lattice model. -/
 109theorem finite_difference_second_order_estimate
 110    (f : ℝ → ℝ) (x a : ℝ) (ha : a ≠ 0) (hf : ContDiff ℝ 4 f) :
 111    ∃ C : ℝ, 0 ≤ C ∧
 112      |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 -
 113        deriv (deriv f) x| ≤ C * a ^ 2 :=
 114  CubicReggeConvergence.weak_field_error_estimate f x a ha hf
 115
 116/-- Exact comparison model: the continuum action is chosen to be the
 117canonical second-order Regge action itself, so the error constant is zero.
 118
 119This is not the physical regular cubic-lattice continuum model.  It is a
 120sanity-check instance showing that `RegularCubicLatticeModel` and
 121`ReggeCubicLatticeLimitInput` are constructible without further caller data.
 122The real cubic-lattice instance still has to identify this action with the
 123finite-difference Dirichlet action. -/
 124def exactSecondOrderComparisonModel
 125    (K : Triangulation3D) (hK : IncidenceConsistent K)
 126    (a : ℝ) (ha : 0 < a) :
 127    RegularCubicLatticeModel K hK where
 128  latticeSpacing := a
 129  spacing_pos := ha
 130  continuumAction := reggeActionSecondOrder K hK (canonicalReggeHessian K hK)
 131  errorConstant := 0
 132  errorConstant_nonneg := le_rfl
 133  secondOrder_action_error := by
 134    intro ξ
 135    simp
 136
 137def exactSecondOrderCubicLatticeLimitInput
 138    (K : Triangulation3D) (hK : IncidenceConsistent K)
 139    (a : ℝ) (ha : 0 < a) :
 140    ReggeCubicLatticeLimitInput K hK where
 141  model := exactSecondOrderComparisonModel K hK a ha
 142  limit_estimate := by
 143    intro ξ
 144    simp [exactSecondOrderComparisonModel]
 145
 146end
 147
 148end ReggeCubicLatticeLimit
 149end Gravity
 150end IndisputableMonolith
 151