default_volume
plain-language theorem explainer
Default volume element supplies unit grid spacing for discrete integration in relativistic action integrals. Researchers assembling ψ-sector kinetic and potential terms in the ILG framework reference it to supply the measure for Fields.kinetic_action. The definition is a direct record construction that sets grid_spacing to 1.0 and applies norm_num to confirm positivity.
Claim. The default volume element is the record with grid spacing equal to 1.0 together with the positivity witness $0 < 1$.
background
The ILG.Action module re-exports geometry and field types to support construction of action functionals. VolumeElement is an abbreviation for the structure in Fields.Integration that carries a real-valued grid spacing together with a proof that the spacing is positive; this supplies the discrete d⁴x measure used with the metric factor √(-g). The upstream kinetic_action definition takes a scalar field, metric tensor, and volume element to return (1/2) ∫ √(-g) g^{μν} (∂_μ ψ)(∂_ν ψ) d⁴x.
proof idea
One-line wrapper that applies the record constructor with grid_spacing := 1.0 and norm_num to discharge the positivity obligation.
why it matters
This definition supplies the concrete volume element required by PsiKinetic and PsiPotential, which assemble the ψ-sector kinetic and potential contributions to the ILG action. It bridges the symbolic integration interface in Fields.Integration to the concrete action terms, consistent with the volume-element structure used throughout the Relativity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.