def
definition
massFromLedger
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 176.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
200/-- The complete ledger algebra bundle. -/
201structure LedgerAlgebra where
202 /-- The transaction type. -/
203 transaction : Type := Transaction
204 /-- The ledger type. -/
205 ledger : Type := Ledger
206 /-- Transactions are balanced. -/