rs_eta
plain-language theorem explainer
The rs_eta definition supplies the Minkowski metric in RS-native form as a function on Fin 4 indices. Researchers working on metric unification in Recognition Science would cite it when bridging the T0-T8 forcing chain to standard GR calculations. The definition is a direct case distinction on the indices that encodes the signature diag(-1, +1, +1, +1).
Claim. The RS Minkowski metric function on indices $i,j$ in Fin 4 is defined by returning 0 when $i$ differs from $j$, returning -1 when $i=0$ on the diagonal, and returning +1 on the remaining diagonal entries.
background
The Metric Unification module constructs the RS-derived metric to match the IndisputableMonolith Relativity stack. The forcing chain produces the metric via RCL, J-uniqueness (T5), the eight-tick octave (T7), and D=3 (T8), yielding diag(-1, +1, +1, +1). The BilinearForm abbrev from Tensor defines the interface as Tensor 0 2, while the IM eta definition returns -1 or +1 on the diagonal according to the low index.
proof idea
The definition is implemented directly via conditional expressions on whether the indices are equal and whether the first index is zero. It matches the structure of the upstream eta definition in Metric.eta by unfolding the cases for diagonal and off-diagonal entries.
why it matters
This definition serves as the base for the unification theorems rs_eta_eq_im_eta and rs_minkowski_eq, which establish that the RS metric coincides with minkowski_tensor. It closes the bridge from the T0-T8 chain to downstream GR structures such as Christoffel symbols and geodesics. The module doc notes that all downstream GR theorems operate on this RS-derived metric without duplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.