Encyclopedia Holography Holography Ledger Owner Map Cut Constant Owner Assignment Not Bucket Correct

ARTICLE 3 claims 3 theorems

Holography Ledger Owner Map Cut Constant Owner Assignment Not Bucket Correct

A formal proof that no fixed, pre-assigned owner can account for every posting in a ledger, forcing ownership to be read from the ledger's own state.

Verify this page

What the owner-map cut proves

A ledger, a discrete record of committed units, must be able to say who owns each unit. One tempting shortcut is to assign each unit to a fixed owner in advance, say by a rule that the first unit always belongs to account A, the second to account B, and so on. The declaration constant_owner_assignment_not_bucket_correct is a machine-checked theorem that rules out that shortcut: no single fixed assignment of owners can correctly describe every possible ledger state.

The proof works by considering a single posting, a legal step that adds one committed unit to some owner. The framework's library shows that such a step changes the ledger's committed count by exactly one, and that the posting is recoverable from the boundary data alone: the owner map, which assigns each committed unit to its owner, is built purely from the ledger's own per-owner counts. The theorem then demonstrates that a constant assignment, one that does not depend on the ledger state, fails. For any chosen fixed owner, there exists a ledger state where that owner's count does not match the number of units the fixed rule would assign to them.

What this establishes is that ownership is a property of the ledger's state, not of a pre-ordained schedule. The owner map is a function of the ledger, and the posting of a new unit lands at a position determined by the current counts. This is the sense in which the framework models a boundary-native cut: the data needed to describe a boundary step is already present in the ledger states themselves, with nothing copied from an external proof or tick.

The theorem does not claim that ownership is physically meaningful in any conventional sense, nor that this ledger model corresponds to a physical system. It is a statement about the internal consistency of the framework's own definitions. It also does not claim that the owner map is the only way to assign ownership, only that a fixed, constant assignment is insufficient. The proof is axiom-clean, relying only on the standard logical axioms of the machine-checked library, with no additional assumptions about physical constants.

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))
THEOREM legalAtomicTick_changes_units · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
legalAtomicTick_changes_units · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:616 
theorem legalAtomicTick_changes_units {d : Nat} {L L' : LedgerState d}
    (hn : NonnegLedger (d := d) L)
    (h : LegalAtomicTick (d := d) L L') :
    ledgerCommittedUnits L' = ledgerCommittedUnits L + 1 :=
  ledgerCommittedUnits_legalAtomicTick_succ hn h
THEOREM ownerMap_fiber_card · 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])⟩

What this page does not claim

This theorem does not claim that the ledger model corresponds to any physical system. This theorem does not claim that the owner map is the only possible way to assign ownership. This theorem does not claim that ownership is physically meaningful in a conventional sense.

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