Chapter GaugeWeylResidual

import Mathlib

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

/-!
# The Weyl gauge is an incomplete gauge fixing: the remnant is the time-independent subgroup

Source: `book.tex`, §*"Pure Yang–Mills theory"* of the chapter *"Timepiece and
the Gribov ambiguity"* (lines 7364–7375) and the same statement in the
Yang–Mills chapter (lines 7106–7112):

> "Since the Weyl gauge is an incomplete gauge-fixing, this new Hamiltonian
> `H_W` is invariant under a remnant gauge symmetry generated by
> `θ_a (D_i π^i)_a`, where the function `θ` is constant in time."

and the definition of a *complete* gauge fixing (line 2294): a gauge fixing is
complete when it crosses each gauge orbit at most once, i.e. when no non-trivial
gauge transformation preserves the gauge-fixing surface.

This file proves both halves of the manuscript's claim for the (abelian model
of the) Weyl gauge `A₀ = 0`, in `1 + 1` dimensions, where a gauge parameter is a
function `θ : ℝ → ℝ → ℝ` of time and space acting by

```
A₀ ↦ A₀ + ∂_t θ,     A₁ ↦ A₁ + ∂_x θ.
```

## Main results

* `weyl_residual_iff_time_independent` — a gauge transformation preserves the
  Weyl surface `A₀ = 0` **iff** its parameter is constant in time: the remnant
  gauge group is exactly the time-independent subgroup, as the book states.
* `remnant_moves_every_configuration` — the remnant acts non-trivially (indeed
  freely) on the spatial gauge field: there is a time-independent `θ` that moves
  *every* configuration `A₁`.
* `weyl_gauge_fixing_incomplete` — hence the Weyl gauge fixing crosses a gauge
  orbit more than once: two distinct configurations of the Weyl surface are
  gauge equivalent, so the gauge fixing is **not complete**.
* `weyl_surface_preserved_by_remnant` — conversely the remnant really does map
  the Weyl surface to itself, so it is a symmetry of the gauge-fixed theory.
-/

namespace BookProof.ChapterGaugeWeylResidual

/-- The coordinate representing the time derivative `∂_t θ` of a gauge
parameter. -/
noncomputable def dt (θ : ℝ → ℝ → ℝ) (t x : ℝ) : ℝ := deriv (fun s => θ s x) t

/-- The coordinate representing the space derivative `∂_x θ` of a gauge
parameter. -/
noncomputable def dx (θ : ℝ → ℝ → ℝ) (t x : ℝ) : ℝ := deriv (fun y => θ t y) x

/-- The gauge transformation of the temporal component: `A₀ ↦ A₀ + ∂_t θ`. -/
noncomputable def gaugeA0 (θ A0 : ℝ → ℝ → ℝ) : ℝ → ℝ → ℝ :=
  fun t x => A0 t x + dt θ t x

/-- The gauge transformation of the spatial component: `A₁ ↦ A₁ + ∂_x θ`. -/
noncomputable def gaugeA1 (θ A1 : ℝ → ℝ → ℝ) : ℝ → ℝ → ℝ :=
  fun t x => A1 t x + dx θ t x

/-- A gauge parameter is *time-independent* — the book's "constant in time" —
when its value does not depend on the time argument. -/
def TimeIndependent (θ : ℝ → ℝ → ℝ) : Prop := ∀ t s x, θ t x = θ s x









end BookProof.ChapterGaugeWeylResidual