metric_to_matrix
plain-language theorem explainer
metric_to_matrix converts a MetricTensor into its explicit 4x4 real matrix at a spacetime point x by evaluating the underlying bilinear form. Discrete relativity and Regge calculus calculations cite it when moving from abstract tensor interfaces to matrix inversion or determinant steps. The definition is a direct functional extraction that fixes the upper index to the zero vector and selects the lower index conditionally between the row and column arguments.
Claim. For a metric tensor $g$ and point $x$, the matrix $M$ has entries $M_{ij} = g.g(x, 0, k)$ where the lower index vector $k$ satisfies $k_0 = i$ and $k_1 = j$.
background
The MetricTensor structure packages a bilinear form $g$ together with a symmetry axiom that equates the form under swap of the two lower indices. The Relativity.Geometry.Metric module supplies this conversion after importing the tensor and derivative layers, placing the construction inside a 4-dimensional spacetime setting that abstracts local metric components for discrete models.
proof idea
The definition is a one-line wrapper that applies the bilinear form component of MetricTensor at the supplied point $x$, with the upper index fixed to the zero vector and the lower index built by the conditional selector that returns $i$ on the first Fin 2 slot and $j$ on the second.
why it matters
Downstream definitions such as inverse_metric, metric_det, and metric_matrix_invertible_at in DiscreteBridge rely on this conversion to obtain concrete matrix objects. It supplies the matrix representation needed for non-degeneracy checks that mirror the variational invertibility hypothesis and for Regge-calculus convergence statements referenced in the DiscreteBridge documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.