`particleCharge`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Ledger
domain: RRF
line: 160 · 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 160.

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

formal source

 157/-- Conservation law from particle-antiparticle pairs. -/
 158inductive ParticlePair | particle | antiparticle
 159
 160def particleCharge : ParticlePair → ℤ
 161  | .particle => 1
 162  | .antiparticle => -1
 163
 164end ConservationLaw
 165
 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

papers checked against this theorem

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