Encyclopedia Holography Holography Ledger Owner Map Cut Ledger Tick Is Owned Boundary Extension

ARTICLE 4 claims 4 theorems

Holography Ledger Owner Map Cut Ledger Tick Is Owned Boundary Extension

A ledger's every entry can be read back from the ledger's own state, with no hidden record, and each new posting changes that state in a way that belongs to exactly one account.

Verify this page

The owner map

A ledger is a discrete record of events, in this case a list of committed units, each assigned to an account and a side, debit or credit. The Recognition Science framework models such a ledger as a state that evolves one legal tick at a time, where a tick is a single atomic posting that adds one committed unit. The question is whether the ledger itself, just its current state, carries enough information to say who owns each unit and what the last posting was.

The owner map answers that question. It is a function that reads the ledger state and assigns every committed unit to its owner, an account and a side pair, by looking at the cumulative counts of units per owner. The framework's machine-checked library of formal theorems proves that this map is correct: the number of units mapped to a given owner equals that owner's recorded count, and a unit that falls in an owner's bucket is indeed assigned to that owner. The map is built only from the ledger's own numbers, with nothing copied from any external record of how the ledger got there.

The central result, the one this page names, is that one legal tick is an owned boundary extension. In plain language: when the ledger takes a single legal step, the posting that caused the step can be recovered from the boundary data, the before and after states, and it is recoverable as a specific owner and side. The theorem proves that the posting function, which reads only the two ledger states, returns exactly the account and side that the tick posted to. It also proves that a debit and a credit produce different boundary functions at the same aperture, so the side of the posting is not lost in the state change.

In Recognition Science, this result matters because it shows a tick is not an arbitrary mutation. The ledger's own state, before and after, determines the posting uniquely. That is what the declaration establishes: a legal tick is not just a change, it is a change owned by a particular account and side, and the ownership is visible in the ledger itself.

What the declaration does not claim is just as important. It does not claim that the owner map is the only possible way to assign ownership, and in fact the library proves that a constant assignment, one that ignores the ledger state, fails to match the owner counts. It does not claim anything about the physical constants of the framework; the forcing path here uses no source scale, no hbar, no G, and no pi. And it does not claim to bridge from this occurrence-bearing carrier to pair-kernel physical source normalization, which remains an open target for the next arc.

THEOREM ownerMap_fiber_card · mem_bucket_of_ownerMap · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
ownerMap_fiber_card · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:306 
theorem ownerMap_fiber_card {d : Nat} (L : LedgerState d)
    (k : Fin d) (side : Side) :
    (Finset.univ.filter (fun i : Fin (ledgerCommittedUnits L) =>
      ownerMap L i = (k, side))).card =
      ownerCount L k side := by
  classical
  set a := bucketStart L k side with ha
  set b := insertPos L k side with hb
  have hab : b = a + ownerCount L k side := by simp [hb, ha, insertPos]
  have hle : b ≤ ledgerCommittedUnits L := insertPos_le_units L k side
  let s : Finset (Fin (ownerCount L k side)) := Finset.univ
  have hcard : s.card = ownerCount L k side := by simp [s]
  refine Eq.trans ?_ hcard
  refine (Finset.card_bij
    (fun (t : Fin (ownerCount L k side)) (_ : t ∈ s) =>
      (⟨a + t.val, by
          have ht : t.val < ownerCount L k side := t.isLt
          have hlt : a + t.val < a + ownerCount L k side := Nat.add_lt_add_left ht a
          exact lt_of_lt_of_le (hab ▸ hlt) hle⟩ :
        Fin (ledgerCommittedUnits L)))
    ?_ ?_ ?_).symm
  · intro t _
    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
    refine ownerMap_eq_of_mem_bucket L _ k side (Nat.le_add_right a t.val) ?_
    have ht : t.val < ownerCount L k side := t.isLt
    have : a + t.val < a + ownerCount L k side := Nat.add_lt_add_left ht a
    simpa [hb, insertPos, ha] using this
  · intro t1 t2 _ _ heq
    exact Fin.ext (Nat.add_left_cancel (congrArg Fin.val heq))
  · intro i hi
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi
    have hmem := mem_bucket_of_ownerMap L i
    rw [hi] at hmem
    have hlo : a ≤ i.val := by simpa [ha, bucketStart] using hmem.1
    have hhi : i.val < a + ownerCount L k side := by
      simpa [hb, insertPos, ha] using hmem.2
    refine ⟨⟨i.val - a,
        Nat.sub_lt_left_of_lt_add hlo (by omega : i.val < a + ownerCount L k side)⟩,
      by simp [s], Fin.ext (by simp [Nat.add_sub_of_le hlo])⟩
