`LedgerDensity`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Ledger
domain: RRF
line: 169 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 169.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 166/-! ## Ledger Density and Mass -/
 167
 168/-- Ledger density at a point (abstract). -/
 169structure LedgerDensity where
 170  /-- Number of transactions per unit volume. -/
 171  density : ℝ
 172  /-- Density is non-negative. -/
 173  nonneg : 0 ≤ density
 174
 175/-- Mass from ledger density (the claim). -/
 176noncomputable def massFromLedger (L : LedgerDensity) (volume : ℝ) : ℝ :=
 177  L.density * volume
 178
 179/-- Curvature from ledger density (the gravity mapping). -/
 180noncomputable def curvatureFromLedger (L : LedgerDensity) : ℝ :=
 181  L.density  -- Placeholder: actual mapping is more complex
 182
 183/-! ## Double-Entry Principle -/
 184
 185/-- The double-entry principle: every credit has a matching debit. -/
 186structure DoubleEntry where
 187  /-- For every credit, there's a corresponding debit. -/
 188  credit_has_debit : ∀ (c : ℤ), c < 0 → ∃ (d : ℤ), d = -c
 189  /-- For every debit, there's a corresponding credit. -/
 190  debit_has_credit : ∀ (d : ℤ), d > 0 → ∃ (c : ℤ), c = -d
 191
 192/-- Double-entry is always satisfied (by construction). -/
 193theorem double_entry_exists : DoubleEntry := {
 194  credit_has_debit := fun c _ => ⟨-c, rfl⟩,
 195  debit_has_credit := fun d _ => ⟨-d, rfl⟩
 196}
 197
 198/-! ## Ledger Algebra Summary -/
 199

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.