IndisputableMonolith.Relativity.Geometry.MetricUnification
The MetricUnification module supplies the RS-style Minkowski metric as a function Fin 4 to Fin 4 to real numbers, forced by the T0-T8 chain. Researchers bridging discrete J-cost lattices to continuum GR cite it to fix the flat baseline before curvature calculations. The module consists of direct definitions and equality lemmas that realize the metric without complex derivations.
claimThe RS Minkowski metric is the function $g: 4$-indices to $4$-indices to reals with signature $(-1,1,1,1)$, diagonal entries $g_{00}=-1$ and $g_{ii}=1$, and all off-diagonal entries zero, satisfying the symmetry and flat-space conditions required by the T0-T8 forcing chain.
background
This module sits inside the Relativity.Geometry namespace and imports the Tensor scaffold, the Metric definitions, and the Curvature derivations. It introduces the RS-style Minkowski metric as the flat-space object forced by the T0-T8 chain, where T8 sets three spatial dimensions inside four-dimensional spacetime. The upstream Curvature module supplies Christoffel symbols derived from this metric, while the Tensor import is explicitly marked as a scaffold outside the certificate chain.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the flat metric baseline that the DiscreteBridge uses to connect lattice J-cost to the Einstein field equations via the Ricci scalar. It realizes the metric component of the T0-T8 forcing chain and is re-exported by the Geometry aggregator for all downstream relativity calculations.
scope and limits
- Does not derive the metric from axioms beyond the T0-T8 forcing chain.
- Does not treat curved or dynamical metrics.
- Does not include numerical evaluation or simulation code.
- Does not address quantum or higher-dimensional extensions.
used by (2)
depends on (3)
declarations in this module (18)
-
def
rs_eta -
theorem
rs_eta_eq_im_eta -
def
rs_minkowski -
theorem
rs_minkowski_eq -
theorem
rs_eta_00 -
theorem
rs_eta_11 -
theorem
rs_eta_22 -
theorem
rs_eta_33 -
theorem
rs_eta_offdiag -
theorem
rs_eta_symm -
theorem
minkowski_real_christoffel_zero -
theorem
scaffold_agrees_on_minkowski -
structure
RealGeodesic -
structure
TimelikeGeodesic -
structure
RealNullGeodesic -
structure
SpacelikeGeodesic -
theorem
geodesic_uses_real_christoffel -
theorem
minkowski_straight_line_geodesic