The everyday equation's amplitude is a phase: the assembled action is real, so exp(iS) has modulus one
ProvedEveryday.everyday_phaseThe source equation's claim, in one line: the everyday world's dynamics is a single action functional — spacetime, gravity, the other forces, matter, and the Higgs sector, each a labeled part of the integrand — whose exponential of i times itself gives the transition amplitude. The item is the goal theorem of the mission, the equation's quantum-mechanical heart: assemble the four labeled sectors into the action of a configuration of the discrete arena; the assembled action is a real number — the gravity, gauge, and Higgs sectors are real-valued, and the matter sector's Yukawa term plus its hermitian conjugate is real — so the exponential of i times the action has modulus exactly one. The everyday equation generates phases, not probabilities: probability enters only through the coherent sum of such phases.
Formalization Note The assembled action omits the fermion kinetic and Higgs kinetic terms, as the definition discloses; their realness is structurally identical to the assembled sectors'. The quartic coupling λ of the Higgs potential is bound as lam in the formal statement, λ being a reserved keyword in Lean 4. The proof: the action's imaginary part vanishes — the three real-valued sectors contribute zero imaginary part by their coercions, and the matter sector's by the yukawa_real milestone — so the real part of i times the action is zero, and the modulus of the exponential is the exponential of zero, which is one.
import Mathlib import Definitions.Def_Everyday_spacetime import Definitions.Def_Everyday_sectors
namespace Everyday
/-- The everyday equation's amplitude is a phase: assemble the four
labeled sectors — gravity, the other forces, matter (the Yukawa term
plus its hermitian conjugate), and the Higgs potential — into the action
of a configuration; the action is real, so the exponential of i times it
has modulus exactly one. This is the quantum-mechanical heart of the
source equation: the everyday world's dynamics is one real functional
whose exponentiation gives the transition amplitude. -/
theorem everyday_phase {X : Type} [Fintype X] (vol : X → ℝ) (w : X → X → X → ℝ)
(mp : ℝ) (R : X → ℝ) (A : X → X → ℝ) (ψL ψR : X → ℂ) (V : ℂ) (Φh : X → ℂ)
(μ lam : ℝ) :
‖Complex.exp
(Complex.I * everydayAction vol w mp R A ψL ψR V Φh μ lam)‖ = 1 := 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, volume weights vol, triangle weights w, a real number mp, a curvature function R, a gauge field A on the ordered pairs of X, complex fermion fields ψL and ψR, a complex coupling V, a complex Higgs field Φh, and real numbers μ and lam, the complex norm of the complex exponential of (the imaginary unit times everydayAction vol w mp R A ψL ψR V Φh μ lam) equals one. Unfolding, the action is the complex sum of the gravity sector sum, minus one quarter of the gauge functional, the Yukawa term plus its complex conjugate, and the negated Higgs potential sum; and the norm of the exponential is the real exponential of the real part of its argument. The conclusion is an equation between a nonnegative real number and one.