`BookProof.ChapterGaugeWeylResidual.remnant_moves_every_configuration` : ∃ θ : ℝ → ℝ → ℝ, TimeIndependent θ ∧ (∀ t x, dt θ t x = 0) ∧ (∀ t x, dx θ t x = 1) ∧ ∀ A1 :...

Proved

BookProof.ChapterGaugeWeylResidual.remnant_moves_every_configuration

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeWeylResidual.

BookProof.ChapterGaugeWeylResidual.remnant_moves_every_configuration : ∃ θ : ℝ → ℝ → ℝ, TimeIndependent θ ∧ (∀ t x, dt θ t x = 0) ∧ (∀ t x, dx θ t x = 1) ∧ ∀ A1 : ℝ → ℝ → ℝ, gaugeA1 θ A1 ≠ A1

Formalization note: Lean 4 identifier BookProof.ChapterGaugeWeylResidual.remnant_moves_every_configuration.

Preamble

-- Generated from ChapterGaugeWeylResidual.lean — theorem BookProof.ChapterGaugeWeylResidual.remnant_moves_every_configuration
import Mathlib
import Definitions.Def_ChapterGaugeWeylResidual
open BookProof.ChapterGaugeWeylResidual

Formal statement

theorem BookProof.ChapterGaugeWeylResidual.remnant_moves_every_configuration :
    ∃ θ : ℝ → ℝ → ℝ, TimeIndependent θ ∧ (∀ t x, dt θ t x = 0) ∧
      (∀ t x, dx θ t x = 1) ∧ ∀ A1 : ℝ → ℝ → ℝ, gaugeA1 θ A1 ≠ A1 := by sorry

View graph