module module high

`IndisputableMonolith.Relativity.Geometry.MetricUnification`

The module defines the RS-forced Minkowski metric as a function Fin 4 → Fin 4 → ℝ together with its component equalities. Researchers bridging the discrete Recognition Science lattice to continuum GR would cite these definitions when importing the geometry layer. The module is a collection of direct definitions and equality lemmas with no tactic proofs.

claimThe RS Minkowski metric is the function $rs_eta : Fin 4 → Fin 4 → ℝ$ with $rs_eta(0,0) = -1$, $rs_eta(i,i) = 1$ for $i=1,2,3$, and $rs_eta(μ,ν)=0$ otherwise, satisfying $rs_eta = rs_minkowski$ and the standard diagonal form forced by the T0-T8 chain.

background

This module belongs to the Relativity.Geometry section and supplies the metric that appears in the discrete-to-continuum bridge. It imports the Tensor, Metric, and Curvature modules; the Tensor import is explicitly marked as scaffolding and outside the certificate chain. The supplied doc-comment states that the metric is the RS-style Minkowski form forced by the T0-T8 chain (T5 J-uniqueness through T8 D=3 spatial dimensions). Sibling declarations rs_eta, rs_minkowski, rs_eta_00 through rs_eta_offdiag, and rs_eta_symm give the explicit components and symmetry.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Geometry aggregator (which re-exports all geometry components) and the DiscreteBridge module whose doc-comment describes the chain J-cost lattice → quadratic defect → lattice Laplacian → Ricci scalar → Einstein tensor → EFE. It therefore supplies the metric object required for any later derivation of the Einstein field equations inside the Recognition Science framework.

scope and limits

Does not derive the T0-T8 forcing chain.
Does not compute Christoffel symbols or curvature tensors.
Does not treat non-Minkowski or curved metrics.
Does not contain lattice J-cost or discrete defect definitions.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Relativity.Geometry module_import
IndisputableMonolith.Relativity.Geometry.DiscreteBridge module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Relativity.Geometry.Curvature module_import
IndisputableMonolith.Relativity.Geometry.Metric module_import
IndisputableMonolith.Relativity.Geometry.Tensor module_import

declarations in this module (18)

def rs_eta L45
theorem rs_eta_eq_im_eta L51
def rs_minkowski L63
theorem rs_minkowski_eq L66
theorem rs_eta_00 L70
theorem rs_eta_11 L71
theorem rs_eta_22 L72
theorem rs_eta_33 L73
theorem rs_eta_offdiag L75
theorem rs_eta_symm L78
theorem minkowski_real_christoffel_zero L94
theorem scaffold_agrees_on_minkowski L99
structure RealGeodesic L110
structure TimelikeGeodesic L121
structure RealNullGeodesic L130
structure SpacelikeGeodesic L139
theorem geodesic_uses_real_christoffel L149
theorem minkowski_straight_line_geodesic L160