T5_To_NonlinearReggeJCost_Bridge
plain-language theorem explainer
Certificate packaging the T5 uniqueness of the recognition cost J into the nonlinear Regge curvature-action surface on 3D triangulations. Anyone citing the discrete-to-continuum gravity route from forced J will use this interface. It is a Prop-valued structure of eight equalities and implications (log-cosh form, weighted edge action, Dirichlet quadratic, exact split, cubic Taylor local correspondence, six-tet stencil), not a proved theorem by itself.
Claim. Given T5 (uniqueness of $J(x)=\frac12(x+x^{-1})-1$ on $(0,\infty)$ from reciprocity, normalization, the Recognition Composition Law, calibration, and continuity), the bridge asserts: (i) any reciprocal, normalized, composition-law, calibrated continuous cost equals $J$; (ii) in log coordinates $J(e^t)=\cosh t-1$; (iii) the weighted nonlinear edge action equals $\sum_{i,j} w_{ij}\,J(e^{\xi_i-\xi_j})$; (iv) the canonical $J$-quadratic term is half the canonical Regge Dirichlet energy; (v) the full Regge action splits exactly into flat value + $J$-quadratic + remainder; (vi) cubic Taylor control yields local Regge/$J$ correspondence; (vii)--(viii) the canonical periodic Freudenthal torus carries the physical six-tet cubic Dirichlet model.
background
The Unified Forcing Chain module treats T0--T8 as forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). T5 is the uniqueness step: those axioms pin $J(x)=\frac12(x+x^{-1})-1$ on $(0,\infty)$, equivalently $\cosh(\log x)-1$.
This bridge sits after T5 and before continuum completion. It connects that unique cost to discrete gravity: Regge action on incidence-consistent 3D triangulations, vertex potentials $\xi$, dual edge weights, and the nonlinear correspondence package that rewrites edge contributions as $J$-costs of exponential length ratios. The log-coordinate identity $J(e^t)=\cosh t-1$ is the analytic hinge between recognition cost and the quadratic/Dirichlet sector of Regge calculus.
Upstream, $J$ appears throughout the cost and cosmology layers as the recognition cost of a positive ratio. The Aczel smoothness package is the hypothesis surface that makes uniqueness available to callers. Downstream continuum work needs this discrete action surface already identified with $J$.
proof idea
This declaration is a Prop-structure (certificate interface), not a proved theorem. It has no tactic proof body; the fields are named obligations.
The companion theorem t5_to_nonlinear_regge_jcost_bridge_holds inhabits the structure from a T5 instance: uniqueness is discharged by the Aczel-packaged law-of-logic forces-$J$ surface; log-cosh, weighted action formula, Dirichlet identification, exact algebraic split, Taylor-to-local-correspondence implication, and the six-tet Freudenthal routes are filled from the geometry/Regge correspondence lemmas already in the monolith.
Treat the structure as the typed checklist those lemmas must satisfy before the continuum bridge can depend on a single hRegge hypothesis.
why it matters
In the forcing chain, T5 forces unique $J$; this bridge is how that uniqueness enters discrete gravity rather than remaining a pure functional-equation fact. It is a direct field of CompleteForcingChain and the required hypothesis of T5Regge_To_ContinuumLimit_Bridge, which carries the local nonlinear Regge/$J$ surface into continuum completion (weak-field/refinement fully backed; full nonlinear Einstein--Hilbert still conditional).
Framework landmarks: T5 $J$-uniqueness and the RCL-derived form $J(x)=\cosh(\log x)-1$; the eight-tick and $D=3$ steps sit later (T7--T8), but the six-tet Freudenthal stencil already assumes 3D triangulation geometry consistent with that spatial dimension. Without this certificate, continuum and physical-lattice Dirichlet models cannot cite forced $J$ as the edge action.
The inhabiting theorem closes the scaffolding for the discrete side; open residual risk lives in the next bridge's nonlinear continuum layer, not in these algebraic identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.