GaugeField
plain-language theorem explainer
GaugeField defines a gauge field on a space X as a structure whose sole field assigns four real-valued component functions indexed by Fin 4. Researchers deriving gauge symmetry from ledger redundancy in Recognition Science cite this definition to formalize the connection 1-form before stating transformation rules. The declaration is a direct structure definition with no proof obligations or computational content.
Claim. A gauge field on a space $X$ consists of four component maps $A_0, A_1, A_2, A_3 : X → ℝ$, one for each spacetime dimension.
background
The QFT.GaugeInvariance module derives gauge invariance from ledger redundancy: distinct ledger encodings of the same physical configuration are identified, and the freedom to switch among them is gauge symmetry. GaugeField supplies the basic object for this construction by packaging the gauge potential as a 4-tuple of real functions, extending the framework's forced D=3 spatial dimensions to 3+1 spacetime. Upstream results supply the logical integer one, the active-edge count A, and the actualization operator A, which furnish the arithmetic primitives used in the Recognition Composition Law and the phi-ladder.
proof idea
This is a structure definition that directly introduces the type GaugeField with the single field components of type Fin 4 → X → ℝ. No lemmas are applied and no tactics are executed; the declaration serves only as the carrier type for the sibling theorems gauge_field_components and transformGaugeField.
why it matters
GaugeField is the foundational type for the two downstream declarations in the same module: gauge_field_components (which extracts the four components) and transformGaugeField (which adds a gradient). It realizes the QFT-008 claim that gauge symmetry originates from ledger redundancy and supplies the concrete object needed to state the U(1) transformation A_μ → A_μ + ∂_μ θ. Within the larger chain it sits after T8 (D=3) and before any explicit gauge-group action, leaving open the question of how the specific groups SU(2) and SU(3) arise from the same redundancy mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.