rs_eta_11
plain-language theorem explainer
The (1,1) entry of the RS-derived Minkowski metric equals +1. Researchers unifying the Recognition Science forcing chain with general relativity cite this when confirming the positive spatial signature of the metric tensor. The proof is a direct simplification that unfolds the piecewise definition of rs_eta on matching indices.
Claim. Let $eta : Fin 4 to Fin 4 to R$ be the RS Minkowski metric with $eta_{ij}=0$ for $i neq j$, $eta_{00}=-1$, and $eta_{ii}=1$ for $i=1,2,3$. Then $eta_{11}=1$.
background
The module proves that the Minkowski metric forced by the Recognition Science T0-T8 chain coincides with the IndisputableMonolith eta tensor. The derivation runs RCL to J-uniqueness (T5) to J''(1)=1, then the eight-tick octave (T7) and D=3 (T8), producing diag(-1,+1,+1,+1). The local rs_eta is defined as the function that returns 0 off-diagonal, -1 on the time-time entry, and +1 on the three spatial diagonal entries.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of rs_eta. Unfolding the if-then-else cases on equal indices with the second index equal to 1 immediately yields the value 1.
why it matters
This entry check anchors the spatial part of the metric that the T5-T8 chain forces. It supports the module's main results such as rs_eta_eq_im_eta (pointwise equality with the IM eta) and rs_minkowski (identification with the canonical MetricTensor). The declaration therefore lets downstream GR constructions (Christoffel symbols, geodesics) operate directly on the RS-derived metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.