U1Transform
plain-language theorem explainer
U1Transform encodes the standard U(1) phase rotation on complex field values as multiplication by exp(iθ). Researchers deriving gauge symmetries from Recognition Science ledger redundancy cite this definition when building global and local gauge maps. It is introduced as a direct noncomputable definition using complex arithmetic.
Claim. The map $U_1: ℝ × ℂ → ℂ$ is given by $U_1(θ, z) := z · exp(i θ)$ for real phase θ and complex field value z.
background
The QFT module derives gauge invariance from ledger redundancy: distinct ledger encodings of the same physical state permit phase freedoms that constitute the gauge symmetry. U(1) supplies the elementary Abelian case acting on complex scalars. Upstream, RSNativeUnits.U fixes native units with c = 1 while Recognition.U encodes recognition by structural equality.
proof idea
The definition is supplied directly by the expression z multiplied by the complex exponential of i times θ. No lemmas are invoked; it serves as the primitive operation for subsequent group properties.
why it matters
This definition supplies the basic operation used by globalGauge and localGauge to implement uniform and position-dependent phase shifts on FieldConfig. It underpins the theorems U1_identity, U1_composition, and U1_inverse that establish the group structure. In the Recognition framework it realizes the U(1) gauge symmetry as the simplest case of ledger redundancy, directly supporting the paper target of gauge symmetry from information redundancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.