`BookProof.ChapterGaugeShiftExample.shift_gauge_symmetry_headline` : (∀ m : ℤ, m ≠ 0 → ∀ f : L2Z, f ≠ 0 → shiftOp m f ≠ f) ∧ (¬ ∃ f : L2Z, ‖f‖ = 1 ∧ ∀ m : ℤ,...

Proved

BookProof.ChapterGaugeShiftExample.shift_gauge_symmetry_headline

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeShiftExample.

BookProof.ChapterGaugeShiftExample.shift_gauge_symmetry_headline : (∀ m : ℤ, m ≠ 0 → ∀ f : L2Z, f ≠ 0 → shiftOp m f ≠ f) ∧ (¬ ∃ f : L2Z, ‖f‖ = 1 ∧ ∀ m : ℤ, shiftOp m f = f) ∧ (∀ m n : ℤ, shiftOp m * shiftOp n = shiftOp n * shiftOp m) ∧ (∀ A : L2Z →L[ℂ] L2Z, (∀ m : ℤ, A * shiftOp m = shiftOp m * A) → ∀ (m : ℤ) (f : L2Z), ⟪shiftOp m f, A (shiftOp m f)⟫_ℂ = ⟪f, A f⟫_ℂ)

Formalization note: Lean 4 identifier BookProof.ChapterGaugeShiftExample.shift_gauge_symmetry_headline.

Preamble

-- Generated from ChapterGaugeShiftExample.lean — theorem BookProof.ChapterGaugeShiftExample.shift_gauge_symmetry_headline
import Mathlib
import Definitions.Def_ChapterGaugeShiftExample
import Definitions.Def_ChapterContinuityUnitaryInfinite
open BookProof.ChapterContinuityUnitaryInfinite
open BookProof.ChapterGaugeShiftExample


open scoped InnerProductSpace


open BookProof.ChapterContinuityUnitaryInfinite

Formal statement

theorem BookProof.ChapterGaugeShiftExample.shift_gauge_symmetry_headline :
    (∀ m : ℤ, m ≠ 0 → ∀ f : L2Z, f ≠ 0 → shiftOp m f ≠ f) ∧
    (¬ ∃ f : L2Z, ‖f‖ = 1 ∧ ∀ m : ℤ, shiftOp m f = f) ∧
    (∀ m n : ℤ, shiftOp m * shiftOp n = shiftOp n * shiftOp m) ∧
    (∀ A : L2Z →L[ℂ] L2Z, (∀ m : ℤ, A * shiftOp m = shiftOp m * A) →
      ∀ (m : ℤ) (f : L2Z), ⟪shiftOp m f, A (shiftOp m f)⟫_ℂ = ⟪f, A f⟫_ℂ) := by sorry

View graph