mem_bucket_of_ownerMap · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:291 
theorem mem_bucket_of_ownerMap {d : Nat} (L : LedgerState d)
    (i : Fin (ledgerCommittedUnits L)) :
    bucketStart L (ownerMap L i).1 (ownerMap L i).2 ≤ i.val ∧
      i.val < insertPos L (ownerMap L i).1 (ownerMap L i).2 := by
  classical
  let s := Classical.choose (exists_owner_slot L i)
  have hs := Classical.choose_spec (exists_owner_slot L i)
  have hmap : ownerMap L i = ownerOfSlot d s hs.1 := rfl
  have hslot :
      ownerSlot (d := d) (ownerMap L i).1 (ownerMap L i).2 = s := by
    rw [hmap, ownerSlot_ownerOfSlot]
  constructor
  · simpa [bucketStart, hslot] using hs.2.1
  · simpa [insertPos_eq_cumSucc, hslot] using hs.2.2
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 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 constant_owner_assignment_not_bucket_correct · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
constant_owner_assignment_not_bucket_correct · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:622 
theorem constant_owner_assignment_not_bucket_correct {d : Nat} [NeZero d]
    (p0 : Fin d × Side) :
    ¬ (∀ (L : LedgerState d) (k : Fin d) (side : Side),
        (Finset.univ.filter (fun _ : Fin (ledgerCommittedUnits L) =>
          p0 = (k, side))).card = ownerCount L k side) := by
  classical
  intro h
  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
  have hz := ownerCount_post_zero (d := d)
  have hUd : ledgerCommittedUnits Ld = 1 := hz.2.2.1
  have hUc : ledgerCommittedUnits Lc = 1 := hz.2.2.2
  have hD := h Ld k Side.debit
  have hC := h Lc k Side.credit
  have hcardD :
      (Finset.univ.filter (fun _ : Fin (ledgerCommittedUnits Ld) =>
        p0 = (k, Side.debit))).card =
        if p0 = (k, Side.debit) then 1 else 0 := by
    split_ifs with hp
    · simp [hp, hUd]
    · simp [hp]
  have hcardC :
      (Finset.univ.filter (fun _ : Fin (ledgerCommittedUnits Lc) =>
        p0 = (k, Side.credit))).card =
        if p0 = (k, Side.credit) then 1 else 0 := by
    split_ifs with hp
    · simp [hp, hUc]
    · simp [hp]
  rw [hcardD, hz.1] at hD
  rw [hcardC, hz.2.1] at hC
  have hpD : p0 = (k, Side.debit) := by
    by_cases hp : p0 = (k, Side.debit)
    · exact hp
    · simp [hp] at hD
  have hpC : p0 = (k, Side.credit) := by
    by_cases hp : p0 = (k, Side.credit)
    · exact hp
    · simp [hp] at hC
  exact (by decide : Side.debit ≠ Side.credit)
    (congrArg Prod.snd (hpD.symm.trans hpC))

What this page does not claim

The declaration does not prove that the owner map is the only possible correct assignment, only that a constant one fails. The declaration does not involve the framework's physical constants hbar, G, or pi in its forcing path. The declaration does not connect this ledger result to pair-kernel physical source normalization, which remains open.

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