`add_event`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LedgerForcing on GitHub at line 324.

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

used by

formal source

 321  ring
 322
 323/-- Add an event and its reciprocal to a ledger. -/
 324noncomputable def add_event (L : Ledger) (e : RecognitionEvent) : Ledger := {
 325  events := e :: reciprocal e :: L.events
 326  double_entry := add_event_balanced_list L.events L.double_entry e
 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

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