The Lean 4 theorem `qgKappa_conformal_neg` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalization
ProvedBookProof.QuantumGravity3DGauge.qgKappa_conformal_negtimepiece
The Lean 4 theorem qgKappa_conformal_neg in the ChapterQuantumGravity3DGauge chapter of the timepiece formalization.
Preamble
-- Generated from ChapterQuantumGravity3DGauge.lean — theorem BookProof.QuantumGravity3DGauge.qgKappa_conformal_neg 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.qgKappa_conformal_neg : qgKappa confIndex < 0 := by sorry
Source