pith. machine review for the scientific record. sign in
theorem

add_event_balanced

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.LedgerForcing
domain
Foundation
line
330 · github
papers citing
1 paper (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LedgerForcing on GitHub at line 330.

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

depends on

formal source

 327}
 328
 329/-- Adding a paired event preserves balance. -/
 330theorem add_event_balanced (L : Ledger) (e : RecognitionEvent) :
 331    balanced (add_event L e) := (add_event L e).double_entry
 332
 333/-! ## Ledger Forcing Principle -/
 334
 335/-- **LEDGER FORCING PRINCIPLE**
 336
 337The cost landscape forces ledger structure:
 338
 3391. d'Alembert → J unique → J(x) = J(1/x) (symmetry)
 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 (showing 1 of 1)