sqrt_minus_g
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not evaluate the determinant of any metric components.
- Does not depend on the supplied coordinate values.
- Does not vary with position or curvature.
- Does not enforce any signature condition on the metric.
Lean usage
integrate_scalar f g volformal statement (Lean)
31noncomputable def sqrt_minus_g (_g : MetricTensor) (_x : Fin 4 → ℝ) : ℝ := 1
proof body
Definition body.
32
33/-- Integrate a scalar function over spacetime volume (discrete approximation). -/