scaffold_agrees_on_minkowski
plain-language theorem explainer
The theorem shows that Christoffel symbols computed from the Minkowski metric tensor vanish for every coordinate and index. Researchers bridging Recognition Science forcing chains to standard general relativity would cite it when replacing scaffold placeholders with the Levi-Civita connection. The proof is a one-line term simplification that invokes the pre-established vanishing result for the real Christoffel symbols on Minkowski.
Claim. For the Minkowski metric tensor given by the diagonal matrix with entries $(-1, +1, +1, +1)$, the Christoffel symbols of the Levi-Civita connection satisfy $0 = {}^4R^ρ_{μν}(x)$ for every $x ∈ ℝ⁴$ and every index triple $ρ, μ, ν ∈ {0,1,2,3}$.
background
The module establishes pointwise equality between the Minkowski metric obtained from the Recognition Science forcing chain (RCL → J-uniqueness at T5 → eight-tick octave at T7 → D = 3 at T8) and the standard MetricTensor used in the relativity stack. The Christoffel symbols are the standard coefficients of the Levi-Civita connection derived from a metric tensor g. The upstream christoffel definition supplies the general Hessian-metric formula, while the sibling result minkowski_real_christoffel_zero supplies the specialized vanishing statement for the flat case.
proof idea
The proof is a one-line term-mode wrapper that applies the lemma minkowski_real_christoffel_zero, which states that the real Christoffel symbols vanish identically on the Minkowski metric tensor.
why it matters
The declaration closes the scaffold-to-real transition for the flat metric, allowing all downstream GR structures (geodesics, curvature tensors) to operate directly on the RS-derived η without duplication. It sits inside the module whose main results include rs_minkowski_eq and the geodesic structures that replace scaffold versions with Curvature.christoffel. It directly supports the framework step from T8 (D = 3) to a usable spacetime metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.