IndisputableMonolith.Gravity.D2ScalarDirichletQuadratureLimit

   1import IndisputableMonolith.Gravity.D2QuadratureInstances
   2
   3/-!
   4# D2 Scalar Dirichlet Quadrature Limit: the Curvature-Bearing Conditional
   5
   6## Status: THEOREM (0 gaps, 0 RS-internal axiom) for what is claimed; the
   7## scalar Dirichlet limit for curvature-bearing probes remains the named open
   8## analytic input.
   9
  10## What this module adds
  11
  12This module makes the sharpest honest progress on the remaining open D2
  13quadrature target: the curvature-bearing scalar graph-Dirichlet quadrature
  14limit flagged by `D2ScopingAudit` as the sole remaining analytic input after
  15the damped-schedule residual closure.
  16
  17**The conditional implication (proved).**  We define
  18`ScalarDirichletEnergyLimit`, a clearly-named structure packaging the scalar
  19Dirichlet energy limit hypothesis: a scalar energy function `g : ρ → ℝ`
  20connected to the quadrature proxies by `proxy_eq` and converging to the
  21continuum integral by `tendsto`.  We prove that this hypothesis implies the
  22D2 quadrature convergence target
  23(`scalar_dirichlet_limit_implies_d2_quadrature_target`), using the
  24proxy-transport theorem `D2QuadratureInstances.quadrature_target_iff_of_proxy_eq`.
  25
  26**Combination with the damped-schedule closure (proved).**  Since
  27`D2DampedScheduleClosure.dampedFamily_fullReggeProduct_tendsto_continuum`
  28consumes the quadrature target for the original family and discharges the
  29residual target internally for damped schedules, the scalar Dirichlet energy
  30limit alone suffices for the full D2 product-filter convergence
  31(`scalar_limit_and_damped_implies_full_convergence`).
  32
  33**The flat case as a trivial scalar limit (proved).**  The flat family
  34(zero probes) satisfies `ScalarDirichletEnergyLimit` at zero trivially
  35(`flatFamily_scalarDirichletLimit`), recovering the flat-sector quadrature
  36target and full product-filter convergence via the scalar Dirichlet route
  37(`flatFamily_quadrature_target_via_scalar_limit`,
  38`dampedFlat_fullReggeProduct_tendsto_zero_via_scalar_limit`).
  39
  40## What remains open
  41
  42The `tendsto` field of `ScalarDirichletEnergyLimit` for curvature-bearing
  43uniform-probe families — the concrete numerical limit of finite
  44graph-Dirichlet energies — is the genuine Riemann-sum content of D2 and is
  45not proved here.  For uniform-probe slices, the `proxy_eq` field is
  46discharged by `D2QuadratureInstances.quadratureIntegral_of_uniform_probe`,
  47which collapses the quadrature proxy to
  48`(card tets) · (V/6) · (½ · DirichletEnergy ξ)`.
  49-/
  50
  51namespace IndisputableMonolith
  52namespace Gravity
  53namespace D2ScalarDirichletQuadratureLimit
  54
  55open PhysicalSixTetCubicDirichletInstance
  56open D2QuadratureInstances
  57open D2ScopingAudit
  58open D2DampedScheduleClosure
  59
  60noncomputable section
  61
  62/-! ## §1. The scalar Dirichlet energy limit hypothesis -/
  63
  64/-- The scalar Dirichlet energy limit hypothesis for a quadrature refinement
  65family.  This packages the explicit numerical limit of finite graph-Dirichlet
  66energies that the D2 quadrature target reduces to for uniform-probe families.
  67
  68For uniform-probe families, the `proxy_eq` field is discharged by
  69`D2QuadratureInstances.quadratureIntegral_of_uniform_probe`, which collapses
  70the quadrature proxy to `(card tets) · (V/6) · (½ · DirichletEnergy ξ)`.
  71The `tendsto` field is then the concrete scalar Dirichlet energy limit — the
  72genuine Riemann-sum content of D2 that remains open for curvature-bearing
  73probes. -/
  74structure ScalarDirichletEnergyLimit
  75    {α ρ : Type*} {l : Filter α}
  76    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
  77    (refinementFilter : Filter ρ) (continuumIntegral : ℝ) where
  78  /-- The scalar energy function: typically the scaled Dirichlet energy of
  79  the uniform probe at each refinement. -/
  80  scalarEnergy : ρ → ℝ
  81  /-- The scalar energy computes the quadrature proxy at each refinement.
  82  For uniform-probe slices, this is `quadratureIntegral_of_uniform_probe`. -/
  83  proxy_eq : ∀ r : ρ, (F.slice r).quadratureIntegral = scalarEnergy r
  84  /-- The scalar Dirichlet energies converge to the continuum integral.
  85  This is the open analytic input for curvature-bearing probe families. -/
  86  tendsto : Filter.Tendsto scalarEnergy refinementFilter (nhds continuumIntegral)
  87
  88/-! ## §2. The main conditional implication -/
  89
  90/-- **The scalar Dirichlet energy limit implies the D2 quadrature convergence
  91target.**  This is the sharpest honest conditional implication for the
  92curvature-bearing sector: if a scalar sequence of graph-Dirichlet energies
  93(connected to the quadrature proxies by `proxy_eq`) converges to the
  94continuum integral, then the D2 quadrature convergence target holds.
  95
  96Combined with the damped-schedule residual closure
  97(`D2DampedScheduleClosure`), this reduces the full D2 product-filter
  98convergence to the scalar Dirichlet energy limit alone (see
  99`scalar_limit_and_damped_implies_full_convergence`).
 100
 101The scalar limit itself for curvature-bearing probes remains the open
 102analytic content of D2. -/
 103theorem scalar_dirichlet_limit_implies_d2_quadrature_target
 104    {α ρ : Type*} {l : Filter α}
 105    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
 106    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
 107    (H : ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) :
 108    D2ScopingAudit.D2QuadratureConvergenceTarget l F refinementFilter continuumIntegral :=
 109  (quadrature_target_iff_of_proxy_eq
 110    F refinementFilter continuumIntegral H.scalarEnergy H.proxy_eq).mpr H.tendsto
 111
 112/-! ## §3. Combination with the damped-schedule closure -/
 113
 114/-- **The scalar Dirichlet energy limit plus the damped schedule implies full
 115D2 product-filter convergence.**  Since the damped-schedule closure
 116discharges the uniform residual target unconditionally for damped schedules
 117(via `dampedFamily_fullReggeProduct_tendsto_continuum`), the scalar
 118Dirichlet energy limit alone suffices for the full nonlinear Regge aggregate
 119to converge to the continuum Einstein-Hilbert/Dirichlet integral on the
 120product filter.
 121
 122This is the sharpest reduction of D2 to a single analytic input: the scalar
 123graph-Dirichlet energy limit for curvature-bearing probe families. -/
 124theorem scalar_limit_and_damped_implies_full_convergence
 125    {α ρ : Type*} {l : Filter α}
 126    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
 127    (σ : α → ℝ)
 128    (hσ0 : Filter.Tendsto σ l (nhds 0))
 129    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
 130    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
 131    (H : ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) :
 132    Filter.Tendsto
 133      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
 134        (α := α) (ρ := ρ) (dampedFamily F σ hσ0 hσne))
 135      (refinementFilter ×ˢ l : Filter (ρ × α))
 136      (nhds continuumIntegral) :=
 137  dampedFamily_fullReggeProduct_tendsto_continuum F σ hσ0 hσne
 138    refinementFilter continuumIntegral
 139    (scalar_dirichlet_limit_implies_d2_quadrature_target F refinementFilter
 140      continuumIntegral H)
 141
 142/-! ## §4. The flat case as a trivial scalar limit -/
 143
 144/-- The flat family satisfies the scalar Dirichlet energy limit at zero:
 145the scalar energy is identically zero (the Dirichlet energy of the zero
 146potential vanishes), and zero converges to zero. -/
 147noncomputable def flatFamily_scalarDirichletLimit
 148    {α ρ : Type*} {l : Filter α}
 149    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
 150    (refinementFilter : Filter ρ) :
 151    ScalarDirichletEnergyLimit (flatFamily F) refinementFilter 0 where
 152  scalarEnergy := fun _ => 0
 153  proxy_eq := by
 154    intro r
 155    exact flattenSlice_quadratureIntegral (F.slice r)
 156  tendsto := tendsto_const_nhds
 157
 158/-- The flat-sector quadrature target follows from the scalar limit
 159hypothesis, recovering `D2QuadratureInstances.flatFamily_quadrature_target`
 160via the scalar Dirichlet route. -/
 161theorem flatFamily_quadrature_target_via_scalar_limit
 162    {α ρ : Type*} {l : Filter α}
 163    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
 164    (refinementFilter : Filter ρ) :
 165    D2ScopingAudit.D2QuadratureConvergenceTarget l (flatFamily F) refinementFilter 0 :=
 166  scalar_dirichlet_limit_implies_d2_quadrature_target (flatFamily F) refinementFilter 0
 167    (flatFamily_scalarDirichletLimit F refinementFilter)
 168
 169/-- The flat-sector full product-filter convergence follows from the scalar
 170limit hypothesis, recovering
 171`D2QuadratureInstances.dampedFlat_fullReggeProduct_tendsto_zero` via the
 172scalar Dirichlet route. -/
 173theorem dampedFlat_fullReggeProduct_tendsto_zero_via_scalar_limit
 174    {α ρ : Type*} {l : Filter α}
 175    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
 176    (σ : α → ℝ)
 177    (hσ0 : Filter.Tendsto σ l (nhds 0))
 178    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
 179    (refinementFilter : Filter ρ) :
 180    Filter.Tendsto
 181      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
 182        (α := α) (ρ := ρ) (dampedFamily (flatFamily F) σ hσ0 hσne))
 183      (refinementFilter ×ˢ l : Filter (ρ × α))
 184      (nhds 0) :=
 185  scalar_limit_and_damped_implies_full_convergence (flatFamily F) σ hσ0 hσne
 186    refinementFilter 0 (flatFamily_scalarDirichletLimit F refinementFilter)
 187
 188end
 189
 190end D2ScalarDirichletQuadratureLimit
 191end Gravity
 192end IndisputableMonolith