inductive
definition
ParticlePair
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 158.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
155}
156
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