Pith. sign in
module module moderate

IndisputableMonolith.Geometry.ReggeActionNonlinearCorrespondence

show as:
view Lean formalization →

Module that identifies the nonlinear Regge action with the Recognition J-cost in logarithmic edge coordinates. It supplies the exact canonical split into a Dirichlet quadratic term plus controlled remainder, and the local correspondence statements gravity and forcing-chain code import. The development rests on T5 cost identities and the cubic Taylor bound for the nonlinear remainder.

claimIn log edge coordinates $u=\log x$, set $J(e^u)=\cosh u-1$. The weighted J-cost action is even along lines; its canonical quadratic term equals the Dirichlet form and is nonnegative. The nonlinear Regge action splits exactly into that quadratic piece plus a remainder controlled by a cubic Taylor bound, giving a local Regge–J-cost correspondence and a strongest true replacement statement.

background

Recognition Science fixes the unique admissible cost by the Recognition Composition Law (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Discrete gravity on triangulations is written as a nonlinear Regge action on edge lengths. To match the two, one passes to logarithmic edge coordinates so the cost becomes an even function of a real potential and its Hessian is transparent.

The module sits between the functional-equation helpers for T5 and the cubic Taylor bound for the nonlinear Regge remainder. The former supplies the algebraic identities for $J$ in log coordinates; the latter isolates the third-order analytic estimate in finite-dimensional vertex-potential space once the nonlinear Hessian is known.

Objects introduced here include the log-coordinate cost, the weighted J-cost action and its evenness along lines, the canonical quadratic term (identified with a Dirichlet form and shown nonnegative), the exact canonical split of the nonlinear Regge action, and the local correspondence / strongest-true-replacement packages built from that split.

proof idea

Not a single theorem: a short development chain. First, define $J$ in log coordinates and record $J(e^u)=\cosh u-1$ together with oddness/negation identities from the T5 functional equation. Lift to a weighted action on edge potentials; evenness along lines follows from the evenness of $\cosh u-1$. Extract the canonical quadratic term, prove it equals the Dirichlet form, and obtain nonnegativity. Form the exact split of the nonlinear Regge action into that quadratic piece plus remainder. Close with the local correspondence and strongest-true-replacement statements by feeding the remainder into the imported cubic Taylor bound.

why it matters in Recognition Science

This is the analytic bridge that lets discrete gravity speak the same cost language as the forcing chain. UnifiedForcingChain imports it while proving T0–T8 as inevitabilities from the cost foundation, so the Regge side stays aligned with T5 J-uniqueness rather than an ad hoc quadratic action. ReggeRemainderClosureAudit uses it as the analytic-remainder branch certificate for Track 1B-REM, separate from finite-Freudenthal combinatorics. PhysicalSixTetCubicDirichletInstance packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; the canonical quadratic identification and local correspondence are the geometric inputs that instance depends on. Without the exact split and the Dirichlet match, the nonlinear Regge remainder cannot be closed against the RS cost.

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)