def definition def or abbrev

`totalCost`

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

formal statement (Lean)

  91noncomputable def totalCost (L : Ledger) : ℝ :=

Definition body.

  92  (L.entries.map (·.cost)).sum
  93
  94/-- Empty ledger has zero balance. -/

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

totalCost in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
costDensity in IndisputableMonolith.Cosmology.DarkEnergy decl_use
isBalanced in IndisputableMonolith.Cosmology.DarkEnergy decl_use
SpacetimeRegion in IndisputableMonolith.Cosmology.DarkEnergy decl_use
SMLagrangianCert in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton decl_use
totalCost in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton decl_use
totalCost_nonneg in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton decl_use
totalCost_zero_at_vacuum in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton decl_use
born_rule_jcost_connection in IndisputableMonolith.Foundation.QuantumLedger decl_use
empty_ledger_cost in IndisputableMonolith.Foundation.QuantumLedger decl_use
expectedCost in IndisputableMonolith.Foundation.QuantumLedger decl_use
ledger_cost_additive in IndisputableMonolith.Foundation.QuantumLedger decl_use

Lean names referenced from this declaration's body.

totalCost in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
totalCost in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use