`BookProof.ChapterGaugeIncompleteFixing.exists_physical_extension` {S : Set X} (hS : IsComprehensiveGaugeFixing G S) (h : X → ℝ) (hrem : ∀ s ∈ S, ∀ t ∈ S, ∀ g : G, g • s = t → h s
ProvedBookProof.ChapterGaugeIncompleteFixing.exists_physical_extensiontheoremstimepiece
Prove the following Lean 4 theorem from ChapterGaugeIncompleteFixing.
BookProof.ChapterGaugeIncompleteFixing.exists_physical_extension {S : Set X} (hS : IsComprehensiveGaugeFixing G S) (h : X → ℝ) (hrem : ∀ s ∈ S, ∀ t ∈ S, ∀ g : G, g • s = t → h s = h t) : ∃ f : X → ℝ, IsPhysicalObservable G f ∧ ∀ s ∈ S, f s = h s
Formalization note: Lean 4 identifier BookProof.ChapterGaugeIncompleteFixing.exists_physical_extension.
Preamble
-- Generated from ChapterGaugeIncompleteFixing.lean — theorem BookProof.ChapterGaugeIncompleteFixing.exists_physical_extension
import Mathlib
import Definitions.Def_ChapterGaugeIncompleteFixing
open BookProof.ChapterGaugeIncompleteFixing
open scoped InnerProductSpace
variable {X : Type*}
variable (G : Type*) [Group G] [MulAction G X]Formal statement
theorem BookProof.ChapterGaugeIncompleteFixing.exists_physical_extension {S : Set X}
(hS : IsComprehensiveGaugeFixing G S) (h : X → ℝ)
(hrem : ∀ s ∈ S, ∀ t ∈ S, ∀ g : G, g • s = t → h s = h t) :
∃ f : X → ℝ, IsPhysicalObservable G f ∧ ∀ s ∈ S, f s = h s := by sorry