bridge_certificate
plain-language theorem explainer
The bridge_certificate theorem asserts that the DiscreteContinuumBridge structure is inhabited under the Regge convergence hypothesis by supplying its fields from flat-chain and curvature results. Lattice-to-continuum modelers in quantum gravity would cite it to close the link from J-cost defects to the Einstein equations. The construction is a direct structure instantiation that combines proved lemmas with the external hypothesis.
Claim. Assuming the nonlinear Regge calculus convergence hypothesis, the complete discrete-to-continuum bridge certificate holds: the flat chain property is satisfied, the coupling $8phi^5$ is positive, spacetime dimension equals 4, the Christoffel symbols of the Minkowski metric are torsion-free, the Levi-Civita connection exists and is unique, and the Regge action converges to the Einstein-Hilbert action.
background
The module connects J-cost lattice theory to continuum GR through quadratic defects, lattice Laplacians, Ricci scalars, and the Einstein tensor. The ReggeConvergenceHypothesis is defined as the statement that on simplicial manifolds with mesh tending to zero the Regge action converges to the Einstein-Hilbert action (Cheeger-Muller-Schrader 1984). The DiscreteContinuumBridge structure packages the flat chain, coupling positivity, dimension equality, torsion-freeness, and Levi-Civita theorems as a single Prop.
proof idea
The proof instantiates the DiscreteContinuumBridge structure by direct field assignment: flat_chain to flat_chain_holds, coupling_positive to coupling_from_phi, dimension via norm_num, christoffel_torsion_free and the two Levi-Civita properties from the fundamental theorems on the Minkowski tensor, and regge_convergence to the supplied hypothesis. It is a structure constructor that relies on prior lemmas in the module and the external hypothesis.
why it matters
This declaration supplies the bridge certificate that is used by the end_to_end theorem to assemble the full chain from the Recognition Composition Law through J-uniqueness, phi, D=3, the eight-tick octave, and curvature tensors to the Einstein field equations. It occupies the Tier 3 slot in the module architecture, packaging the external Regge convergence result alongside proved elements. The embedded summary comment lists the five external hypotheses as standard mathematics rather than RS-specific assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.