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

Proved

BookProof.QgOuterFock.sum_reindex_particles

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

timepiece

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

Preamble

-- Generated from ChapterQgOuterFockEsa.lean — theorem BookProof.QgOuterFock.sum_reindex_particles
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.sum_reindex_particles {n : ℕ} {α : Type*} [AddCommMonoid α] (F : Fin (n * 84) → α) :
    ∑ I : Fin (n * 84), F I = ∑ p : Fin n, ∑ j : Fin 84, F (pcoord p j) := by sorry

Source

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

View graph