t5regge_to_continuum_limit_bridge_holds
plain-language theorem explainer
Given unique J-cost (T5) and the nonlinear Regge/J-cost bridge, the continuum completion certificate holds: weak-field lattice–manifold correspondence, vanishing action error under refinement, unique zero completion limit, and a conditional path to full nonlinear Einstein–Hilbert. Cited by the complete forcing chain assembler. Proof is a structure constructor wiring Gravity lattice-manifold lemmas and discrete Regge completion uniqueness.
Claim. Assume $J$ is the unique reciprocal, normalized, calibrated continuous cost satisfying the Recognition Composition Law, and assume the nonlinear Regge/$J$-cost bridge from that uniqueness. Then the Regge-to-continuum bridge holds: the local Regge action is available; every weak-field metric has a linearized lattice–manifold correspondence; lattice refinements exist; the canonical discrete Regge completion limit is zero and unique; weak-field action deviation tends to zero under refinement; and full nonlinear Einstein–Hilbert recovery holds conditionally on action/Ricci/Riemann hypotheses.
background
In the Unified Forcing Chain, T5 asserts that the Recognition Composition Law plus reciprocity, normalization $F(1)=0$, calibration $F''(1)=1$, and continuity force $J(x)=\frac12(x+1/x)-1$ on $(0,\infty)$. That uniqueness is packaged as a structure of cost hypotheses rather than a bare formula.
The preceding bridge certificate carries T5 into a nonlinear Regge curvature-action surface: discrete curvature measured in $J$-cost units. The continuum bridge is the next stage: complete that discrete action to a continuum geometric limit, first in the weak-field/refinement layer, then (conditionally) toward full nonlinear Einstein–Hilbert.
Module setting: every T0–T8 step is forced from the cost foundation. This declaration sits after T5 uniqueness and the Regge bridge, before the chain is assembled into the unconditional complete forcing chain.
proof idea
Structure constructor for the continuum bridge certificate. The Regge local-action field is the input Regge bridge hypothesis unchanged.
Weak-field correspondence is discharged by introducing a weak-field metric and refinement data, then applying Gravity.UnifiedLatticeManifoldCorrespondence.unifiedCorrespondence. Refinement existence and vanishing action deviation are direct citations of the corresponding lattice–manifold lemmas (exists_lattice_refinement_for_weak_field, actionDeviation_tendsto_zero).
Canonical completion zero is discreteReggeCompletionLimit_zero; uniqueness is discreteReggeCompletionLimit_unique_zero at positive mesh. The nonlinear full EH field is conditional: under action/Ricci/Riemann hypotheses it packages nonlinearUnified_of_cms.
why it matters
Feeds complete_forcing_chain, the top-level unconditional forcing-chain witness that threads T-1 through T8. Without this bridge, T5 uniqueness would stop at a discrete Regge action and would not connect to continuum gravity language used downstream of the chain.
Framework landmark: T5 J-uniqueness ($J(x)=\cosh(\log x)-1$) is the cost identity that calibrates curvature cost; the continuum bridge is how that discrete cost surface is completed toward Einstein–Hilbert geometry. Doc-comment is explicit: weak-field/refinement is theorem-backed; full nonlinear EH remains conditional on named geometric hypotheses.
Closes a scaffolding gap between discrete ledger cost and continuum GR recovery inside the forcing narrative, while keeping the nonlinear step honestly conditional rather than overclaimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.