Pith. sign in
module module moderate

IndisputableMonolith.Gravity.ReggeCubicLatticeLimit

show as:
view Lean formalization →

Regular cubic-lattice comparison model for the canonical second-order Regge action on the RS lattice Z³. It packages limit inputs, comparison models, and vanishing-error statements that match discrete second-order Regge data to continuum second variation under perfect cube shape quality. Gravity workers cite it when specializing cubic Regge convergence to second-order action asymptotics. The argument wires named lattice-limit inputs to finite-difference and exact second-order comparison theorems.

claimOn the regular cubic lattice $\mathbb{Z}^3$ with spacing $h$, the module supplies comparison models and limit inputs so that the canonical second-order Regge action $S^{(2)}_h$ converges to the continuum second variation of the nonlinear Regge action, with cubic remainder controlled and error vanishing along refining lattice models (perfect shape quality $\sigma=1$).

background

Regge calculus discretizes gravity on a simplicial complex by assigning edge lengths and a deficit-angle action. The upstream second-variation module states nonlinear second-variation and cubic-remainder targets in usable form; the full Cayley-Menger/arccos expansion is not yet fully expanded, so analytic facts live in named input structures.

On the RS cubic lattice $\mathbb{Z}^3$, cubic Regge convergence does not need the full Cheeger-Müller-Schrader regularity package: every cube is identical, so shape quality is perfect ($\sigma=1$) and the CMS aspect-ratio condition holds automatically. This module sits between that lattice convergence story and the second-order action asymptotics.

Local objects include regular cubic lattice models, Regge second-order cubic lattice limit data, physical six-tet cubic Dirichlet models, and exact second-order comparison models that feed finite-difference second-order estimates.

proof idea

Definition-and-limit module, not a single theorem. It introduces lattice models and limit-input structures (regular cubic lattice model, Regge cubic lattice limit input, exact second-order comparison model), then maps physical six-tet cubic Dirichlet data into those inputs. Limit theorems assert that the second-order Regge action on the cubic lattice converges with error vanishing along refining models, using finite-difference second-order estimates and the upstream second-variation/cubic-remainder interface together with cubic Regge convergence on $\mathbb{Z}^3$.

why it matters in Recognition Science

Supplies the cubic-lattice second-order comparison layer that the physical six-tet cubic Dirichlet instance imports. That downstream module connects the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model and packages the exact theorem obligations needed to instantiate the physical model; it does not assert Dirichlet equality for free. In the gravity domain this is the bridge from RS-specific cubic Regge convergence (no full CMS) and the second-variation remainder interface to concrete physical lattice instances used in continuum-limit arguments.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)