RSCubicConvergenceConditions
plain-language theorem explainer
Packages the two remaining CMS-style hypotheses needed for Regge convergence on the RS cubic lattice: a curvature bound K and the mesh threshold a₀ = 1/K. Shape quality is omitted because cubes force σ = 1. Downstream error bounds cite this bundle; the structure is pure data with a positivity proof for the threshold.
Claim. A record of RS cubic convergence data consists of a real curvature scale $K > 0$ and the associated mesh threshold $a_0(K) := 1/K$, which is automatically positive.
background
The module treats Regge calculus on the RS cubic lattice $\mathbb{Z}^3$, where the usual Cheeger–Müller–Schrader (CMS) regularity package is partly free. CMS asks for (C1) a curvature bound $|\mathrm{Riem}| < K$, (C2) a shape-quality lower bound $\sigma$ on aspect ratios, and (C3) a mesh-size threshold $a < a_0(K)$. On identical cubes, $\sigma = 1$ holds identically, so only (C1) and (C3) remain as hypotheses.
The module strategy is direct lattice convergence rather than invoking the full CMS theorem: the $J$-cost Laplacian on $\mathbb{Z}^3$ is a standard lattice action; Lax equivalence gives second-order convergence; quartic $J$-error is controlled by $|J(e^\varepsilon)-\varepsilon^2/2| \le |\varepsilon|^4/24$ in the weak-field regime. An 8-tick UV cutoff and the $\varphi$-exponential growth bound $\varphi^N > C\cdot N^3$ further limit concentration.
The curvature scale here is an abstract positive real (not the dimensionless bridge constant $K=\varphi^{1/2}$ from Constants), serving as the CMS-style bound on Riemann curvature for the continuum limit comparison.
proof idea
Definitional structure, not a theorem. Fields are a real $K_{\mathrm{curvature}}$, the inequality $0 < K_{\mathrm{curvature}}$, and a default mesh threshold $1/K_{\mathrm{curvature}}$. The only proof obligation is positivity of the threshold, discharged by the positivity tactic from $K > 0$. No upstream lemmas are applied beyond that arithmetic.
why it matters
This is the RS-specific thinning of CMS: by dropping shape quality, the cubic lattice needs only bounded curvature and $a < 1/K$. The sole consumer rs_convergence_bound turns the package into the error estimate $|S_{\mathrm{RS}} - S_{\mathrm{EH}}| \le K \cdot a^2$, noting that the shape factor $\sigma = 1$ drops out of the general CMS bound.
In the broader Recognition gravity story this supports unconditional $O(a^2)$ weak-field convergence and conditional strong-field convergence on the cubic lattice, using the eight-tick UV cutoff and $J$-convexity rather than a generic triangulated CMS theorem. It sits in the Gravity domain as the hypothesis interface for cubic Regge continuum limits tied to the RS voxel geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.