Everyday spacetime: the path-integral amplitude and the gravity sector sum
Definitioneveryday_spacetimeThe source equation writes a transition amplitude W as a path integral — the integral of the exponential of i times the action over all field configurations with momenta below the ultraviolet cutoff Λ — and integrates its action against the invariant spacetime element ∫ d⁴x √(-g), whose gravity content is the Einstein–Hilbert term (m_p²/2) R. The bundle defines the two objects that carry this structure in the mission's arena. The amplitude: on a finite configuration space C, the path integral is the finite sum over configurations of the phase exp(i S c) — the exact discrete stand-in for the source's domain of integration. And the gravity sector: on a finite spacetime X with volume weights vol standing in for the measure √(-g) d⁴x, the Einstein–Hilbert sector is the weighted sum ∑_x vol x · (m_p²/2) R x of the curvature R against the invariant volume element.
Formalization Note The finite configuration space is the discrete stand-in for the continuum of fields below the cutoff Λ; the finite spacetime with volume weights stands in for the invariant measure √(-g) d⁴x. The Planck mass m_p and the curvature field R are explicit real parameters; no metric or smoothness structure is claimed.
import Mathlib
open scoped BigOperators
namespace Everyday
/-- The amplitude to undergo a transition between two configurations in
the path-integral formalism of the source equation, on a finite
configuration space: the sum over configurations of the phase
exp(i S c). The source integrates over all fields with momenta below
the ultraviolet cutoff Λ; the finite configuration space is the exact
discrete stand-in for that domain of integration. -/
noncomputable def amplitude {C : Type} [Fintype C] (S : C → ℝ) : ℂ :=
∑ c, Complex.exp (Complex.I * (S c : ℂ))
/-- The gravity sector of the source equation: the Einstein–Hilbert
term (m_p²/2) R integrated against the invariant volume element. The
discrete spacetime is a finite set X of points with volume weights vol
standing in for the measure √(-g) d⁴x, and R is the curvature assigned
to each point. -/
noncomputable def gravSum {X : Type} [Fintype X] (vol : X → ℝ) (mp : ℝ) (R : X → ℝ) : ℝ :=
∑ x, vol x * (mp ^ 2 / 2 * R x)
end Everyday
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The code defines, inside a namespace Everyday, two items. First, amplitude, a noncomputable function: given a type C equipped with the structure of a finite type, and a function S assigning a real number to each element of C, it returns a complex number — the sum over all elements c of C of the complex exponential of (the imaginary unit times the coercion of the real number S c to the complex numbers). Second, gravSum, also a noncomputable function: given a type X equipped with the structure of a finite type, a function vol assigning a real number to each element of X, a real number mp, and a function R assigning a real number to each element of X, it returns the sum over all elements x of X of the product of vol x and (mp squared, divided by two, times R x) — a real number. No hypotheses are attached to either definition; both are total.