`BookProof.QuantumGravityFock.qgGradedFock_stone_flow` (omega g : ℕ → ℝ) : ∃ (T : UnboundedSelfAdjoint (lp (fun _ : GradedIdx => ℂ) 2)) (U : ℝ → (lp (fun _ : GradedIdx => ℂ) 2 →L[ℂ

Proved

BookProof.QuantumGravityFock.qgGradedFock_stone_flow

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterQuantumGravityFock.

BookProof.QuantumGravityFock.qgGradedFock_stone_flow (omega g : ℕ → ℝ) : ∃ (T : UnboundedSelfAdjoint (lp (fun _ : GradedIdx => ℂ) 2)) (U : ℝ → (lp (fun _ : GradedIdx => ℂ) 2 →L[ℂ] lp (fun _ : GradedIdx => ℂ) 2)), IsSelfAdjointExtension ((lpFiniteModes GradedIdx).subtype.comp (qgGradedHam omega g)) T.op ∧ IsStoneFlow T U

Formalization note: Lean 4 identifier BookProof.QuantumGravityFock.qgGradedFock_stone_flow.

Preamble

-- Generated from ChapterQuantumGravityFock.lean — theorem BookProof.QuantumGravityFock.qgGradedFock_stone_flow
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
import Definitions.Def_ChapterNavierStokesIkebeKato
import Definitions.Def_ChapterNavierStokesFockSpace
import Definitions.Def_ChapterNavierStokesFullEsa
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterSirkTrotterKato
import Definitions.Def_ChapterYangMillsFriedrichs
import Definitions.Def_ChapterHermiteGalerkinFriedrichs
import Definitions.Def_ChapterComplexShiftCore
import Definitions.Def_ChapterFockSecondQuantization
import Mathlib
import Definitions.Def_ChapterQuantumGravityFock
import Definitions.Def_ChapterEsaClosureCore
import Definitions.Def_ChapterNavierStokesEsa
import Definitions.Def_ChapterStoneBridge
import Definitions.Def_ChapterStoneResolvent
open BookProof.EsaClosure
open BookProof.StoneBridge
open BookProof.QuantumGravityFock



open BookProof.NavierStokesFlow BookProof.NavierStokesFlow.IkebeKato
open BookProof.NavierStokesFlow.FockOfFock BookProof.NavierStokesFlow.FullEsa
open BookProof.FarisLavine BookProof.StoneBridge BookProof.EsaClosure
open BookProof.ChapterStoneResolvent BookProof.YangMillsFriedrichs
open BookProof.HermiteGalerkin BookProof.HashimotoShiftInvert
open BookProof.FockSecondQuantization

noncomputable section

Formal statement

theorem BookProof.QuantumGravityFock.qgGradedFock_stone_flow (omega g : ℕ → ℝ) :
    ∃ (T : UnboundedSelfAdjoint (lp (fun _ : GradedIdx => ℂ) 2))
      (U : ℝ → (lp (fun _ : GradedIdx => ℂ) 2 →L[ℂ] lp (fun _ : GradedIdx => ℂ) 2)),
      IsSelfAdjointExtension
        ((lpFiniteModes GradedIdx).subtype.comp (qgGradedHam omega g)) T.op ∧ IsStoneFlow T U := by sorry

View graph