rs_eta_22
plain-language theorem explainer
The theorem confirms that the Recognition Science Minkowski metric evaluates to 1 at the (2,2) position. Physicists bridging RS forcing chains to standard general relativity cite this when confirming the positive spatial signature. The proof proceeds by direct simplification against the piecewise definition of rs_eta.
Claim. $rs_eta(2,2)=1$, where $rs_eta(i,j)$ returns $-1$ if $i=j=0$, $+1$ if $i=j>0$, and $0$ otherwise.
background
The module establishes equivalence between the metric forced by the T0-T8 chain in Recognition Science and the standard Minkowski tensor used in the IndisputableMonolith relativity stack. The function $rs_eta : Fin 4 → Fin 4 → ℝ$ is defined to return $-1$ on the time-time component and $+1$ on the three spatial diagonals, with off-diagonals zero. This definition originates from the chain RCL → J-uniqueness (T5) → eight-tick octave (T7) → D=3 (T8). The upstream $rs_eta$ in CMB Temperature supplies the baryon-to-photon ratio but is not used here; the local $rs_eta$ definition drives the simplification.
proof idea
The proof is a one-line wrapper that invokes the simplifier on the definition of $rs_eta$, which directly yields 1 for the (2,2) entry since the index is spatial.
why it matters
This result verifies a spatial diagonal entry of the RS metric, supporting the parent claim $rs_eta_eq_im_eta$ that equates the two metric definitions. It fills the T8 step of the forcing chain by confirming D=3 yields the expected signature diag(-1,+1,+1,+1). No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.