`ledger_forcing_principle`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.LedgerForcing
domain: Foundation
line: 343 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LedgerForcing on GitHub at line 343.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

Derivations using this theorem

Why Reality Posts a Ledger · foundational / THEOREM
Recognition events must close in a conservation-respecting ledger; balance and reciprocity are forced

depends on

formal source

 3402. Symmetry → recognition events come in pairs
 3413. Paired events → double-entry bookkeeping required
 3424. Double-entry → conservation (log-sums cancel) -/
 343theorem ledger_forcing_principle :
 344    (∀ x : ℝ, x ≠ 0 → J x = J (x⁻¹)) ∧
 345    (∀ e : RecognitionEvent, event_cost e = event_cost (reciprocal e)) ∧
 346    (∀ e : RecognitionEvent, Real.log e.ratio + Real.log (reciprocal e).ratio = 0) ∧
 347    (∃ L : Ledger, balanced L ∧ ledger_cost L = 0)
 348  := ⟨fun _ hx => J_symmetric hx, reciprocity, paired_log_sum_zero,
 349     empty_ledger, empty_ledger_balanced, empty_ledger_cost⟩
 350
 351end
 352end LedgerForcing
 353end Foundation
 354end IndisputableMonolith

papers checked against this theorem

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