`BookProof.ChapterGaugeWeylResidual.weyl_gauge_fixing_incomplete` : ∃ (θ : ℝ → ℝ → ℝ) (A1 : ℝ → ℝ → ℝ), TimeIndependent θ ∧ (∀ t x, dt θ t x = 0) ∧ gaugeA0 θ (fun...

Proved

BookProof.ChapterGaugeWeylResidual.weyl_gauge_fixing_incomplete

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeWeylResidual.

BookProof.ChapterGaugeWeylResidual.weyl_gauge_fixing_incomplete : ∃ (θ : ℝ → ℝ → ℝ) (A1 : ℝ → ℝ → ℝ), TimeIndependent θ ∧ (∀ t x, dt θ t x = 0) ∧ gaugeA0 θ (fun _ _ => 0) = (fun _ _ => 0) ∧ gaugeA1 θ A1 ≠ A1

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

Preamble

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

Formal statement

theorem BookProof.ChapterGaugeWeylResidual.weyl_gauge_fixing_incomplete :
    ∃ (θ : ℝ → ℝ → ℝ) (A1 : ℝ → ℝ → ℝ),
      TimeIndependent θ ∧ (∀ t x, dt θ t x = 0) ∧
        gaugeA0 θ (fun _ _ => 0) = (fun _ _ => 0) ∧ gaugeA1 θ A1 ≠ A1 := by sorry

View graph