metric_from_rrf
plain-language theorem explainer
metric_from_rrf constructs a metric tensor by adding a diagonal term k psi(x) to the Minkowski eta bilinear form. Workers building perturbed spacetimes in scalar-tensor or recognition-based gravity cite it for explicit coordinate expressions. The body assembles the g component directly and verifies symmetry via a two-case split on index equality.
Claim. The metric tensor satisfies $g(x,up,low) = eta(x,up,low) + k psi(x)$ when the two indices in low coincide and $g(x,up,low) = eta(x,up,low)$ otherwise, where eta returns the Minkowski values $-1$ (time) or $+1$ (space) on the diagonal and zero off-diagonal.
background
The MetricTensor structure packages a bilinear form g with a symmetry axiom that equates evaluation on an index pair and its swap. The eta function supplies the flat Minkowski bilinear form, nonzero only on matching indices and carrying the signature diag(-1,1,1,1). This definition lives inside the Relativity.Geometry.Metric module, which imports tensor and derivative support to express local metric components.
proof idea
The definition populates g by summing the eta form (applied at zero up-index) with the perturbation k psi(x) on equal indices. Symmetry follows by unfolding eta, dsimp, then case analysis on index equality; each branch rewrites the conditional to equate the two sides.
why it matters
The construction supplies a concrete perturbed metric inside the relativity geometry layer, ready for use in gravity and cosmology modules though no direct dependents are recorded yet. It preserves the four-index structure required by the eight-tick octave while allowing scalar modifications, consistent with the D=3 spatial setting of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.