regge_to_eh_convergence_discharged
plain-language theorem explainer
The discharged theorem states that for any real Einstein-Hilbert action value S_EH and mesh parameter a in (0,1), there exist a Regge action S_Regge and positive constant C such that the absolute difference is bounded by C a squared. Researchers closing discrete gravity limits in Recognition Science would cite this as the existence half of the fifth gravity axiom. The proof is a one-line application of the trivial witness that sets S_Regge equal to S_EH.
Claim. 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}|$ is at most $C a^2$.
background
Recognition Science lists the Cheeger-Müller-Schrader convergence of discrete Regge action to continuum Einstein-Hilbert action as the fifth internal gravity axiom. The module supplies a conditional theorem form: the bound holds once an explicit witness is supplied. The local setting uses real-valued actions and a scale parameter a that controls mesh refinement in the discrete-to-continuum transition.
proof idea
The proof is a one-line wrapper that applies the trivial Cheeger-Müller witness. This witness equates S_Regge to S_EH, which satisfies the inequality for any positive C. The accompanying note records that the construction is structural only and does not yet derive S_Regge from an independent triangulation.
why it matters
The declaration discharges the existence obligation of the original regge_to_eh_convergence axiom in TwoLimitsTheorem.lean, replacing an axiom with a proved statement. It sits inside the Recognition Science gravity chain that begins from the phi-forcing structures and integration-gap identities. The open question it touches is the full Lean formalization of distributional curvature convergence needed for the physically substantive case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.