IndisputableMonolith.Gravity.D2ScalarDirichletPartial

   1import IndisputableMonolith.Gravity.D2ScalarDirichletQuadratureLimit
   2
   3namespace IndisputableMonolith
   4namespace Gravity
   5namespace D2ScalarDirichletPartial
   6
   7open PhysicalSixTetCubicDirichletInstance
   8open D2QuadratureInstances
   9open D2ScalarDirichletQuadratureLimit
  10open D2ScopingAudit
  11open Geometry.ReggeTriangulation3D
  12open Geometry.ReggeHessian3D
  13open Geometry.Triangulation3DConsistency
  14open Geometry.ReggeActionConcrete
  15open Geometry.PeriodicFreudenthalTorus
  16
  17noncomputable section
  18
  19-- §1. The abstract equivalence
  20theorem scalar_dirichlet_limit_nonempty_iff_tendsto
  21    {α ρ : Type*} {l : Filter α}
  22    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
  23    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
  24    (g : ρ → ℝ)
  25    (hg : ∀ r : ρ, (F.slice r).quadratureIntegral = g r) :
  26    Nonempty (ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) ↔
  27    Filter.Tendsto g refinementFilter (nhds continuumIntegral) := by
  28  constructor
  29  · intro h
  30    obtain ⟨H⟩ := h
  31    have heq : g = H.scalarEnergy := by
  32      funext r
  33      exact (hg r).symm.trans (H.proxy_eq r)
  34    rw [heq]
  35    exact H.tendsto
  36  · intro h
  37    refine ⟨?_⟩
  38    exact { scalarEnergy := g, proxy_eq := hg, tendsto := h }
  39
  40-- §2. The constructive direction
  41noncomputable def scalarDirichletLimitOfTendsto
  42    {α ρ : Type*} {l : Filter α}
  43    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
  44    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
  45    (g : ρ → ℝ)
  46    (hg : ∀ r : ρ, (F.slice r).quadratureIntegral = g r)
  47    (htendsto : Filter.Tendsto g refinementFilter (nhds continuumIntegral)) :
  48    ScalarDirichletEnergyLimit F refinementFilter continuumIntegral :=
  49  { scalarEnergy := g, proxy_eq := hg, tendsto := htendsto }
  50
  51-- §3. The equivalence for the quadrature integral sequence
  52theorem scalar_dirichlet_limit_iff_quadrature_tendsto
  53    {α ρ : Type*} {l : Filter α}
  54    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
  55    (refinementFilter : Filter ρ) (continuumIntegral : ℝ) :
  56    Nonempty (ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) ↔
  57    Filter.Tendsto (fun r => (F.slice r).quadratureIntegral) refinementFilter (nhds continuumIntegral) := by
  58  exact scalar_dirichlet_limit_nonempty_iff_tendsto F refinementFilter continuumIntegral
  59    (fun r => (F.slice r).quadratureIntegral) (fun r => rfl)
  60
  61-- §4. The uniform-probe identification
  62theorem uniform_probe_quadratureIntegral_eq_scaled_dirichlet
  63    {α ρ : Type*} {l : Filter α}
  64    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
  65    (r : ρ) :
  66    letI : NeZero (F.slice r).Nx := (F.slice r).instNx
  67    letI : NeZero (F.slice r).Ny := (F.slice r).instNy
  68    letI : NeZero (F.slice r).Nz := (F.slice r).instNz
  69    ∀ ξ : VertexPotential
  70        (canonicalEncodedPeriodicFreudenthalTorus (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz
  71          (F.slice r).hx (F.slice r).hy (F.slice r).hz).K,
  72      (∀ τ : Fin (Fintype.card (PeriodicTet (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz)),
  73        (F.slice r).data.tetProbe (tetFinEquiv (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz τ) = ξ) →
  74      (F.slice r).quadratureIntegral =
  75        (Fintype.card (PeriodicTet (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz) : ℝ) *
  76          ((F.slice r).data.limitCellVolume / 6) *
  77          ((1 / 2) *
  78            canonicalDirichletEnergy
  79              (canonicalEncodedPeriodicFreudenthalTorus (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz
  80                (F.slice r).hx (F.slice r).hy (F.slice r).hz).K
  81              (canonicalEncodedPeriodicFreudenthalTorus (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz
  82                (F.slice r).hx (F.slice r).hy (F.slice r).hz).hK
  83              ξ) := by
  84  exact quadratureIntegral_of_uniform_probe (F.slice r)
  85
  86-- §5. The combined reduction for uniform-probe families
  87theorem uniform_probe_scalar_dirichlet_limit_iff_quadrature_tendsto
  88    {α ρ : Type*} {l : Filter α}
  89    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
  90    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
  91    (huniform : ∀ r : ρ,
  92      letI : NeZero (F.slice r).Nx := (F.slice r).instNx
  93      letI : NeZero (F.slice r).Ny := (F.slice r).instNy
  94      letI : NeZero (F.slice r).Nz := (F.slice r).instNz
  95      ∃ ξ : VertexPotential
  96          (canonicalEncodedPeriodicFreudenthalTorus (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz
  97            (F.slice r).hx (F.slice r).hy (F.slice r).hz).K,
  98        ∀ τ : Fin (Fintype.card (PeriodicTet (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz)),
  99          (F.slice r).data.tetProbe (tetFinEquiv (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz τ) = ξ) :
 100    Nonempty (ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) ↔
 101    Filter.Tendsto (fun r => (F.slice r).quadratureIntegral) refinementFilter (nhds continuumIntegral) := by
 102  -- For uniform-probe families, quadratureIntegral_of_uniform_probe (via
 103  -- uniform_probe_quadratureIntegral_eq_scaled_dirichlet) rewrites the proxy
 104  -- as the scaled Dirichlet energy. The equivalence then follows from
 105  -- scalar_dirichlet_limit_nonempty_iff_tendsto.
 106  exact scalar_dirichlet_limit_nonempty_iff_tendsto F refinementFilter continuumIntegral
 107    (fun r => (F.slice r).quadratureIntegral) (fun r => rfl)
 108
 109end
 110
 111end D2ScalarDirichletPartial
 112end Gravity
 113end IndisputableMonolith