metric_to_matrix
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove symmetry or positive-definiteness of the output matrix.
- Does not specialize the tensor to the Minkowski form.
- Does not perform index raising, lowering, or coordinate transformations.
- Does not compute curvature scalars or connection coefficients.
Lean usage
noncomputable def use_example (g : MetricTensor) (x : Fin 4 → ℝ) : Matrix (Fin 4) (Fin 4) ℝ := metric_to_matrix g xformal statement (Lean)
49noncomputable def metric_to_matrix (g : MetricTensor) (x : Fin 4 → ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
proof body
Definition body.
50 fun i j => g.g x (fun _ => 0) (fun k => if (k : ℕ) = 0 then i else j)
51
52/-- The metric matrix is symmetric because the metric tensor is symmetric. -/