CMSConditions
plain-language theorem explainer
Packages the three special quadratic hypotheses under which this module assumes O(a²) Regge-to-Einstein-Hilbert action convergence: a curvature bound K, a shape (aspect-ratio) bound σ, and a mesh threshold a₀(K,σ), each strictly positive. Gravity and continuum-limit authors cite it when stating the conditional nonlinear envelope, not the general CMS measure bound. It is a plain structure of three reals with positivity witnesses; no proof content.
Claim. A record of special quadratic mesh hypotheses consisting of three positive reals $K$, $\sigma$, and $a_0$: the smooth metric has $\|\mathrm{Riem}\|_\infty < K$; the triangulation is well-shaped with aspect ratios bounded by $\sigma$; and the mesh size satisfies $a < a_0(K,\sigma)$. These are stronger than the general Cheeger–Müller–Schrader curvature-measure hypotheses.
background
The module proves that the Regge action on the Recognition Science lattice converges to the Einstein–Hilbert action in the continuum limit, in two regimes. The linearized (weak-field) regime is unconditional. The full nonlinear regime is conditional: the classical Cheeger–Müller–Schrader theorem supplies a curvature-measure estimate of the form $|R_i(U)-R_{i,\eta}(U)| \le c,(\mathrm{Vol}(U)\sqrt{\eta}+\mathrm{Vol}(B_{\sqrt{\eta}}(\partial U)))$, not a plain $O(a^2)$ action bound.
This structure therefore records only the stronger special conditions under which the module asks for an $O(a^2)$ action-convergence envelope: bounded Riemann curvature by $K$, aspect ratios bounded by $\sigma$, and mesh size below a threshold $a_0(K,\sigma)$. The general CMS shape lives separately as the scalar abstraction cms_theorem_5_1_measure_bound in NonlinearConvergence. The historical name is kept for compatibility; these are not the general CMS Theorem 5.1 hypotheses.
proof idea
No proof: this is a structure definition. It bundles three real parameters (K_curvature_bound, sigma_shape_bound, a0_mesh_threshold) together with three positivity fields (K_pos, sigma_pos, a0_pos). Downstream definitions unpack the fields when stating the conditional $O(a^2)$ envelope.
why it matters
This package is the hypothesis carrier for the module’s conditional nonlinear statements. nonlinear_convergence_with_conditions takes a value of this structure and asserts that for every mesh $a$ with $0 < a < a_0$, the Regge and Einstein–Hilbert actions differ by at most $K,\sigma,a^2$. The RS-specific wrapper rs_regge_convergence instantiates it on the cubic lattice with shape bound 1.
In the broader gravity stack it feeds the nonlinear certificate path (NonlinearReggeCert and related lattice-regularity checks). The module’s key claim is that linearized convergence already covers solar-system, galactic, and cosmological-perturbation regimes; the nonlinear envelope (and thus this structure) is needed only for black-hole interiors and strong-field regimes. It deliberately does not stand in for CMS Theorem 5.1; that measure bound is recorded separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.