rs_eta_eq_im_eta
plain-language theorem explainer
The declaration establishes pointwise agreement between the Recognition Science Minkowski metric rs_eta and the IndisputableMonolith eta bilinear form on diagonal index pairs. Researchers unifying RS forcing chains with standard relativity would cite this to ensure curvature and geodesic calculations use a single metric definition. The proof is a short term-mode script that unfolds the two definitions, applies definitional simplification, and splits cases on index equality before simp.
Claim. For indices $μ, ν ∈ Fin 4$, the RS-derived Minkowski metric component $η_{RS}(μ, ν)$ equals the IM bilinear form $η(0, 0, λ)$ where the selector $λ : Fin 2 → Fin 4$ returns $μ$ when the first coordinate is 0 and $ν$ otherwise.
background
The Metric Unification module shows that the Minkowski metric obtained from the Recognition Science forcing chain is identical to the IndisputableMonolith Geometry.eta / minkowski_tensor. The chain runs RCL → J-uniqueness (T5) → J''(1)=1 → 8-tick octave (T7) → D=3 (T8) and yields η = diag(−1, +1, +1, +1). rs_eta is the concrete RS implementation of this metric; eta is the local non-sealed bilinear-form interface whose g field maps two vectors in (Fin 4 → ℝ) and an index selector in (Fin 2 → Fin 4) to ℝ, as defined in the Hamiltonian MetricTensor structure.
proof idea
The term proof unfolds rs_eta and eta, applies dsimp, then performs by_cases on μ = ν. The equal branch substitutes the hypothesis and finishes with simp; the unequal branch finishes with simp under the inequality hypothesis.
why it matters
This pointwise equality supplies the bridge that lets all downstream GR theorems (Christoffel symbols, Riemann tensor, geodesics) operate on the RS-derived metric without duplication. It directly supports the sibling result rs_minkowski that constructs the canonical MetricTensor and proves it equal to minkowski_tensor. The module doc states the result closes the gap between the T5–T8 forcing chain and the IndisputableMonolith relativity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.