T5Regge_To_ContinuumLimit_Bridge
plain-language theorem explainer
Certificate packaging the passage from unique J-cost through nonlinear Regge action to a continuum limit: weak-field lattice–manifold correspondence, unique zero-spacing completion, and vanishing action error, with full nonlinear Einstein–Hilbert kept explicitly conditional on named Regge axioms. The complete forcing chain and its holds theorem cite it. Definitional Prop bundle with a trivial Subsingleton instance.
Claim. Given $J$-uniqueness (reciprocity, normalization, the Recognition Composition Law, calibration, continuity) and the nonlinear Regge/$J$-cost bridge, the continuum bridge asserts: the local Regge action is available; every weak-field metric input admits a lattice–manifold correspondence certificate; for every positive box length a canonical refinement exists; discrete refinement completes uniquely at spacing $0$; the weak-field action error $M^2 a^2/10\to 0$ as $a\to 0$; and a full nonlinear Einstein–Hilbert certificate exists only if the three named Regge convergence axioms hold.
background
The module UnifiedForcingChain forces the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law, normalization, calibration). T5 is $J$-uniqueness: on $(0,\infty)$, those hypotheses pin $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$).
The immediate upstream certificate is the T5-to-nonlinear-Regge/$J$-cost bridge: it carries that uniqueness theorem into a discrete curvature-action surface. Continuum completion is phrased via DiscreteReggeCompletionLimit: for a lattice refinement $R$, spacing tends to a limit $\ell$ in the usual $\varepsilon$-$N_0$ sense. Weak-field data and lattice refinements live in the unified lattice–manifold correspondence layer; the nonlinear Einstein–Hilbert route is gated by three external Regge convergence axioms (action, Ricci, Riemann), not assumed silently.
proof idea
This declaration is a structure (a Prop certificate), not a proved theorem. Its fields are named obligations: re-export the local Regge bridge; universal weak-field correspondence and existence of refinements at any positive box length; zero-spacing completion and uniqueness of that limit; a one-line filter tendsto for the quadratic weak-field action error; and an implication from the three named nonlinear Regge axioms to a nonempty nonlinear unified certificate.
The companion theorem t5regge_to_continuum_limit_bridge_holds is what discharges the fields (starting from regge_local_action_available := hRegge). The Subsingleton instance is allEq by rfl: as a Prop-valued structure, any two inhabitants are definitionally equal.
why it matters
Sits on the T5 rung of the forcing chain: unique $J$ is not left as a pure cost identity; it is wired through nonlinear Regge discrete gravity into a continuum-completion certificate. Downstream, CompleteForcingChain consumes this bridge among the post-T5 gravity/continuum layers, and t5regge_to_continuum_limit_bridge_holds is the constructive inhabitant.
The design is deliberately split: weak-field refinement and zero-spacing uniqueness are theorem-backed obligations, while full nonlinear Einstein–Hilbert is conditional on named external Regge convergence inputs. That keeps the complete inevitability claim honest about where continuum GR is forced versus where it still depends on classical Regge-limit hypotheses. Framework landmarks: T5 $J$-uniqueness and the RCL-driven cost foundation; continuum $D=3$ geometry is the ambient setting, not re-proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.