rs_eta_33
plain-language theorem explainer
The declaration shows that the RS Minkowski metric evaluates to 1 at indices 3 and 3. Workers on Recognition Science derivations of spacetime cite this when confirming the positive signature on spatial directions. The proof reduces directly by simplification against the piecewise definition of the metric function.
Claim. Let $η : Fin 4 → Fin 4 → ℝ$ be defined by $η(i,j) = 0$ if $i ≠ j$, $η(0,0) = -1$, and $η(i,i) = 1$ for $i ≠ 0$. Then $η(3,3) = 1$.
background
The module proves that the Minkowski metric forced by the Recognition Science chain (RCL to J-uniqueness at T5, eight-tick at T7, D=3 at T8) coincides with the standard eta tensor. The function rs_eta implements this metric explicitly as a map on Fin 4 indices: zero off-diagonal, -1 at (0,0), and +1 on the remaining diagonal entries. An upstream scalar rs_eta in CMB Temperature gives the baryon-to-photon ratio, but the local geometric version governs the present result. The chain yields the diagonal form diag(-1, +1, +1, +1).
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of rs_eta, which resolves the conditional for equal indices 3 and 3 to the constant 1.
why it matters
This supplies one diagonal spatial case required for the parent equality rs_eta_eq_im_eta between the RS and IM metrics. It directly instantiates the T8 forcing of three spatial dimensions with positive signature. The module thereby lets downstream GR constructions (Christoffel symbols, geodesics) operate on the RS-derived metric without redefinition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.