Resolution of the identity into the two occupation sectors: `N + ψ ψ† = 1`, i.e

Proved

BookProof.NavierStokes.ghostNumber_resolution

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

ghostsnavier-stokestimepiece

Resolution of the identity into the two occupation sectors: N + ψ ψ† = 1, i.e. ψ† ψ + ψ ψ† = 1 (the CAR restated with the number operator).

Formalization Note. Lean 4 identifier: BookProof.NavierStokes.ghostNumber_resolution (module BookProof.NavierStokes), line-linked source: ChapterNavierStokes.lean lines 134–138.

Preamble

-- Generated from ChapterNavierStokes.lean — theorem BookProof.NavierStokes.ghostNumber_resolution
import Mathlib
import Definitions.Def_ChapterNavierStokes
open BookProof.NavierStokes












open Matrix

Formal statement

theorem BookProof.NavierStokes.ghostNumber_resolution : ghostNumber + ghostAnnih * ghostCreate = 1 := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterNavierStokes.lean#L134-L138

View graph