rs_cubic_shape_quality
plain-language theorem explainer
On the Recognition Science cubic lattice every cell is identical, so the CMS shape-quality factor equals 1. Anyone citing the RS cubic Regge convergence certificate needs this identity to drop the shape multiplier from the error bound. The proof is definitional reflexivity: the cubic shape bound is defined to be 1.
Claim. The cubic-lattice shape-quality bound equals $1$: every cube has optimal aspect ratio, so the CMS shape factor $\sigma$ is identically one.
background
The module treats Regge convergence on the RS cubic lattice $\mathbb{Z}^3$ without invoking the full Cheeger–Müller–Schrader (CMS) regularity package. CMS error estimates carry a shape factor $\sigma$ that measures aspect-ratio distortion of simplices; on a perfectly cubic mesh every cell is congruent, so $\sigma=1$ and the factor drops out of the bound.
Upstream, cubic_shape_bound is defined as the real constant $1$, with the comment that a cubic lattice has optimal aspect ratio. The dimensionless bridge ratio $K=\varphi^{1/2}$ multiplies the mesh-size power in the general CMS-style estimate $|S_{\mathrm{RS}}-S_{\mathrm{EH}}|\le K,a^2\sigma$; with $\sigma=1$ one recovers the cleaner RS form $|S_{\mathrm{RS}}-S_{\mathrm{EH}}|\le K,a^2$.
Local strategy (module doc): perfect shape quality, the eight-tick UV cutoff, $J$-cost convexity, and the $\varphi$-exponential growth bound together replace CMS hypotheses for weak-field $O(a^2)$ convergence.
proof idea
One-line term proof by reflexivity. The cubic shape bound is defined as the real number $1$, so the equality is definitional and rfl closes it. No lemmas are applied.
why it matters
Feeds the certificate cubic_convergence_cert, which packages four RS-specific facts: unit shape quality, a positive UV cutoff, $\varphi$-exponential growth, and the weak-field error estimate. That certificate is the module's claim that cubic Regge convergence holds without full CMS regularity.
In the framework this is the first of the four structural reasons the RS lattice is special: identical cubes give $\sigma=1$, so the general CMS aspect-ratio condition is automatic. Combined with the eight-tick octave (T7) fixing the mesh scale and $J$-convexity controlling nonlinear remainders, it underwrites unconditional $O(a^2)$ convergence in the weak-field regime. The identity is tiny but load-bearing: without it the shape factor would remain in every downstream error estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.