Metric
plain-language theorem explainer
This abbreviation re-exports the metric tensor structure from the geometry module as a local alias for ILG action and field definitions. Researchers assembling Einstein-Hilbert terms, fluid continuum limits, or vacuum energy models cite it to avoid repeated module qualification when building functionals. The implementation is a direct one-line alias with no added structure or axioms.
Claim. Let $Metric$ denote the metric tensor structure consisting of a bilinear form $g$ on spacetime indices together with the symmetry condition $g(x, up, low) = g(x, up, low')$ where $low'$ flips the first index component, as provided by the geometry module.
background
The ILG action module re-exports geometry and field types to support variational principles in the Recognition framework. The aliased MetricTensor from Relativity.Geometry.Metric supplies a bilinear form $g$ with an explicit symmetry axiom on index flips. Upstream results supply parallel local metric interfaces: the Hamiltonian version offers a non-sealed default-zero form, the Gravity.Connection version adds an explicit symmetric 4x4 matrix with inverse, and the Homogenization version focuses on a determinant accessor.
proof idea
This is a direct abbreviation that aliases Geometry.MetricTensor with no further reduction or tactic steps.
why it matters
The alias feeds forty downstream declarations including coeff_bound_of_uniformBounds in continuum limits, SelfSustaining thresholds in vacuum energy, and christoffel_symmetric in connection geometry. It standardizes metric access for the relativity layer of the Recognition Science forcing chain, supporting the eight-tick octave and D=3 spatial dimension derivations while enabling RCL-compatible action integrals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.