IndisputableMonolith.Relativity.Geometry.MetricUnification
Module supplies the Minkowski metric forced by the T0-T8 chain, expressed as a map from four indices to reals. Researchers linking lattice J-cost to Einstein equations cite it as the flat-space base case. It consists of definitions and equalities that instantiate the chain output with no internal proofs.
claimThe RS Minkowski metric $\eta : \mathrm{Fin}\,4 \to \mathrm{Fin}\,4 \to \mathbb{R}$ with diagonal entries $(1,-1,-1,-1)$ and vanishing off-diagonal entries, as forced by the T0-T8 chain.
background
The module sits inside the Relativity.Geometry hierarchy and imports the Tensor scaffold (explicitly marked outside the certificate chain), the Metric definitions, and the Curvature module whose doc-comment states it derives Christoffel symbols from the metric. The local theoretical setting is the flat spacetime metric required by the T0-T8 forcing chain in Recognition Science, with the supplied doc-comment identifying the object as the RS-style Minkowski metric.
Sibling declarations in the same module introduce rs_eta, rs_minkowski and their equality lemmas, establishing the concrete component values and symmetry properties. This metric then serves as the starting point for curvature calculations and the discrete-to-continuum bridge.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module feeds the Geometry aggregator and the DiscreteBridge module. The latter's doc-comment states it connects J-cost lattice to quadratic defect, lattice Laplacian, Ricci scalar, Einstein tensor and the Einstein field equations. It therefore supplies the flat-space foundation step required by the T0-T8 chain for the Recognition Science derivation of general relativity.
scope and limits
- Does not derive the metric from the Recognition Composition Law.
- Does not treat curved or non-Minkowski spacetimes.
- Does not contain numerical checks against laboratory values.
- Does not address coordinate transformations or frame changes.
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