Least Action Principle

Variational calculus on the Fζ Lagrangian |Fζ f|². Time evolution equivariance (TimeStructure.lagrangian_phi_equivariant) ensures |Fζ f|² is a true Lagrangian, and δL = 0 ⟹ f ∈ ker(Fζ).

Variational Structure

Fζ is linear, so L[f] = |Fζ f|² admits standard first variation. δL = 0 for all test η implies Fζ f = 0, i.e. f ∈ ker(Fζ).

theorem FUST.LeastAction.Fζ_linear_combination (f g : ℂ → ℂ) (a b z : ℂ) : FζOperator.Fζ (fun (t : ℂ) => a * f t + b * g t) z = a * FζOperator.Fζ f z + b * FζOperator.Fζ g z

theorem FUST.LeastAction.Fζ_additive (f g : ℂ → ℂ) (z : ℂ) : FζOperator.Fζ (fun (t : ℂ) => f t + g t) z = FζOperator.Fζ f z + FζOperator.Fζ g z

theorem FUST.LeastAction.lagrangian_perturbation (f η : ℂ → ℂ) (ε z : ℂ) : TimeStructure.FζLagrangian (fun (t : ℂ) => f t + ε * η t) z = Complex.normSq (FζOperator.Fζ f z) + 2 * (ε * FζOperator.Fζ η z * (starRingEnd ℂ) (FζOperator.Fζ f z)).re + Complex.normSq ε * Complex.normSq (FζOperator.Fζ η z)

First variation: L[f+εη] = L[f] + 2Re(ε·Fζη·conj(Fζf)) + O(ε²)

theorem FUST.LeastAction.critical_point_of_witness (f : ℂ → ℂ) (z : ℂ) (h_witness : ∃ (η : ℂ → ℂ), FζOperator.Fζ η z ≠ 0) : (∀ (η : ℂ → ℂ), FζOperator.Fζ f z * FζOperator.Fζ η z = 0) → FζOperator.Fζ f z = 0

Critical point: if a nontrivial test variation exists, δL = 0 implies Fζ f = 0