rs_eta_offdiag
plain-language theorem explainer
The off-diagonal components of the RS-derived Minkowski metric vanish for distinct indices in Fin 4. Researchers unifying the forcing-chain metric with standard relativity tensors would cite this to lock in the diagonal structure of η. The result is a one-line simplification that unfolds the piecewise definition of rs_eta under the i ≠ j hypothesis.
Claim. For $i,j$ in the set of four indices with $i≠j$, the RS Minkowski metric satisfies $η_{ij}=0$.
background
The module establishes pointwise agreement between the metric forced by the T0-T8 chain (RCL to J-uniqueness to eight-tick octave to D=3) and the IndisputableMonolith eta tensor. The function rs_eta implements this metric explicitly: it returns zero whenever the indices differ and otherwise returns −1 for the time component or +1 for the spatial components. Upstream, the same name appears in CMB Temperature for the baryon-to-photon ratio, but the local definition here is the metric map used for all subsequent Christoffel and geodesic work.
proof idea
One-line wrapper that applies the simp tactic to the definition of rs_eta together with the supplied hypothesis i ≠ j.
why it matters
The lemma supplies the off-diagonal vanishing required by the Minkowski form that emerges from T7 (eight-tick) and T8 (D=3). It directly supports the parent equality rs_eta_eq_im_eta that identifies the RS metric with the standard Minkowski tensor, allowing the entire downstream GR stack (Christoffel symbols, geodesics) to run on the Recognition-derived η without duplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.