Pith. sign in
module module moderate

IndisputableMonolith.Geometry.ReggeActionNonlinearCorrespondence

show as:
view Lean formalization →

Local bridge from nonlinear Regge action to Recognition J-cost in log coordinates. Discrete-gravity and forcing-chain workers cite it when swapping a Regge remainder for a canonical J-quadratic plus controlled higher terms. Builds weighted J-actions, evenness along lines, Dirichlet identification of the quadratic piece, an exact canonical split, and the strongest true local replacement theorem.

claimWrite the J-cost in log coordinates as $J_{\log}(t)=\cosh(t)-1$. Form the weighted J-cost action on vertex potentials; it is even along lines. Its canonical quadratic term equals a Dirichlet energy and is nonnegative. The nonlinear Regge action splits exactly into that quadratic piece plus a remainder. Under the local geometric hypotheses, the strongest true replacement identifies the Regge action with the J-cost action up to the cubic Taylor control.

background

Recognition Science pins the cost functional by the Recognition Composition Law; T5 uniqueness forces $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. This module works that cost in additive log coordinates, so the natural local variable is a real potential increment rather than a multiplicative edge factor.

On the geometry side, discrete gravity is carried by a nonlinear Regge action on a finite-dimensional space of vertex potentials. The imported cubic Taylor module isolates the third-order remainder bound once the nonlinear Hessian is known. Functional-equation helpers from the T5 cost package supply the algebraic identities for $J$ under inversion and scaling.

The local objects are therefore: log-coordinate J-cost, a weighted action built from it, the canonical quadratic (Dirichlet) term extracted from that action, and the exact split of the nonlinear Regge action into quadratic plus remainder.

proof idea

Definition layer first: log-coordinate J-cost, its identity with $\cosh-1$, and oddness/evenness under sign flip. Weighted J-cost action is assembled next; negation and restriction to lines yield evenness of the action along lines.

The canonical quadratic term is defined and matched to a Dirichlet energy form, with nonnegativity following from that identification. The exact canonical split decomposes the nonlinear Regge action into this quadratic piece plus remainder.

Higher theorems package the local correspondence and the strongest true replacement: they combine the split with the imported cubic Taylor bound so the remainder is controlled in the finite-dimensional potential space. Structure is definitional setup plus algebraic identities, then analytic remainder control from the upstream Taylor module.

why it matters in Recognition Science

Feeds the unified forcing chain (T0–T8 from the cost foundation), where geometric discreteness and the eight-tick / $D=3$ steps need a clean Regge-to-J link rather than an ad hoc lattice action. Also imported by the Regge remainder closure audit (Track 1B-REM analytic branch) as the certificate that the nonlinear remainder is the J-cost remainder under local correspondence.

On the gravity side it supplies obligations for the physical six-tet cubic Dirichlet instance: packaging exact theorem hooks so a periodic Freudenthal torus can instantiate the physical Dirichlet model without asserting equality for free. Landmark contact is T5 J-uniqueness ($J=\cosh\circ\log-1$) and the passage from that cost to a Dirichlet quadratic suitable for discrete curvature. Closes the analytic half of the Regge–J replacement used downstream in forcing and gravity scaffolds.

scope and limits

used by (3)

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 (19)