Chapter GaugeAdjointAlgebra

import Mathlib

/-
Copyright (c) 2026. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aristotle
-/

/-!
# The gauge algebra, the Gauss law and the gauge invariance of the Weyl Hamiltonian

Source: `book.tex`, chapter *"Timepiece and the Gribov ambiguity"*,
§*"Pure Yang–Mills theory"* (lines 7290–7400) and the parallel Yang–Mills
chapter (lines 7020–7120).  The manuscript writes the 3D Hamiltonian in the
Weyl gauge

```
H_W = ½ π^i_a π^i_a + ½ B_{i a} B_{i a},
```

states that it *"is invariant under a remnant gauge symmetry generated by
`θ_a (D_i π^i)_a`"* — the **Gauss law** — and that it is *positive definite*.

This file formalizes the algebraic content of those statements, with the
coordinates representing spatial derivatives of the fields kept as **independent
variables** (`dA`, `dX`, `dθ`), exactly as everywhere else in this development.
The gauge algebra is an arbitrary real Lie algebra `L` (so `su(3)`, `su(2)` and
`u(1)` are all instances), and the gauge-invariant inner product `κ` (Killing
form, trace form, …) is an arbitrary invariant symmetric bilinear form.

## Main results

* `adj_closure` — the infinitesimal gauge transformations close on the adjoint
  fields: `[δ_θ, δ_η] = δ_{⁅θ,η⁆}`, i.e. `θ ↦ δ_θ` is a representation of the
  gauge algebra (this is the Jacobi identity).
* `covariantDeriv_covariant` — the covariant derivative `D_i X = ∂_i X + ⁅A_i, X⁆`
  transforms in the adjoint representation, *provided* the derivative
  coordinates obey the Leibniz gauge-fixing rule
  `δ(∂_i X) = ⁅∂_i X, θ⁆ + ⁅X, ∂_i θ⁆`.
* `gaussLaw_covariant`, `gaussLaw_constraint_surface_invariant` — the Gauss-law
  generator transforms in the adjoint, hence the constraint surface `G = 0` is
  preserved by the (remnant) gauge group.
* `magnetic_covariant` — the magnetic field `B_{ij} = ∂_i A_j − ∂_j A_i + ⁅A_i, A_j⁆`
  transforms in the adjoint under a *local* gauge transformation
  `δ A_i = ∂_i θ + ⁅A_i, θ⁆` (the inhomogeneous terms cancel by the symmetry of
  the second-derivative coordinates).
* `weylEnergy_gauge_invariant` — the Weyl-gauge energy `½π² + ½B²` has vanishing
  gauge variation.
* `weylEnergy_nonneg` — and it is non-negative for a positive semidefinite
  invariant form, which is the book's *"positive definite in the Weyl gauge"*.
-/

namespace BookProof.ChapterGaugeAdjointAlgebra

open Finset

variable {L : Type*} [LieRing L]

/-! ## The Jacobi identity in the form used throughout -/



/-! ## The infinitesimal gauge transformation of an adjoint field -/

/-- The infinitesimal gauge variation of a field transforming in the adjoint
representation: `δ_θ X = ⁅X, θ⁆`. -/
def adjVar (θ X : L) : L := ⁅X, θ⁆







/-! ## Covariant derivative and the Gauss law -/

/-- The covariant derivative in the independent derivative coordinates:
`D_i X = (∂_i X) + ⁅A_i, X⁆`, where `dX i` is the coordinate representing
`∂_i X`. -/
def covariantDeriv (A dX : Fin 3 → L) (X : L) (i : Fin 3) : L := dX i + ⁅A i, X⁆

/-- The local (inhomogeneous) gauge variation of the gauge field:
`δ A_i = ∂_i θ + ⁅A_i, θ⁆`. -/
def gaugeVarA (A dθ : Fin 3 → L) (θ : L) (i : Fin 3) : L := dθ i + ⁅A i, θ⁆



/-- The Gauss-law generator `G = Σ_i D_i π^i` of the Weyl gauge (book 7364). -/
def gaussLaw (A dπ π : Fin 3 → L) : L := ∑ i, (dπ i + ⁅A i, π i⁆)





/-! ## The magnetic field and the Weyl Hamiltonian -/

/-- The non-abelian magnetic field in the independent derivative coordinates:
`B_{ij} = ∂_i A_j − ∂_j A_i + ⁅A_i, A_j⁆`. -/
def magnetic (A : Fin 3 → L) (dA : Fin 3 → Fin 3 → L) (i j : Fin 3) : L :=
  dA i j - dA j i + ⁅A i, A j⁆



/-! ## The Weyl-gauge energy -/

/-- The Weyl-gauge energy `½ Σ_i κ(π_i, π_i) + ¼ Σ_{i,j} κ(B_{ij}, B_{ij})`
for an invariant symmetric form `κ` on the gauge algebra. -/
noncomputable def weylEnergy {M : Type*} (κ : M → M → ℝ) (π : Fin 3 → M)
    (B : Fin 3 → Fin 3 → M) : ℝ :=
  (1 / 2) * ∑ i, κ (π i) (π i) + (1 / 4) * ∑ i, ∑ j, κ (B i j) (B i j)







end BookProof.ChapterGaugeAdjointAlgebra