flat_chain_holds
plain-language theorem explainer
The Minkowski flat chain asserts that the standard Minkowski metric produces identically zero Christoffel symbols, Riemann tensor, Ricci tensor, scalar curvature, and Einstein tensor. Researchers verifying the flat-space limit of Recognition Science's discrete lattice would reference this when confirming the vanishing of curvature quantities. The proof proceeds by term-mode record construction that directly supplies the zero identities already established for the Minkowski tensor.
Claim. The Minkowski metric satisfies the flat chain: its Christoffel symbols vanish identically, the Riemann tensor is identically zero, the Ricci tensor vanishes, the Ricci scalar is zero, and the Einstein tensor is zero.
background
The Discrete-to-Continuum Bridge module connects the J-cost lattice to continuum GR via the chain J-cost lattice to quadratic defect to lattice Laplacian to Ricci scalar to Einstein tensor. FlatChain encodes the Minkowski case of this chain: from the metric through vanishing connection and curvature tensors to a zero Einstein tensor. The module states that the flat limit forms the first proved tier, including spatial metric from J-cost, Laplacian convergence at O(a²), coupling κ = 8φ⁵, and D = 3.
proof idea
The proof is a term-mode record construction that populates each field of the FlatChain structure with the corresponding zero lemma for the Minkowski tensor. It supplies the Christoffel zero identity and the zero identities for the Riemann, Ricci, scalar, and Einstein tensors.
why it matters
This theorem supplies the flat_chain field required by bridge_certificate, which assembles the full DiscreteContinuumBridge modulo the Regge convergence hypothesis. It completes the proved Tier 1 of the discrete-to-continuum bridge, confirming that the J-cost lattice recovers the flat Einstein equations. The result aligns with the Recognition Science forcing chain by establishing the Minkowski case as the base for the eight-tick octave and three-dimensional spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.