The Lean 4 theorem `qgOuterCore_dense` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalization

Open

BookProof.QgOuterFock.qgOuterCore_dense

by leonardopedro · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

The Lean 4 theorem qgOuterCore_dense in the ChapterQgOuterFockEsa chapter of the timepiece formalization.

Preamble

-- Generated from ChapterQgOuterFockEsa.lean — theorem BookProof.QgOuterFock.qgOuterCore_dense
import Mathlib
import Definitions.Def_ChapterQgOuterFockEsa
open BookProof.QgOuterFock



open Finset MvPolynomial
open BookProof.HermiteProductCore BookProof.YangMillsHermite
open BookProof.FarisLavine
open BookProof.NavierStokesFlow.DifferentialL2
open BookProof.HermiteRelative
open BookProof.FullQuadratic
open BookProof.QuantumGravity3DGauge
open BookProof.Qg3DGaugeEsa
open BookProof.QgHermiteOscillator
open BookProof.DirectSumEsa
open BookProof.StoneBridge BookProof.EsaClosure BookProof.ChapterStoneResolvent

noncomputable section

Formal statement

theorem BookProof.QgOuterFock.qgOuterCore_dense : Dense ((qgOuterCore : Submodule ℂ qgOuterFock) : Set qgOuterFock) := by sorry

Source

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

View graph