transformGaugeField
plain-language theorem explainer
Gauge transformation of the gauge field adds a supplied gradient to each of the four components of A at every point x. Researchers deriving U(1) symmetry from ledger redundancy in Recognition Science cite this when showing that phase choices leave observables unchanged. The definition is a direct record constructor performing componentwise addition.
Claim. Given a gauge field with components $A_μ(x)$ for $μ=0,1,2,3$, the transformed field is defined by $A'_μ(x) = A_μ(x) + ∂_μ θ(x)$, where the four partial-derivative maps are supplied explicitly as the gradient argument.
background
The QFT.GaugeInvariance module derives gauge symmetry from ledger redundancy: distinct phase encodings of the same physical state are physically equivalent. GaugeField is the structure whose components map Fin 4 to functions X → ℝ, representing the connection 1-form whose standard shift is A_μ → A_μ + ∂_μ θ. Upstream results supply the 8-tick phases (periodic with period 2π) and the active-edge count A = 1 that fix the fundamental tick structure used throughout the ledger.
proof idea
One-line wrapper that constructs a fresh GaugeField record whose components map is the pointwise sum of the input components and the supplied gradient.
why it matters
This supplies the explicit transformation rule required to realize U(1) gauge symmetry inside the Recognition Science ledger. It directly implements the module target of obtaining gauge invariance from information redundancy and feeds the sibling constructions U1Transform, localGauge and physical_equiv_symm. The definition closes the concrete step between the abstract ledger redundancy claim and the standard gauge-shift formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.