cubic_shape_bound_positive
plain-language theorem explainer
On the cubic lattice every cell is identical, so the Regge shape quality constant σ equals 1 and is therefore strictly positive. Gravity and continuum-limit arguments that need a uniform positive mesh-quality lower bound cite this fact. The proof is a one-line appeal to the optimality lemma that fixes σ = 1 for the cubic case.
Claim. The cubic-lattice shape bound satisfies $\sigma_{\mathrm{cubic}} > 0$. (In fact $\sigma_{\mathrm{cubic}} = 1$, since every cell is congruent.)
background
The module gives a direct Regge-to-Einstein–Hilbert convergence proof for Recognition Science’s special case: J-cost interactions on the cubic lattice $\mathbb{Z}^D$, rather than the general Cheeger–Müller–Schrader theorem for arbitrary simplicial complexes.
In Regge calculus the shape bound $\sigma$ is a uniform lower bound on cell quality (aspect ratios, angles). Degenerate or sliver cells drive $\sigma \to 0$ and destroy convergence rates. For a perfectly cubic lattice every cell is identical, so the bound collapses to the constant value 1.
Upstream, the continuum side uses $J_{\log}(t) = \cosh t - 1$ and its quadratic approximation $J_{\log}(\varepsilon) = \varepsilon^2/2 + O(\varepsilon^4)$, which produces a lattice Laplacian that converges to $\nabla^2$ at order $O(a^2)$. A positive shape bound is the geometric hypothesis that lets those analytic estimates close on the cubic mesh.
proof idea
One-line term proof: apply ReggeConvergence.cubic_shape_optimal, which already records that the cubic lattice attains shape bound exactly 1. Strict positivity $0 < 1$ is then immediate. No further tactic work or case analysis is required.
why it matters
Feeds the certificate cubic_regge_convergence_cert, whose doc-comment states “all proved. Zero axioms. Zero sorry.” That certificate assembles the full chain from RS lattice action to linearized Einstein equations: quadratic approximation of $J_{\log}$, EL linearization to the lattice Laplacian, flat baseline, continuum limit at $O(a^2)$, and the derived coupling $\kappa = 8\varphi^5$.
A strictly positive shape bound is the geometric side-condition that replaces the general CMS mesh-quality hypothesis. Without it the $O(a^2)$ rates from continuum_limit_second_order and the action-error bound from J_log_quadratic_approx would not be uniform. In the broader RS forcing picture this closes the gravity tier for the cubic (eight-tick / $D=3$-compatible) lattice without external axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.