pith. machine review for the scientific record. sign in
theorem proved term proof

ledger_forcing_principle

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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,

proof body

Term-mode proof.

 349     empty_ledger, empty_ledger_balanced, empty_ledger_cost⟩
 350
 351end
 352end LedgerForcing
 353end Foundation
 354end IndisputableMonolith

depends on (19)

Lean names referenced from this declaration's body.