Prove2Me

: LedgerWf formatExampleLedger

Proved
BookProof.SirkBandLedger.formatExampleLedger_wf

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

sirkspectral-theorytimepiece

Lean 4 theorem BookProof.SirkBandLedger.formatExampleLedger_wf (module BookProof.SirkBandLedger), source chapter BookProof/ChapterSirkBandLedger.lean.

Preamble
-- Generated from ChapterSirkBandLedger.lean — theorem BookProof.SirkBandLedger.formatExampleLedger_wf
import Mathlib
import Definitions.Def_ChapterSirkBandLedger
open BookProof.SirkBandLedger















open BookProof.SirkCertificateReader
open BookProof.BandEnclosure



































open BookProof.HermiteGalerkin BookProof.YangMillsFriedrichs
open BookProof.YangMillsFriedrichsLimit BookProof.ChapterSirkRitzSpectrum

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]




open BookProof.FarisLavine BookProof.HermiteGalerkin BookProof.YangMillsFriedrichs
open BookProof.HashimotoShiftInvert BookProof.FriedrichsExtension

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]






set_option maxRecDepth 10000
Formal statement
theorem BookProof.SirkBandLedger.formatExampleLedger_wf : LedgerWf formatExampleLedger := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterSirkBandLedger.lean

View graph