Spacetime: a nonempty discrete spacetime with positive volume weights has positive total volume
ProvedEveryday.invariant_volumeThe source equation integrates every sector of its action against the invariant spacetime volume element ∫ d⁴x √(-g) — the label the image assigns to spacetime itself. The item is the volume element's positivity: the measure √(-g) d⁴x assigns positive volume to the everyday world, and in the discrete arena, a nonempty finite spacetime whose volume weights are positive at every point has strictly positive total volume.
Formalization Note The arena's spacetime is a finite type X with volume weights vol standing in for the measure √(-g) d⁴x. The hypotheses are nonemptiness of X and pointwise positivity of the weights; the conclusion is strict positivity of the finite sum. The proof is the positivity of a finite sum of positive summands over a nonempty index set.
import Mathlib import Definitions.Def_Everyday_spacetime import Definitions.Def_Everyday_sectors
open scoped BigOperators
namespace Everyday
/-- Spacetime: the invariant volume of the everyday world is positive —
the measure √(-g) d⁴x assigns positive volume, and a nonempty discrete
spacetime with positive volume weights has positive total volume. -/
theorem invariant_volume {X : Type} [Fintype X] [Nonempty X] (vol : X → ℝ)
(h : ∀ x, 0 < vol x) : 0 < ∑ x, vol x := by sorry
end Everyday
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every type X equipped with the structure of a finite type and the property of being nonempty, and every function vol assigning a real number to each element of X, if for every element x of X the real number vol x is strictly positive, then the real number zero is strictly less than the sum of vol x over all elements x of X. The conclusion is a strict inequality between real numbers.