IndisputableMonolith.Gravity.ReggeConvergenceRegistry

   1import Mathlib
   2import IndisputableMonolith.Gravity.NonlinearConvergence
   3
   4/-!
   5# Regge Convergence Registry
   6
   7This module consolidates the four external convergence Propositions currently
   8scattered in `NonlinearConvergence.lean` into a single named structure
   9`ReggeConvergenceRegistry`.
  10
  11The registry is a **faithful repackaging**: each field is typed by the exact
  12original proposition from `NonlinearConvergence`, and the faithful-projection
  13theorems below show that each registry field recovers the corresponding
  14original proposition.  No convergence content is restated or re-proved; only
  15references to the existing propositions are repackaged.
  16
  17## Provenance
  18
  19The four convergence inputs are external-mathematics results:
  20
  21- `cms_measure_bound`: Cheeger–Müller–Schrader (1984), Theorem 5.1 —
  22  curvature-measure convergence with `η^(1/2)` bulk + boundary-tube term.
  23  Status: external theorem, axiomatized.
  24- `special_quadratic`: stronger `O(a²)` action-convergence hypothesis
  25  used in special weak-field / numerical settings.
  26  Status: external hypothesis, axiomatized.
  27- `ricci_convergence`: Regge Ricci-scalar convergence at `O(a²)`.
  28  Status: external hypothesis, axiomatized.
  29- `riemann_convergence`: Regge holonomy / Riemann convergence.
  30  Status: external hypothesis, axiomatized.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Gravity
  35
  36open NonlinearConvergence
  37
  38namespace ReggeConvergenceRegistry
  39
  40/-! ## The registry structure -/
  41
  42/-- A registry that consolidates the four external convergence Propositions
  43from `NonlinearConvergence` into a single named structure.
  44
  45Each field is typed by the **exact** original proposition, so this is a
  46faithful repackaging, not a weakening.  The `provenance` field documents
  47each input as an external-mathematics result with a status tag. -/
  48structure ReggeConvergenceRegistry where
  49  /-- CMS Theorem 5.1 curvature-measure bound (Cheeger–Müller–Schrader 1984). -/
  50  cms_measure_bound : cms_theorem_5_1_measure_bound
  51  /-- Special-purpose `O(a²)` action-convergence hypothesis. -/
  52  special_quadratic : special_quadratic_regge_to_eh_convergence_hypothesis
  53  /-- Regge Ricci-scalar convergence axiom. -/
  54  ricci_convergence : regge_ricci_convergence_axiom
  55  /-- Regge Riemann / holonomy convergence axiom. -/
  56  riemann_convergence : regge_riemann_convergence_axiom
  57  /-- Documentation of each external-math result with a status tag. -/
  58  provenance : List String
  59
  60/-! ## Faithful-projection theorems
  61
  62These theorems show that each registry field, when projected from a registry
  63value, yields a proof of the **exact** original proposition from
  64`NonlinearConvergence`.  This confirms the registry is a faithful
  65repackaging, not a weakening. -/
  66
  67/-- The `cms_measure_bound` field of a registry is a proof of the original
  68`cms_theorem_5_1_measure_bound` proposition from `NonlinearConvergence`. -/
  69theorem cms_measure_bound_faithful (r : ReggeConvergenceRegistry) :
  70    cms_theorem_5_1_measure_bound := r.cms_measure_bound
  71
  72/-- The `special_quadratic` field of a registry is a proof of the original
  73`special_quadratic_regge_to_eh_convergence_hypothesis` proposition. -/
  74theorem special_quadratic_faithful (r : ReggeConvergenceRegistry) :
  75    special_quadratic_regge_to_eh_convergence_hypothesis := r.special_quadratic
  76
  77/-- The `ricci_convergence` field of a registry is a proof of the original
  78`regge_ricci_convergence_axiom` proposition. -/
  79theorem ricci_convergence_faithful (r : ReggeConvergenceRegistry) :
  80    regge_ricci_convergence_axiom := r.ricci_convergence
  81
  82/-- The `riemann_convergence` field of a registry is a proof of the original
  83`regge_riemann_convergence_axiom` proposition. -/
  84theorem riemann_convergence_faithful (r : ReggeConvergenceRegistry) :
  85    regge_riemann_convergence_axiom := r.riemann_convergence
  86
  87/-! ## Construction from original propositions -/
  88
  89/-- Given proofs of all four original propositions and a provenance list,
  90construct a `ReggeConvergenceRegistry`.  This is the converse of the
  91faithful-projection theorems, showing the registry is a faithful
  92repackaging. -/
  93def mk (h1 : cms_theorem_5_1_measure_bound)
  94    (h2 : special_quadratic_regge_to_eh_convergence_hypothesis)
  95    (h3 : regge_ricci_convergence_axiom)
  96    (h4 : regge_riemann_convergence_axiom)
  97    (prov : List String) : ReggeConvergenceRegistry where
  98  cms_measure_bound := h1
  99  special_quadratic := h2
 100  ricci_convergence := h3
 101  riemann_convergence := h4
 102  provenance := prov
 103
 104/-- Projecting the `cms_measure_bound` field of a registry built via `mk`
 105recovers the original proof. -/
 106theorem mk_cms_measure_bound
 107    (h1 : cms_theorem_5_1_measure_bound)
 108    (h2 : special_quadratic_regge_to_eh_convergence_hypothesis)
 109    (h3 : regge_ricci_convergence_axiom)
 110    (h4 : regge_riemann_convergence_axiom)
 111    (prov : List String) :
 112    (mk h1 h2 h3 h4 prov).cms_measure_bound = h1 := rfl
 113
 114/-- Projecting the `special_quadratic` field of a registry built via `mk`
 115recovers the original proof. -/
 116theorem mk_special_quadratic
 117    (h1 : cms_theorem_5_1_measure_bound)
 118    (h2 : special_quadratic_regge_to_eh_convergence_hypothesis)
 119    (h3 : regge_ricci_convergence_axiom)
 120    (h4 : regge_riemann_convergence_axiom)
 121    (prov : List String) :
 122    (mk h1 h2 h3 h4 prov).special_quadratic = h2 := rfl
 123
 124/-- Projecting the `ricci_convergence` field of a registry built via `mk`
 125recovers the original proof. -/
 126theorem mk_ricci_convergence
 127    (h1 : cms_theorem_5_1_measure_bound)
 128    (h2 : special_quadratic_regge_to_eh_convergence_hypothesis)
 129    (h3 : regge_ricci_convergence_axiom)
 130    (h4 : regge_riemann_convergence_axiom)
 131    (prov : List String) :
 132    (mk h1 h2 h3 h4 prov).ricci_convergence = h3 := rfl
 133
 134/-- Projecting the `riemann_convergence` field of a registry built via `mk`
 135recovers the original proof. -/
 136theorem mk_riemann_convergence
 137    (h1 : cms_theorem_5_1_measure_bound)
 138    (h2 : special_quadratic_regge_to_eh_convergence_hypothesis)
 139    (h3 : regge_ricci_convergence_axiom)
 140    (h4 : regge_riemann_convergence_axiom)
 141    (prov : List String) :
 142    (mk h1 h2 h3 h4 prov).riemann_convergence = h4 := rfl
 143
 144/-- Projecting the `provenance` field of a registry built via `mk`
 145recovers the original list. -/
 146theorem mk_provenance
 147    (h1 : cms_theorem_5_1_measure_bound)
 148    (h2 : special_quadratic_regge_to_eh_convergence_hypothesis)
 149    (h3 : regge_ricci_convergence_axiom)
 150    (h4 : regge_riemann_convergence_axiom)
 151    (prov : List String) :
 152    (mk h1 h2 h3 h4 prov).provenance = prov := rfl
 153
 154/-! ## Round-trip: projection and construction are inverses -/
 155
 156/-- Building a registry from the projections of `r` recovers `r`.
 157This confirms the registry is a faithful repackaging. -/
 158theorem mk_roundtrip (r : ReggeConvergenceRegistry) :
 159    mk r.cms_measure_bound r.special_quadratic r.ricci_convergence
 160       r.riemann_convergence r.provenance = r := rfl
 161
 162/-! ## Default provenance -/
 163
 164/-- The default provenance list documenting each external-math result
 165with a status tag. -/
 166def defaultProvenance : List String :=
 167  [ "cms_measure_bound: Cheeger–Müller–Schrader (1984), Theorem 5.1 — curvature-measure convergence; status: external theorem, axiomatized"
 168  , "special_quadratic: stronger O(a²) action-convergence hypothesis; status: external hypothesis, axiomatized"
 169  , "ricci_convergence: Regge Ricci-scalar O(a²) convergence; status: external hypothesis, axiomatized"
 170  , "riemann_convergence: Regge holonomy / Riemann convergence; status: external hypothesis, axiomatized" ]
 171
 172end ReggeConvergenceRegistry
 173end Gravity
 174end IndisputableMonolith