cubic_shape_bound
plain-language theorem explainer
On the RS cubic lattice the geometric shape factor is exactly 1: every cell is a unit cube of identical aspect ratio. Gravity and continuum-limit arguments cite this constant whenever they need the optimal shape bound that multiplies the O(a²) Regge-to-Einstein error. The declaration is a one-line real constant, not a derived inequality.
Claim. The shape bound for the Recognition Science cubic lattice is the real number $\sigma = 1$, corresponding to identical cubes of optimal aspect ratio.
background
The module proves that the Regge action on the RS lattice converges to the Einstein-Hilbert action in the continuum limit. Convergence is split into an unconditional linearized (weak-field) regime and a conditional full nonlinear regime under Cheeger-Muller-Schrader-type hypotheses.
In classical Regge calculus the shape bound $\sigma$ controls how badly tetrahedra or cubes can degenerate; it multiplies the leading $O(a^2)$ error between the discrete action and the continuum Einstein-Hilbert action. For a general triangulation $\sigma$ can be large. The RS lattice is the integer cubic lattice $\mathbb{Z}^3$, so every cell is congruent and the aspect ratio is optimal.
The constant is therefore fixed at 1 rather than left as a free geometric parameter. Downstream certificates record this fact as shape_quality_free or as the positivity statement $0 < \sigma$.
proof idea
Pure definitional assignment: the real constant is set equal to 1. No lemmas, tactics, or algebraic reduction are involved. Sibling positivity (cubic_shape_optimal) is the one-line unfold-and-norm_num check that $0 < 1$.
why it matters
This constant is the RS-specific geometric advantage of the cubic lattice. CubicConvergenceCert records it as shape_quality_free : cubic_shape_bound = 1, one of three structural advantages of the RS lattice. rs_cubic_shape_quality is the trivial reflexivity proof of the same equality, and notes that $\sigma = 1$ drops out of the error bound $|S_{\mathrm{RS}} - S_{\mathrm{EH}}| \le K \cdot a^2$.
ReggeConvergenceCert and CubicReggeConvergenceCert both require positivity of the bound as a certificate field, feeding the claim that linearized Regge convergence covers solar-system, galactic, CMB, and gravitational-wave regimes. In the forcing chain this sits under the continuum-limit side of Axiom 1 (lattice to Einstein), not under T5-T8; it is the geometric input that lets the eight-tick cubic structure carry an optimal shape factor into gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.