pith. machine review for the scientific record. sign in
structure definition def or abbrev

LedgerEntry

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  60structure LedgerEntry where
  61  /-- Position in 3D space. -/
  62  position : Fin 3 → ℝ
  63  /-- Time (tick number). -/
  64  tick : Phase
  65  /-- Charge/type indicator. -/
  66  charge : ℤ
  67  /-- Cost of this entry. -/
  68  cost : ℝ
  69  /-- Cost is non-negative. -/
  70  cost_nonneg : cost ≥ 0
  71
  72/-- A ledger is a collection of balanced entries. -/

used by (23)

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

depends on (25)

Lean names referenced from this declaration's body.