metric_matrix_invertible_at
plain-language theorem explainer
The declaration defines non-degeneracy of the metric tensor at a spacetime point by requiring its matrix representation to be invertible. Workers on the discrete-to-continuum bridge in Recognition Science cite it inside the Regge convergence hypothesis. The definition is a direct one-line statement that the set of inverses for metric_to_matrix g x is nonempty.
Claim. Let $g$ be a metric tensor and $x : Fin 4 → ℝ$. The $4×4$ matrix representation of $g$ at $x$ is invertible.
background
The DiscreteBridge module builds the link from lattice J-cost structures to continuum curvature via the metric tensor. MetricTensor supplies a local bilinear form on spacetime points (Fin 4 → ℝ), with the matrix extraction metric_to_matrix turning this form into an explicit 4×4 array at each point. The module states a three-tier architecture: Tier 1 contains proved flat limits and Laplacian convergence from J-cost; Tier 2 contains the Christoffel-to-Einstein tensor chain; Tier 3 packages the external Regge convergence result as an explicit hypothesis rather than an axiom.
proof idea
This is a definition whose body is the direct assertion Nonempty (Invertible (metric_to_matrix g x)). No lemmas or tactics are applied; the expression itself encodes the invertibility condition.
why it matters
The definition supplies the invertibility premise inside ReggeConvergenceHypothesis, which states that on a sequence of simplicial manifolds with mesh tending to zero the Regge action converges to the Einstein-Hilbert action. It therefore closes the discrete-continuum bridge without importing the full variational stack. The surrounding module ties the construction to the Recognition Science forcing chain (T0–T8) and the eight-tick octave while keeping D = 3 spatial dimensions implicit in the lattice-to-curvature passage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.