IndisputableMonolith.Gravity.D2ScopingAudit

   1import IndisputableMonolith.Gravity.Track1BCPhysicalResidual
   2import IndisputableMonolith.Gravity.MasterTheoremUnconditional
   3
   4/-!
   5# Gravity: Honest D2 (Regge → Einstein-Hilbert) Scoping Audit
   6
   7## Status: THEOREM (0 sorry, 0 RS-internal axiom) for what is claimed; the
   8## open frontier is named, not asserted.
   9
  10## What this module pins down (peer-review findings F2 / Rec 3)
  11
  12The D2 classical-recovery witness consumed by the master theorem is
  13`MasterTheoremUnconditional.concretePhysicalRegEHContinuumProp`, namely
  14
  15```
  16∀ D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData l, target D
  17```
  18
  19and `physicalReggeEHConcreteProductFilterTarget_holds D` is discharged by
  20`D.fullReggeProduct_tendsto_continuum`.  Reading the structure
  21(`PhysicalSixTetCubicDirichletInstance`), the datum `D` carries **two
  22analytic hypothesis fields**:
  23
  24* `quadrature_tendsto` — the canonical periodic six-tet quadrature rule
  25  converges to the continuum EH/Dirichlet integral, and
  26* `uniform_residual` — the (full nonlinear Regge − quadrature) residual is
  27  uniformly controlled on the product filter.
  28
  29`fullReggeProduct_tendsto_continuum` is a genuine theorem: it combines those
  30two hypotheses by a triangle-inequality squeeze.  So the honest status of
  31D2 is a **reduction**, not a from-primitives closure:
  32
  33> On the canonical periodic six-tet cubic torus, quadrature convergence plus
  34> a vanishing Regge-residual envelope imply full nonlinear Regge → continuum
  35> EH convergence on the product filter.
  36
  37This module states that reduction cleanly (`d2_reduction`), discloses that
  38the D2 target is a real `Tendsto` convergence statement (not `True`), and
  39**names the precise remaining targets** so they are not hidden inside a
  40data structure.
  41
  42## What is NOT proved (the actual open frontier)
  43
  441. `D2QuadratureConvergenceTarget` discharged from primitive mesh geometry
  45   for a concrete refinement family (currently a supplied field).
  462. `D2ResidualVanishingTarget` discharged from a primitive curvature/spacing
  47   bound (currently a supplied field; the residual-envelope constructors in
  48   `PhysicalSixTetCubicDirichletInstance` reduce it to a vanishing envelope,
  49   but the envelope itself is still supplied).
  503. Generalization beyond the canonical periodic, flat, product six-tet torus
  51   to physically admissible **non-product, non-flat** triangulations, with
  52   contracted second Bianchi closure on the same family.
  53
  54Items 1-2 are analytic; item 3 is the load-bearing geometric problem
  55(F2).  None is asserted here.
  56-/
  57
  58namespace IndisputableMonolith
  59namespace Gravity
  60namespace D2ScopingAudit
  61
  62open PhysicalSixTetCubicDirichletInstance
  63
  64/-! ## §1. Disclosure: the D2 target is a genuine convergence statement -/
  65
  66/-- The D2 product-filter target is literally a `Filter.Tendsto` convergence
  67of the full nonlinear Regge aggregate to the continuum integral.  It is not
  68`True` and it does not mention the master conclusion. -/
  69theorem d2_target_is_convergence
  70    {α ρ : Type*} {l : Filter α}
  71    (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
  72    Track1BCPhysicalResidual.PhysicalReggeEHConcreteProductFilterTarget D =
  73      Filter.Tendsto
  74        (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
  75          (α := α) (ρ := ρ) D.family)
  76        (D.refinementFilter ×ˢ l : Filter (ρ × α))
  77        (nhds D.continuumIntegral) := rfl
  78
  79/-! ## §2. The precise remaining analytic targets, named -/
  80
  81/-- **Remaining target 1 (quadrature convergence).**  The canonical periodic
  82six-tet quadrature rule converges to the continuum EH/Dirichlet integral on
  83the cross-cardinality product schedule.  Currently supplied as the
  84`quadrature_tendsto` field of the product-filter datum. -/
  85def D2QuadratureConvergenceTarget
  86    {α ρ : Type*} (l : Filter α)
  87    (family : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
  88    (refinementFilter : Filter ρ) (continuumIntegral : ℝ) : Prop :=
  89  CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
  90    family refinementFilter continuumIntegral
  91
  92/-- **Remaining target 2 (residual vanishing).**  The (full nonlinear Regge −
  93quadrature) residual is uniformly controlled on the product filter.
  94Currently supplied as the `uniform_residual` field. -/
  95def D2ResidualVanishingTarget
  96    {α ρ : Type*} (l : Filter α)
  97    (family : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
  98    (refinementFilter : Filter ρ) : Prop :=
  99  CanonicalPeriodicTetSixTetVolumeQuadratureProductUniformResidualTarget
 100    family refinementFilter
 101
 102/-! ## §3. The proved reduction -/
 103
 104/-- **D2 REDUCTION THEOREM (what is actually proved).**  On the canonical
 105periodic six-tet cubic torus, the two named analytic targets — quadrature
 106convergence to the continuum integral and a vanishing Regge-residual — imply
 107that the full nonlinear Regge aggregate converges to the continuum
 108Einstein-Hilbert/Dirichlet integral on the product filter.
 109
 110This is the honest content of the D2 master witness: convergence is reduced
 111to the two analytic inputs, which remain the open targets (§2).  It makes no
 112claim about non-product or non-flat triangulations. -/
 113theorem d2_reduction
 114    {α ρ : Type*} {l : Filter α}
 115    (family : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
 116    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
 117    (hquad : D2QuadratureConvergenceTarget l family refinementFilter continuumIntegral)
 118    (hres : D2ResidualVanishingTarget l family refinementFilter) :
 119    Filter.Tendsto
 120      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
 121        (α := α) (ρ := ρ) family)
 122      (refinementFilter ×ˢ l : Filter (ρ × α))
 123      (nhds continuumIntegral) :=
 124  (CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData.fullReggeProduct_tendsto_continuum
 125    (α := α) (ρ := ρ) (l := l)
 126    { family := family
 127      refinementFilter := refinementFilter
 128      continuumIntegral := continuumIntegral
 129      quadrature_tendsto := hquad
 130      uniform_residual := hres })
 131
 132/-- The reduction, packaged as a single implication for citation. -/
 133theorem d2_reduction_statement
 134    {α ρ : Type*} {l : Filter α}
 135    (family : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
 136    (refinementFilter : Filter ρ) (continuumIntegral : ℝ) :
 137    D2QuadratureConvergenceTarget l family refinementFilter continuumIntegral →
 138    D2ResidualVanishingTarget l family refinementFilter →
 139    Filter.Tendsto
 140      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
 141        (α := α) (ρ := ρ) family)
 142      (refinementFilter ×ˢ l : Filter (ρ × α))
 143      (nhds continuumIntegral) :=
 144  fun hquad hres => d2_reduction family refinementFilter continuumIntegral hquad hres
 145
 146/-! ## §4. Scope record -/
 147
 148/-- Honest D2 scope: the reduction is proved; the two analytic inputs and the
 149general-triangulation extension are open. -/
 150structure D2ScopeStatus where
 151  reduction_proved : Bool
 152  quadrature_target_open : Bool
 153  residual_target_open : Bool
 154  general_triangulation_open : Bool
 155
 156/-- The current D2 scope on the canonical periodic six-tet torus. -/
 157def d2ScopeStatus : D2ScopeStatus where
 158  reduction_proved := true
 159  quadrature_target_open := true
 160  residual_target_open := true
 161  general_triangulation_open := true
 162
 163end D2ScopingAudit
 164end Gravity
 165end IndisputableMonolith
 166