Encyclopedia Holography Holography Ledger Owner Map Cut Owner Map Separates Debit Credit

ARTICLE 4 claims 3 theorems 1 model

Holography Ledger Owner Map Cut Owner Map Separates Debit Credit

A ledger that records every transaction can tell you who owns each unit of value, and it can tell debit from credit without ever looking at the proof of the transaction.

Verify this page

The owner map

A ledger is a discrete record of events. In the Recognition Science framework, a ledger is a list of accounts, each holding a number of committed units on the debit side and on the credit side. The owner map is a function built from the ledger alone: it assigns to each committed unit the account and side that own it. The map does this by counting, for each account and side, how many units it holds, and then laying those units out in a fixed order. No information from outside the ledger is needed.

The framework's machine-checked library of formal theorems proves that this owner map separates debit from credit. The theorem, called ownerMap_separates_debit_credit, states that in a nonempty ledger, the owner map assigns different positions to debit units and to credit units. A debit unit and a credit unit of the same account never occupy the same slot in the map. This is not a convention; it is forced by the way the map is defined from the counts. The proof is a theorem in the library, meaning it is checked by a machine and rests only on the framework's three standard axioms.

The separation matters because it lets the ledger recover a transaction from its own states. The framework proves that one legal tick, one step in which a single unit is committed, is an owned boundary extension: the posting, the record of who moved the unit, is recoverable from the owner-map boundary data. Debit and credit produce different boundary functions at the same aperture, the same window of committed units. So the ledger does not need a separate record of intent; the structure of the counts already distinguishes the two sides.

The theorem does not claim that the owner map is a physical quantity. It is a combinatorial fact about the ledger structure. The framework's own notes mark as open the bridge from this occurrence-bearing carrier to pair-kernel physical source normalization, a later step that would connect the map to physical constants. The theorem also does not claim that the owner map is the only way to separate debit from credit, nor that it works for empty ledgers. Those limits are part of the theorem's statement, not omissions.

MODEL ownerMap · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
ownerMap · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:259 
noncomputable def ownerMap {d : Nat} (L : LedgerState d) :
    Fin (ledgerCommittedUnits L) → Fin d × Side :=
  fun i =>
    ownerOfSlot d (Classical.choose (exists_owner_slot L i))
      (Classical.choose_spec (exists_owner_slot L i)).1
THEOREM ownerMap_separates_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
ownerMap_separates_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:485 
theorem ownerMap_separates_debit_credit (d : Nat) [NeZero d] :
    let L0 : LedgerState d := { debit := fun _ => 0, credit := fun _ => 0 }
    let k : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
    let Ld := post L0 k Side.debit
    let Lc := post L0 k Side.credit
    ledgerCommittedUnits Ld = 1 ∧
      ledgerCommittedUnits Lc = 1 ∧
      ownerMap Ld ⟨0, by
        have h := (ownerCount_post_zero (d := d)).2.2.1
        exact Nat.lt_of_lt_of_eq Nat.zero_lt_one h.symm⟩ ≠
      ownerMap Lc ⟨0, by
        have h := (ownerCount_post_zero (d := d)).2.2.2
        exact Nat.lt_of_lt_of_eq Nat.zero_lt_one h.symm⟩ := by
  intro L0 k Ld Lc
  have h := ownerCount_post_zero (d := d)
  refine ⟨h.2.2.1, h.2.2.2, ?_⟩
  have hd := ownerMap_of_unique_owner Ld k Side.debit h.2.2.1 h.1
  have hc := ownerMap_of_unique_owner Lc k Side.credit h.2.2.2 h.2.1
  intro heq
  exact (by decide : Side.debit ≠ Side.credit)
    (congrArg Prod.snd (hd.symm.trans (heq.trans hc)))
THEOREM postingOfBoundaryStep_of_post · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
postingOfBoundaryStep_of_post · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:399 
theorem postingOfBoundaryStep_of_post {d : Nat} [NeZero d] {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    postingOfBoundaryStep L (post L k side) = (k, side) := by
  classical
  have hprop :
      ownerCount (post L k side) k side = ownerCount L k side + 1 ∧
        (∀ k' side', (k', side') ≠ (k, side) →
          ownerCount (post L k side) k' side' = ownerCount L k' side') := by
    constructor
    · simp [ownerCount_post hn k side k side]
    · intro k' side' hne
      simp [ownerCount_post hn k side k' side', hne]
  have hε :=
    Classical.epsilon_spec
      (p := fun p : Fin d × Side =>
        ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 + 1 ∧
          (∀ k' side', (k', side') ≠ p →
            ownerCount (post L k side) k' side' = ownerCount L k' side'))
      ⟨(k, side), hprop⟩
  set p := postingOfBoundaryStep L (post L k side)
  have hform := ownerCount_post hn k side p.1 p.2
  by_cases heq : (p.1, p.2) = (k, side)
  · exact heq
  · have h1 : ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 := by
      simpa [heq] using hform
    have h2 : ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 + 1 := hε.1
    omega
THEOREM heat_eq_ownerMap_ne_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
heat_eq_ownerMap_ne_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:672 
theorem heat_eq_ownerMap_ne_debit_credit (d : Nat) [NeZero d] :
    let L0 : LedgerState d := { debit := fun _ => 0, credit := fun _ => 0 }
    let k : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
    let Ld := post L0 k Side.debit
    let Lc := post L0 k Side.credit
    NonnegLedger (d := d) L0 ∧
      movingStepHeat (cutOfLedgerState L0) (cutOfLedgerState Ld) =
        movingStepHeat (cutOfLedgerState L0) (cutOfLedgerState Lc) ∧
      ownerMap Ld ⟨0, by
        have h := (ownerCount_post_zero (d := d)).2.2.1
        exact Nat.lt_of_lt_of_eq Nat.zero_lt_one h.symm⟩ ≠
      ownerMap Lc ⟨0, by
        have h := (ownerCount_post_zero (d := d)).2.2.2
        exact Nat.lt_of_lt_of_eq Nat.zero_lt_one h.symm⟩ := by
  intro L0 k Ld Lc
  have hn : NonnegLedger (d := d) L0 := ⟨fun _ => le_rfl, fun _ => le_rfl⟩
  refine ⟨hn, ?_, (ownerMap_separates_debit_credit d).2.2⟩
  rw [induced_movingStepHeat_eq_one hn (legalAtomicTick_of_post L0 k Side.debit),
    induced_movingStepHeat_eq_one hn (legalAtomicTick_of_post L0 k Side.credit)]

What this page does not claim

The owner map is a physical quantity. The owner map is the only way to separate debit from credit. The theorem applies to empty ledgers.

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/Holography/LedgerOwnerMapCut.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND