IndisputableMonolith.Unification.TwoLimitsDischarged
The Unification.TwoLimitsDischarged module supplies the Cheeger-Müller-Schrader witness that bounds the difference between any Regge action and the Einstein-Hilbert action by a term linear in the square of the mesh size. Discrete-gravity researchers cite it to control the continuum limit without separate appeals to distributional geometry. The module packages the required convergence statement into one self-contained object.
claimFor any Einstein-Hilbert action $S_{EH}$ and mesh size $a ∈ (0,1)$, there exists a Regge action $S_{Regge}$ and constant $C > 0$ such that $|S_{Regge} - S_{EH}| ≤ C a^2$.
background
The module belongs to the Unification domain and imports only Mathlib. It introduces the Cheeger-Müller-Schrader witness as a single statement that encodes distributional curvature convergence between Regge calculus on a mesh and the continuum Einstein-Hilbert action. The witness replaces external differential-geometry results with an explicit quadratic error bound controlled by mesh size.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module discharges the two limits required for Regge-to-Einstein-Hilbert convergence inside the Recognition Science unification. It supplies the witness quoted in its documentation and thereby supports sibling results such as regge_to_eh_convergence_discharged.
scope and limits
- Does not construct explicit Regge triangulations for given $S_{EH}$.
- Does not evaluate or bound the constant $C$.
- Does not extend the error estimate beyond order $a^2$.
- Does not treat the degenerate cases $a=0$ or $a otin (0,1)$.