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

Proved

BookProof.Qg3DGaugeEsa.torsionOps_eq

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

timepiece

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

Preamble

-- Generated from ChapterQg3DGaugeEsa.lean — theorem BookProof.Qg3DGaugeEsa.torsionOps_eq
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.torsionOps_eq {D : Submodule ℂ (L2d 84)} (Φ : CoreRep 84 D) (m : Fin 64) :
    torsionOps Φ m = Φ.op (mulOp (torsionP m)) := by sorry

Source

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

View graph