rs_minkowski
plain-language theorem explainer
The RS-derived Minkowski metric is supplied as a MetricTensor instance that matches the IndisputableMonolith definition exactly. Physicists bridging Recognition Science forcing chains to standard general relativity would cite this to avoid duplicating metric definitions in curvature and geodesic calculations. The construction is a direct abbreviation equating the two structures.
Claim. The Recognition Science Minkowski metric tensor is defined to be identical to the standard Minkowski metric tensor, where the components satisfy $g_{00}=-1$ and $g_{11}=g_{22}=g_{33}=1$ with all off-diagonal entries zero.
background
The Metric Unification module shows that the Minkowski metric derived from the Recognition Science forcing chain equals the IndisputableMonolith stack's eta. The chain proceeds from the Recognition Composition Law through J-uniqueness (T5), the eight-tick octave (T7), and D=3 (T8) to yield diag(-1,+1,+1,+1). MetricTensor is a local bilinear form interface appearing as a symmetric 4x4 matrix in Gravity.Connection and as a functional form g : (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ in Hamiltonian.
proof idea
This is a one-line abbreviation that directly assigns the RS metric to the existing minkowski_tensor definition from the Metric module.
why it matters
This definition supplies the canonical MetricTensor for all downstream relativity theorems in the module, including the equality proof rs_minkowski_eq and geodesic structures. It completes the unification step in the forcing chain from RCL through T5, T7, T8 to the explicit Minkowski form, allowing GR results to inherit the RS derivation without redefinition. The parent result rs_minkowski_eq confirms definitional equality, closing the bridge for Einstein equations and timelike geodesics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.