IndisputableMonolith.Unification.TwoLimitsDischarged

   1import Mathlib
   2
   3-- NOTE: We intentionally do NOT import `IndisputableMonolith.Unification.TwoLimitsTheorem`
   4-- because that module currently has a pre-existing Mathlib API drift on line 46
   5-- (the `continuum_limit_second_order` interface uses an outdated bound shape).
   6-- The discharge below stands independently and can be wired into TwoLimitsTheorem
   7-- once that file is updated.
   8
   9/-!
  10# Conditional Discharge of `regge_to_eh_convergence`
  11
  12The fifth RS-internal gravity axiom in §XXIII.B' is the
  13Cheeger–Müller–Schrader convergence of the discrete Regge action to
  14the continuum Einstein–Hilbert action.  This is *classical*
  15mathematics (Cheeger–Müller 1984; Schrader 1990s) but requires
  16distributional curvature convergence machinery not in Mathlib.
  17
  18This module provides a **conditional theorem** form: given an
  19explicit Cheeger–Müller witness, the convergence statement
  20`|S_Regge − S_EH| ≤ C·a²` follows.  The witness is the
  21named hypothesis we would otherwise need to import from
  22distributional Riemannian-geometry literature.
  23
  24Status flag: PARTIAL CLOSURE / CONDITIONAL THEOREM.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Unification
  29namespace TwoLimitsDischarged
  30
  31noncomputable section
  32
  33/-- The Cheeger–Müller–Schrader witness: for any `S_EH` and any
  34    mesh size `a ∈ (0,1)`, there exists a Regge action value
  35    `S_Regge` and a constant `C > 0` controlling the
  36    `|S_Regge − S_EH| ≤ C·a²` error.  This bundles the
  37    distributional curvature convergence we would otherwise need
  38    from differential-geometry literature. -/
  39def CheegerMullerWitness : Prop :=
  40  ∀ (S_EH : ℝ) (a : ℝ), 0 < a → a < 1 →
  41    ∃ (S_Regge : ℝ) (C : ℝ), 0 < C ∧ |S_Regge - S_EH| ≤ C * a ^ 2
  42
  43/-- **CONDITIONAL THEOREM** (was `axiom regge_to_eh_convergence`):
  44    given a Cheeger–Müller witness, the Regge → EH convergence
  45    holds at every mesh size in `(0, 1)`. -/
  46theorem regge_to_eh_convergence_proof
  47    (h_witness : CheegerMullerWitness) :
  48    ∀ (S_EH : ℝ) (a : ℝ), 0 < a → a < 1 →
  49      ∃ (S_Regge : ℝ) (C : ℝ), 0 < C ∧ |S_Regge - S_EH| ≤ C * a ^ 2 :=
  50  h_witness
  51
  52/-- **TRIVIAL WITNESS**: the convergence holds vacuously by taking
  53    `S_Regge = S_EH` and `C = 1` (the difference is zero, hence
  54    ≤ `1 · a²` for any `a > 0`).  This shows the bound is satisfiable. -/
  55theorem cheeger_muller_witness_trivial : CheegerMullerWitness := by
  56  intro S_EH a ha _
  57  refine ⟨S_EH, 1, by norm_num, ?_⟩
  58  simp
  59  positivity
  60
  61/-- **DISCHARGED THEOREM**: the original `regge_to_eh_convergence`
  62    statement holds, with an explicit constructive witness. -/
  63theorem regge_to_eh_convergence_discharged :
  64    ∀ (S_EH : ℝ) (a : ℝ), 0 < a → a < 1 →
  65      ∃ (S_Regge : ℝ) (C : ℝ), 0 < C ∧ |S_Regge - S_EH| ≤ C * a ^ 2 :=
  66  cheeger_muller_witness_trivial
  67
  68/-! ## Note on the trivial witness
  69
  70The trivial witness `S_Regge = S_EH` proves the *existence* of a
  71Regge value satisfying the bound, but does not derive the Regge
  72action from a discrete triangulation independently of the EH value.
  73The physically interesting case (where `S_Regge` is computed from
  74a triangulation and `S_EH` is the continuum integral) requires the
  75full Cheeger–Müller machinery.
  76
  77So the discharge is **structural**: the existence statement is
  78provable, but the substantive content (that real Regge actions
  79converge to EH) needs a separate physical-discharge proof.
  80
  81The original `axiom` in `TwoLimitsTheorem.lean` carries the same
  82existence statement and so is no stronger than the trivial witness
  83for the proof obligation as currently written.  A future Lean port
  84of Cheeger–Müller would replace `cheeger_muller_witness_trivial`
  85with an actual discrete-construction-based proof.
  86-/
  87
  88end
  89
  90end TwoLimitsDischarged
  91end Unification
  92end IndisputableMonolith
  93