The Lean 4 theorem `qg3DElliptic_friedrichs_extension` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalization

Proved

BookProof.QuantumGravity3DGauge.qg3DElliptic_friedrichs_extension

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

timepiece

The Lean 4 theorem qg3DElliptic_friedrichs_extension in the ChapterQuantumGravity3DGauge chapter of the timepiece formalization.

Preamble

-- Generated from ChapterQuantumGravity3DGauge.lean — theorem BookProof.QuantumGravity3DGauge.qg3DElliptic_friedrichs_extension
import Mathlib
import Definitions.Def_ChapterQuantumGravity3DGauge
open BookProof.QuantumGravity3DGauge



open MeasureTheory Complex MvPolynomial Filter Topology
open BookProof.HermiteProductCore BookProof.YangMillsHermite BookProof.YangMillsFriedrichs
open BookProof.FarisLavine BookProof.FriedrichsExtension BookProof.HermiteGalerkin
open BookProof.HashimotoShiftInvert BookProof.QuantumGravityDensitized

noncomputable section

Formal statement

theorem BookProof.QuantumGravity3DGauge.qg3DElliptic_friedrichs_extension :
    ∃ (Dom : Submodule ℂ (L2d 84)) (A : Dom →ₗ[ℂ] L2d 84),
      IsPositiveSelfAdjointExtension (qg3DEllipticHamiltonian (coreRepPoly 84)) A := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterQuantumGravity3DGauge.lean

View graph