structure definition def or abbrev

`Ledger`

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

formal statement (Lean)

  82structure Ledger where
  83  /-- The entries in the ledger -/
  84  entries : List LedgerEntry
  85  /-- Total balance (sum of log-ratios) -/
  86  balance : ℝ
  87  /-- Balance equals sum of log-ratios -/
  88  balance_eq : balance = (entries.map (fun e => Real.log e.ratio)).sum
  89
  90/-- The total J-cost of a ledger. -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
LedgerEntry in IndisputableMonolith.Foundation.QuantumLedger decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use
LedgerEntry in IndisputableMonolith.QFT.CPTInvariance decl_use