The Lean 4 theorem `weylProd_self` in the `ChapterQg3DGaugeEsa` chapter of the timepiece formalization

Proved

BookProof.Qg3DGaugeEsa.weylProd_self

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

timepiece

The Lean 4 theorem weylProd_self in the ChapterQg3DGaugeEsa chapter of the timepiece formalization.

Preamble

-- Generated from ChapterQg3DGaugeEsa.lean — theorem BookProof.Qg3DGaugeEsa.weylProd_self
import Mathlib
import Definitions.Def_ChapterQg3DGaugeEsa
open BookProof.Qg3DGaugeEsa



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.StoneBridge BookProof.EsaClosure BookProof.ChapterStoneResolvent

noncomputable section

Formal statement

theorem BookProof.Qg3DGaugeEsa.weylProd_self (S : MvPolynomial (Fin 84) ℂ →ₗ[ℂ] MvPolynomial (Fin 84) ℂ)
    (p : MvPolynomial (Fin 84) ℂ) : weylProd S S p = S (S p) := by sorry

Source

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

View graph