theorem
proved
term proof
regge_to_eh_convergence_discharged
show as:
view Lean formalization →
formal statement (Lean)
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 :=
proof body
Term-mode proof.
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