Foundation Ledger Floor T0 Bridge Ledger Add Eq Zero Iff

The ledger's zero rule

A ledger, in the Recognition Science framework, is a discrete record of recognition events. Each possible kind of event gets a natural-number count, so a ledger is a function from event types to nonnegative integers. The theorem ledger_add_eq_zero_iff states a plain fact about adding two such ledgers: their sum is the zero ledger if and only if each summand is itself zero. In symbols, Γ + Δ = 0 ↔ Γ = 0 ∧ Δ = 0. Since the counts are natural numbers, there are no negative entries to cancel a posting; a nonzero entry in either summand survives in the sum.

The theorem belongs to a larger construction, the LedgerFloorT0Bridge, which connects the ledger to a coarser two-state object called the T0 floor. The floor records only whether any recognition has happened at all: false on the empty ledger, true as soon as any event is posted. The bridge proves that this two-state shadow is a genuine quotient of the ledger, not an unrelated choice. The zero rule is what makes the quotient well-behaved: two ledgers share the same shadow exactly when they agree on having zero cost, and the floor's consistency predicate is precisely "the ledger is costless."

In plain terms, the theorem guarantees that the coarse two-state view does not lose information about emptiness. If the floor says "something happened," then at least one of the underlying ledgers genuinely had an event; if both were empty, the floor says "nothing happened." This is the kernel identification that lets the framework treat the T0 floor as the forced shadow of the extensive ledger rather than a separate primitive notion.

What the theorem does not claim is equally important. It says nothing about the numerical cost of recognition, only about the zero/nonzero distinction. A ledger with one event and a ledger with a million events both map to the same floor state. The theorem also does not establish the bridge itself; it is one lemma inside a bundled structure that also proves surjectivity, cost truncation, and the homomorphism property. The bridge as a whole is a theorem, but this particular declaration is only the zero-rule component.

/-- The free ledger is `0` exactly when both summands are `0`: in `I →₀ ℕ` there
are no negative entries to cancel a posting. -/
theorem ledger_add_eq_zero_iff {I : Type v} {Γ Δ : DefectLedger I} :
    Γ + Δ = 0 ↔ Γ = 0 ∧ Δ = 0 := by
  constructor
  · intro hsum
    refine ⟨?_, ?_⟩ <;> ext i
    · have hi : Γ i + Δ i = 0 := by
        have := congrArg (fun f : DefectLedger I => f i) hsum
        simpa [Finsupp.add_apply] using this
      have : Γ i = 0 := by omega
      simpa using this
    · have hi : Γ i + Δ i = 0 := by
        have := congrArg (fun f : DefectLedger I => f i) hsum
        simpa [Finsupp.add_apply] using this
      have : Δ i = 0 := by omega
      simpa using this
  · rintro ⟨h1, h2⟩; rw [h1, h2, add_zero]

theorem ledgerShadow_eq_false_iff {I : Type v} {Γ : DefectLedger I} :
    ledgerShadow Γ = false ↔ Γ = 0 := by
  unfold ledgerShadow
  by_cases hΓ : Γ = 0 <;> simp [hΓ]

What this page does not claim

The theorem does not establish the full LedgerFloorT0Bridge, only the zero-rule component. It does not say anything about the numerical magnitude of recognition cost, only about zero versus nonzero. It does not claim that the ledger itself is the T0 floor, only that the floor is its two-state shadow.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: