rs_eta_symm
plain-language theorem explainer
The Recognition Science-derived Minkowski metric tensor satisfies symmetry in its components for all index pairs in Fin 4. Researchers unifying the forcing chain output with the IndisputableMonolith relativity stack cite this to confirm the tensor is symmetric before invoking Christoffel symbols or curvature. The proof unfolds the rs_eta definition then splits on index equality, applying reflexivity on the diagonal case and simplification off-diagonal.
Claim. For the Recognition Science Minkowski metric with components indexed by $i,j$ in Fin 4, the components satisfy $rs_eta_{ij} = rs_eta_{ji}$.
background
The MetricUnification module bridges the Minkowski metric obtained from Recognition Science's forcing chain (RCL to J-uniqueness to eight-tick octave to D=3) with the IndisputableMonolith Geometry stack. The function rs_eta supplies the components of this RS-derived metric, which the module shows equals the standard diag(-1,+1,+1,+1) form. Upstream results include the Christoffel definition in Action.EulerLagrange (the Hessian-metric symbol) and the module's own rs_eta_eq_im_eta equality, though the symmetry step depends only on the component definition itself.
proof idea
The term proof first unfolds rs_eta to expose the underlying case expression. It then applies by_cases on whether i equals j. When equal, substitution yields reflexivity. When unequal, simp rewrites using the negated equality to obtain the off-diagonal zero or matching entries.
why it matters
Symmetry is required for rs_eta to serve as a valid metric tensor in the unification, feeding the module's main results rs_minkowski and rs_eta_eq_im_eta. It closes one tensor-property check in the RS-to-GR bridge, consistent with the forcing-chain derivation of eta = diag(-1,+1,+1,+1) from T7 and T8. No open scaffolding remains for this property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.