CheegerMullerWitness
plain-language theorem explainer
The Cheeger-Muller witness encodes the existence of a Regge action value and positive constant C such that the absolute difference from any given Einstein-Hilbert action is at most C times the square of the mesh size a, for every a in (0,1). Lattice gravity and discrete-to-continuum unification researchers cite this to justify the Regge-to-Einstein-Hilbert limit without importing full distributional geometry machinery. The declaration is a direct Prop definition that serves as the hypothesis for the conditional convergence statement.
Claim. For any real number $S_{EH}$ and any mesh size $a$ satisfying $0 < a < 1$, there exist a real number $S_{Regge}$ and a positive real number $C$ such that $|S_{Regge} - S_{EH}| ≤ C a^2$.
background
This definition sits in the module discharging the Regge-to-Einstein-Hilbert convergence conditionally. The local theoretical setting is the fifth RS-internal gravity axiom in §XXIII.B', which concerns classical Cheeger-Müller-Schrader convergence of the discrete Regge action to the continuum Einstein-Hilbert action; the module supplies an explicit witness because the required distributional curvature convergence is absent from Mathlib. The witness bundles the needed error control as a named hypothesis rather than an imported theorem.
proof idea
This is a definition that directly encodes the required existence statement for the Regge action and quadratic error bound. No lemmas are applied and no tactics are invoked; the body is the bare universal quantifier and existential claim.
why it matters
The declaration supplies the hypothesis for the conditional theorem regge_to_eh_convergence_proof, which replaces the former axiom regge_to_eh_convergence. It thereby closes the fifth RS-internal gravity axiom in §XXIII.B' and enables the unification step that equates discrete Regge calculus with continuum general relativity at quadratic order in mesh size. The sibling trivial witness shows the bound is satisfiable by the zero-difference choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.