Holography Owner Indexed Horizon Cut Posting Of Profiles Eq Posting Of Boundary

The posting recovered

A ledger, a discrete record of events, can be read in two ways: by its internal state, the list of accounts and their balances, or by its boundary profile, the count of committed units on each side of each account. The declaration postingOfProfiles_eq_postingOfBoundaryStep proves that these two readings carry the same information. Given two ledger states, one before and one after a single legal posting, the boundary profile alone determines which account and which side, debit or credit, received the posting. The posting's address is recoverable from the shape of the boundary alone.

This is not a claim about physics. It is a theorem inside a formal model, a machine-checked library of formal theorems, about a specific encoding of ledgers. The model defines a channel set for each ledger state, where each channel is a slot for a committed unit, addressed by an account, a side, and an index within that account's count. The theorem shows that a legal posting, which adds exactly one new channel, changes the boundary profile in a way that is unique to that posting. The theorem postingOfProfiles_of_post states this directly: the posting recovered from the before and after profiles is exactly the posting that was made.

The proof rests on a chain of lemmas. A legal posting inserts one new channel, preserving all old channels and their readings. The new channel's address is the posting itself. The boundary profile, which counts channels per account and side, therefore changes by exactly one at the posting's address, and nowhere else. The theorem boundaryProfile_determines_nonneg_state goes further: two nonnegative ledger states with the same boundary profile have identical debit and credit balances. The boundary profile is not just a record of the last posting; it is a complete description of the ledger's state.

What the declaration does not claim is equally important. It does not claim that any arbitrary change in the boundary profile corresponds to a legal posting. The theorem free_assignment_not_boundaryProfile shows that a constant boundary profile, one where every account and side has the same count, cannot arise from a legal posting. It does not claim that the boundary profile can be computed without knowing the ledger's internal state; the profile is defined in terms of the ledger's committed units. And it does not claim anything about the physical world. The bridge from this owner-indexed carrier to physical source normalization remains open. The theorem is a statement about a formal model, not about spacetime.

theorem postingOfProfiles_of_post {d : Nat} [NeZero d] {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    postingOfProfiles L (post L k side) = (k, side) := by
  classical
  have hprop :
      boundaryProfile (post L k side) (k, side) =
          boundaryProfile L (k, side) + 1 ∧
        (∀ q : Fin d × Side, q ≠ (k, side) →
          boundaryProfile (post L k side) q = boundaryProfile L q) := by
    constructor
    · simp [boundaryProfile, ownerCount_post hn k side k side]
    · intro q hne
      simp [boundaryProfile, ownerCount_post hn k side q.1 q.2, hne]
  have hε :=
    Classical.epsilon_spec
      (p := fun p : Fin d × Side =>
        boundaryProfile (post L k side) p = boundaryProfile L p + 1 ∧
          (∀ q, q ≠ p → boundaryProfile (post L k side) q = boundaryProfile L q))
      ⟨(k, side), hprop⟩
  set p := postingOfProfiles L (post L k side)
  have hform := ownerCount_post hn k side p.1 p.2
  by_cases heq : p = (k, side)
  · exact heq
  · have h1 : boundaryProfile (post L k side) p = boundaryProfile L p := by
      simpa [boundaryProfile, heq] using hform
    have h2 : boundaryProfile (post L k side) p = boundaryProfile L p + 1 := hε.1
    omega

theorem boundaryProfile_determines_nonneg_state {d : Nat} {L L2 : LedgerState d}
    (hn : NonnegLedger (d := d) L) (hn2 : NonnegLedger (d := d) L2)
    (h : boundaryProfile L = boundaryProfile L2) :
    L.debit = L2.debit ∧ L.credit = L2.credit := by
  have hcount : ∀ k side, ownerCount L k side = ownerCount L2 k side :=
    (boundaryProfile_eq_iff_ownerCounts L L2).1 h
  constructor
  · funext k
    simp [(nonneg_entries_of_ownerCount hn k).1,
      (nonneg_entries_of_ownerCount hn2 k).1, hcount k Side.debit]
  · funext k
    simp [(nonneg_entries_of_ownerCount hn k).2,
      (nonneg_entries_of_ownerCount hn2 k).2, hcount k Side.credit]

theorem newChannel_owner {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    (newChannel hn k side).1 = (k, side) :=
  rfl

theorem channelInsert_preserves_owner {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side)
    (c : OwnerChannel L) :
    (channelInsert hn k side c).1 = c.1 := by
  cases c
  rfl

/-- Free assignment: a constant profile cannot match true fiber sizes for
states with different owner counts. -/
theorem free_assignment_not_boundaryProfile {d : Nat} [NeZero d]
    (n : Nat) :
    ¬ (∀ L : LedgerState d, ∀ p : Fin d × Side, boundaryProfile L p = n) := by
  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
  have hz := ownerCount_post_zero (d := d)
  have h0 : boundaryProfile L0 (k, Side.debit) = n := h L0 (k, Side.debit)
  have h1 : boundaryProfile Ld (k, Side.debit) = n := h Ld (k, Side.debit)
  have h0' : boundaryProfile L0 (k, Side.debit) = 0 := by
    simp [boundaryProfile, ownerCount, L0]
  have h1' : boundaryProfile Ld (k, Side.debit) = 1 := by
    simpa [boundaryProfile, Ld] using hz.1
  omega

What this page does not claim

The declaration does not claim that any boundary profile change corresponds to a legal posting. The declaration does not claim that the boundary profile is computable without the ledger's internal state. The declaration does not claim any physical interpretation; the bridge to physics 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/OwnerIndexedHorizonCut.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: