sqrt_minus_g
plain-language theorem explainer
Placeholder definition assigns the constant 1 to the square root of the negative metric determinant for any metric tensor and spacetime point. Integration routines in the same module cite it to form discrete volume sums for scalar fields and actions. The implementation is a direct constant assignment that bypasses all metric computation.
Claim. The factor $sqrt(-g)$ is defined as the constant $1$ for any metric tensor $g$ and coordinate $x in R^4$.
background
The module supplies discrete approximations to spacetime volume integrals that employ the measure factor $sqrt(-g)$. MetricTensor appears across modules as a structure supplying a local bilinear form on four spacetime indices, with variants that expose components, symmetry, or a determinant accessor. Upstream volume is defined as the cardinality of a finite vertex set. The local setting adopts a uniform grid spacing for summation and treats the full measure theory version as future work.
proof idea
Direct constant definition that returns 1 while ignoring both the metric tensor and coordinate arguments.
why it matters
The definition supplies the volume factor inside integrate_scalar, integrate_smul, and kinetic_nonneg. Those results establish scaling and nonnegativity of the kinetic action once the spatial gradient squared is nonnegative. It therefore scaffolds the discrete Einstein-Hilbert action construction ahead of a metric-determinant implementation that would incorporate the full geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.