structure definition def or abbrev

`LedgerPage`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  82structure LedgerPage where
  83  /-- The events on this page -/
  84  events : List LedgerEvent
  85  /-- The balance: sum of all flows -/
  86  balance : ℤ := events.foldl (fun acc e => acc + e.flow) 0

proof body

Definition body.

  87
  88/-- Compute the balance of a list of events. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IsBalanced in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
paired_preserves_balance in IndisputableMonolith.Algebra.LedgerAlgebra decl_use

depends on (10)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
LedgerEvent in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use