FieldConfig
plain-language theorem explainer
FieldConfig defines a field configuration as a map from spacetime points to complex ledger values. QFT researchers deriving gauge symmetry from information redundancy would cite it as the base object before introducing U(1) transformations. The declaration is a direct type abbreviation with no further computation or proof steps.
Claim. A field configuration on spacetime manifold $X$ is a function $ψ: X → ℂ$ assigning a complex ledger value to each point.
background
The QFT.GaugeInvariance module derives gauge invariance from ledger redundancy in Recognition Science: distinct ledger representations can encode identical physical states, so the freedom to switch among them is gauge symmetry. FieldConfig supplies the basic object for this construction. Upstream, the phase definition from EightTick supplies the eight discrete phases $kπ/4$ for $k=0..7$, while the phase definition from the RiemannHypothesis.Wedge module supplies the unimodular complex number $e^{i w}$.
proof idea
Direct definition: FieldConfig is introduced as the function type $X → ℂ$ with no lemmas or tactics applied.
why it matters
FieldConfig is the input type for both globalGauge and localGauge, the two transformations that realize the module's core claim that gauge symmetry originates in ledger equivalence. It therefore sits at the start of the chain that converts the eight-tick phase structure into U(1) gauge freedom and, ultimately, into the introduction of gauge fields for local transformations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.