`BookProof.ScalaronDensitized.physConf_stone_flow` : ∃ (T : UnboundedSelfAdjoint (Lp ℂ 2 physMeasure)) (U : ℝ → (Lp ℂ 2 physMeasure →L[ℂ] Lp ℂ 2 physMeasure)), IsSelfAdjointExtensi

Proved

BookProof.ScalaronDensitized.physConf_stone_flow

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterScalaronDensitizedTransfer.

BookProof.ScalaronDensitized.physConf_stone_flow : ∃ (T : UnboundedSelfAdjoint (Lp ℂ 2 physMeasure)) (U : ℝ → (Lp ℂ 2 physMeasure →L[ℂ] Lp ℂ 2 physMeasure)), IsSelfAdjointExtension ((physConfCore M alpha).subtype.comp (physConfOp M alpha)) T.op ∧ IsStoneFlow T U

Formalization note: Lean 4 identifier BookProof.ScalaronDensitized.physConf_stone_flow.

Preamble

-- Generated from ChapterScalaronDensitizedTransfer.lean — theorem BookProof.ScalaronDensitized.physConf_stone_flow
import Definitions.Def_ChapterStarobinskyPotential
import Definitions.Def_ChapterQuantumGravityDensitized
import Definitions.Def_ChapterQuantumGravityHalfDensity
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
import Definitions.Def_ChapterNavierStokesFockContinuum
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterSirkTrotterKato
import Mathlib
import Definitions.Def_ChapterScalaronDensitizedTransfer
import Definitions.Def_ChapterEsaClosureCore
import Definitions.Def_ChapterStoneBridge
import Definitions.Def_ChapterStoneResolvent
open BookProof.EsaClosure
open BookProof.StoneBridge
open BookProof.ScalaronDensitized



open MeasureTheory Set Filter Topology
open BookProof.Starobinsky BookProof.QuantumGravityDensitized
open BookProof.QuantumGravityHalfDensity
open BookProof.NavierStokesFlow BookProof.NavierStokesFlow.FockContinuum
open BookProof.FarisLavine BookProof.StoneBridge
open BookProof.ChapterStoneResolvent BookProof.EsaClosure

noncomputable section

variable (M alpha : ℝ)
variable {X : Type*} [MeasurableSpace X]

Formal statement

theorem BookProof.ScalaronDensitized.physConf_stone_flow :
    ∃ (T : UnboundedSelfAdjoint (Lp ℂ 2 physMeasure))
      (U : ℝ → (Lp ℂ 2 physMeasure →L[ℂ] Lp ℂ 2 physMeasure)),
      IsSelfAdjointExtension
        ((physConfCore M alpha).subtype.comp (physConfOp M alpha)) T.op ∧ IsStoneFlow T U := by sorry

View graph