regge_to_eh_convergence_proof
plain-language theorem explainer
Given the Cheeger-Müller witness, the Regge action converges to the Einstein-Hilbert action with quadratic error bound C a² for every mesh size a in (0,1). Discrete gravity researchers would cite this to justify taking continuum limits inside Regge calculus. The proof is a one-line term application of the witness hypothesis.
Claim. Assuming the Cheeger–Müller witness, for all real numbers $S_{EH}$ and $a$ satisfying $0 < a < 1$, there exist real numbers $S_{Regge}$ and $C > 0$ such that $|S_{Regge} - S_{EH}| ≤ C a^2$.
background
The CheegerMullerWitness is the proposition that for any Einstein-Hilbert value $S_{EH}$ and mesh size $a ∈ (0,1)$, there exists a Regge action value $S_{Regge}$ and constant $C > 0$ satisfying the quadratic error bound. This module supplies the conditional theorem form of the fifth RS-internal gravity axiom, the Cheeger–Müller–Schrader convergence of discrete Regge action to continuum Einstein–Hilbert action. The setting is labeled PARTIAL CLOSURE because the required distributional curvature convergence lies outside Mathlib.
proof idea
The proof is a term-mode one-liner consisting of direct application of the hypothesis h_witness.
why it matters
This declaration discharges the conditional form of the fifth RS-internal gravity axiom in §XXIII.B' of the Recognition Science framework. It lets the unification proceed under the explicit Cheeger–Müller witness without importing external distributional geometry results. No downstream uses are recorded, indicating the declaration closes the conditional statement for later unification steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.