module module moderate

`IndisputableMonolith.Gravity.CubicReggeProof`

Cubic-lattice bridge from discrete J-cost dynamics to continuum Einstein–Hilbert geometry. Gravity workers in the RS programme cite it for the linearized Euler–Lagrange identification with the lattice Laplacian and for controlled Regge-action convergence rates. The argument chains 3D continuum-limit lemmas with bond-wise action estimates and the identity that the derivative of cosh(ε)−1 is sinh(ε).

claimOn the cubic lattice $\mathbb{Z}^3$, the linearized Euler–Lagrange equation of the bond-wise $J$-cost action is equivalent to vanishing of the discrete Laplacian. Flat configurations satisfy the EL equations exactly. The total Regge action converges to the continuum Einstein–Hilbert action, with relative error tending to zero at a controlled rate as the lattice spacing shrinks.

background

Recognition Science gravity is built on the cost $J(x)=\frac12(x+x^{-1})-1$, uniquely minimized at $x=1$. In log coordinates this is $J(e^t)=\cosh(t)-1$, a convex bowl. DiscretenessForcing records that this landscape forces discrete structure; ContinuumLimit shows that long-wavelength discrete $J$-dynamics on $\mathbb{Z}^3$ yield a second-order diffusion equation of Klein–Gordon type.

LatticeConvergence extends the 1D second-order continuum limit to $D=3$ by writing the cubic Laplacian as a sum of three independent 1D Laplacians. ReggeCalculus supplies the exact nonlinear Regge framework on the RS lattice (edge lengths and deficit angles), replacing linearized deficit ansätze. NonlinearConvergence and ReggeConvergence record the inputs needed to pass from Regge action to Einstein–Hilbert geometry.

This module sits between those foundations and the packaged lattice–manifold correspondence. It introduces the bond-wise action, the Euler–Lagrange operator for that action, its linearization about flat space, and the continuum limit of the cubic Laplacian.

proof idea

The module is a chain of short analytic lemmas, not a single monolithic proof.

First, the elementary identity $d/d\varepsilon(\cosh\varepsilon-1)=\sinh\varepsilon$ (and $\sinh'(0)=1$) converts log-coordinate cost derivatives into hyperbolic functions. The Euler–Lagrange operator of the bond action is then written explicitly; flat configurations are checked to satisfy it.

Linearization about the flat point identifies the EL operator with the negative discrete Laplacian (equivalently, linearized EL vanishes iff the Laplacian vanishes). Separately, the action per bond is defined and summed; total-action convergence and a relative-error rate are proved so that the relative error tends to zero in the continuum limit. The cubic Laplacian continuum limit is imported from the lattice-convergence layer and tied to the linearized EL picture.

why it matters in Recognition Science

Without a cubic-lattice EL–Laplacian dictionary and controlled action convergence, the deformed-cubic-lattice story cannot be closed. Downstream, UnifiedLatticeManifoldCorrespondence packages the full claim: given a smooth Lorentzian $(M,g)$, there is a sequence of deformed cubic lattices whose Regge action converges to $S_{\mathrm{EH}}[g]$ and whose Regge equations converge to the Einstein field equations.

This module supplies the cubic, linearized, and rate ingredients that package needs. It sits on the gravity side of the forcing chain after $D=3$ (T8) and the eight-tick discrete structure, and it uses the $J$-cost uniqueness (T5) only through the hyperbolic log form already fixed upstream. It does not itself claim the full nonlinear curved-manifold correspondence; that is the parent module's job.

scope and limits

Does not prove the full nonlinear Regge-to-Einstein–Hilbert theorem for arbitrary curved manifolds.
Does not derive $D=3$ or the eight-tick structure; those are upstream forcing results.
Does not treat non-cubic lattices or irregular triangulations.
Does not establish quantum gravity or graviton spectra; classical continuum limit only.
Does not fix Newton's constant or post-Newtonian parameters beyond what ZeroParameterGravity already supplies.

used by (1)

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

IndisputableMonolith.Gravity.UnifiedLatticeManifoldCorrespondence module_import

depends on (8)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.ContinuumLimit module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Gravity.LatticeConvergence module_import
IndisputableMonolith.Gravity.NonlinearConvergence module_import
IndisputableMonolith.Gravity.ReggeCalculus module_import
IndisputableMonolith.Gravity.ReggeConvergence module_import
IndisputableMonolith.Gravity.ZeroParameterGravity module_import

declarations in this module (26)

theorem deriv_J_log_eq_sinh L58
def euler_lagrange L68
theorem flat_satisfies_el L76
theorem sinh_deriv_at_zero L82
theorem linearized_el_plus_laplacian_zero L94
theorem linearized_el_eq_neg_laplacian L106
theorem linearized_el_zero_iff_laplacian_zero L116
theorem action_per_bond L129
theorem total_action_convergence L140
theorem relative_convergence_rate L156
theorem relative_error_tendsto_zero L163
theorem laplacian_continuum_limit L174
theorem laplacian_3D_decomposition L184
theorem quartic_coeff L204
theorem sextic_coeff L207
theorem taylor_coefficients_positive L211
theorem expansion_convergence_ratio L216
theorem kappa_derived L230
theorem kappa_positive L233
theorem newtonian_positive_source L238
theorem cubic_flat_deficit L246
theorem cubic_shape_bound_positive L250
structure ProvedConvergenceChain L268
theorem proved_convergence_chain L294
structure CubicReggeConvergenceCert L323
theorem cubic_regge_convergence_cert L360