VolumeElement
plain-language theorem explainer
The VolumeElement structure records a positive real grid spacing that discretizes the four-dimensional spacetime volume form equipped with the metric factor sqrt(-g). Researchers constructing discretized Einstein-Hilbert or scalar-field actions cite this record when approximating integrals on a uniform lattice. The declaration is a bare structure definition that packages only the spacing datum and its positivity constraint.
Claim. A volume element consists of a grid spacing $Δx ∈ ℝ$ satisfying $Δx > 0$, which supplies the discrete measure approximating $√(-g) d^4x$.
background
The module supplies discrete integration over spacetime via a uniform grid whose spacing enters the measure $Δx^4 ∑ √(-g)$. The structure carries only this spacing together with the proof of its positivity. Upstream results include the ILG alias that forwards the same record and the integrate_scalar routine that consumes it to form finite weighted sums; the Shannon uniform distribution and forcing self-reference structures appear only as indirect dependencies.
proof idea
The declaration is a structure definition with two fields: the real-valued grid spacing and the hypothesis that it is strictly positive. No lemmas or tactics are invoked; the record simply packages the data required by all downstream integration functions.
why it matters
This definition supplies the volume measure consumed by einstein_hilbert_action, kinetic_action, potential_action and the linearity theorems integrate_add and integrate_smul. It therefore forms the discrete foundation for the Einstein-Hilbert and field actions that realize the Recognition framework's spacetime integrals. The construction supports the eight-tick octave and D = 3 spatial dimensions by providing the four-dimensional volume element, while the continuous-measure limit remains an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.