DiscreteContinuumBridge
plain-language theorem explainer
DiscreteContinuumBridge bundles the flat spacetime chain, the positivity of the coupling 8 phi^5, four-dimensionality, torsion-free Christoffel symbols on Minkowski space, Levi-Civita existence and uniqueness, and the Regge convergence hypothesis into one Prop. Researchers tracing lattice J-cost models to the Einstein equations cite it to mark the boundary between proved RS components and the external convergence assumption. The declaration is a direct structure definition with no computation or lemmas applied.
Claim. The discrete-to-continuum bridge certificate is the proposition asserting that the flat spacetime chain holds, that $8 phi^5 > 0$, that spacetime has dimension 4, that the Christoffel symbols of the Minkowski metric are torsion-free, that the Levi-Civita connection exists and is unique for the Minkowski metric, and that the Regge convergence hypothesis holds.
background
FlatChain is the structure recording that the Minkowski metric yields vanishing Christoffel symbols, Riemann tensor, Ricci tensor, scalar curvature, and Einstein tensor. ReggeConvergenceHypothesis is the external statement that the Regge action on a sequence of simplicial manifolds with mesh tending to zero converges to the Einstein-Hilbert action, citing Cheeger-Muller-Schrader 1984. The module sets the local theoretical setting as the three-tier bridge from J-cost lattice through quadratic defect and lattice Laplacian to the Einstein field equations, with Tier 1 and Tier 2 proved inside the Recognition framework and Tier 3 packaged as hypothesis.
proof idea
The declaration is a structure definition that directly assembles the seven listed properties into a single proposition; no tactics or lemmas are applied.
why it matters
It supplies the central certificate that feeds the bridge_certificate theorem and the EndToEndChain structure. The certificate packages the proved flat limit and curvature chain (from T5 J-uniqueness through T8 D=3 and the Levi-Civita theorems) together with the single external Regge hypothesis, thereby closing the explicit accounting of what is proved versus hypothesized on the path from the Recognition Composition Law to the Einstein field equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.