cubic_shape_optimal
plain-language theorem explainer
On the RS cubic lattice the shape bound equals 1 and is therefore strictly positive. Gravity and continuum-limit arguments that assemble CMS-style conditions cite this positivity. The proof unfolds the constant definition and discharges 0 < 1 by numerical normalization.
Claim. The cubic-lattice shape bound satisfies $0 < \sigma_{\mathrm{cubic}}$, where by definition $\sigma_{\mathrm{cubic}} = 1$ (every cell has identical shape and optimal aspect ratio).
background
The module proves that the Regge action on the Recognition Science lattice converges to the Einstein-Hilbert action in the continuum limit. Convergence is split into an unconditional linearized (weak-field) regime and a conditional nonlinear regime that packages Cheeger-Muller-Schrader (CMS) hypotheses.
Among those hypotheses is a shape bound $\sigma$ controlling cell aspect ratios. For a general triangulation $\sigma$ can be large; for the RS cubic lattice $\mathbb{Z}^3$ every cell is congruent, so the bound collapses to the constant 1. The sibling definition records exactly that: cubic_shape_bound := 1.
Upstream cost machinery (J-cost on ratios, recognition-event cost, rung-coarsen sums) identifies the RS Regge action with a sum of J-costs; the shape bound itself is purely geometric and does not depend on those cost functionals.
proof idea
One-line tactic proof. Unfold the definition of the cubic shape bound to the literal real constant 1, then apply norm_num to obtain the elementary inequality $0 < 1$. No lemmas beyond definitional unfolding are required.
why it matters
Positivity of the cubic shape bound is a required field of the CMS-conditions bundle used by the RS-specific quadratic convergence statement: on $\mathbb{Z}^3$ with bounded curvature the J-cost Regge action is taken to converge to the Einstein-Hilbert action at $O(a^2)$, stronger than the general CMS measure bound. The certificate regge_convergence_cert records this fact as cubic_optimal, and the CubicReggeProof chain re-exports it as cubic_shape_bound_positive when assembling the full derivation from the RS lattice to the linearized Einstein field equations. In the forcing picture this sits under continuum recovery of gravity (lattice $\to$ EH), complementary to T8 ($D=3$) which already forces three spatial dimensions for the cubic lattice itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.