rs_minkowski_eq
plain-language theorem explainer
The theorem states that the Recognition Science Minkowski metric tensor coincides exactly with the standard Minkowski tensor from the IndisputableMonolith relativity library. Researchers unifying the forcing chain with general relativity would cite this equality to apply curvature and geodesic results directly to the RS-derived metric. The proof is a single reflexivity step that follows immediately from the definition of the RS metric as the standard tensor.
Claim. The Recognition Science Minkowski metric tensor equals the standard Minkowski tensor, i.e., $M_{RS} = M_{IM}$ where both are elements of the type of symmetric bilinear forms on four-dimensional spacetime with signature $(-1,+1,+1,+1)$.
background
The module establishes that the Minkowski metric obtained from the Recognition Science forcing chain equals the IndisputableMonolith definition. The chain proceeds from the Recognition Composition Law through J-uniqueness (T5), the second derivative condition J''(1)=1, the eight-tick octave (T7), and the emergence of three spatial dimensions (T8) to yield the diagonal form diag(-1,+1,+1,+1). Upstream, minkowski_tensor is defined as the MetricTensor whose g component is the eta matrix with the required symmetry. The sibling definition rs_minkowski simply sets the RS-derived MetricTensor to minkowski_tensor.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity. Because rs_minkowski is definitionally equal to minkowski_tensor by its own declaration, the equality rs_minkowski = minkowski_tensor holds by rfl without further computation or tactic steps.
why it matters
This equality supplies the required bridge so that all downstream general-relativity theorems (Christoffel symbols, Riemann tensor, Ricci curvature, Einstein equations, and geodesics) operate on the RS-derived metric without duplication or redefinition. It closes the link between the forcing-chain landmarks (RCL, T5 J-uniqueness, T7 eight-tick octave, T8 D=3) and the concrete MetricTensor used in the relativity stack. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.