Holography Owner Indexed Horizon Cut Boundary Profile Separates Debit Credit

What the boundary profile proves

A ledger is a record of events, each event a posting that moves a unit from one account to another. In the Recognition Science framework, a ledger state is a collection of channels, and each channel belongs to an account and to one of two sides, debit or credit. The boundary profile of a state is a table that records, for every account and side, how many channels exist there. It is a coarse summary: it counts, but it does not say which specific channel is which.

The theorem boundaryProfile_separates_debit_credit, proved in the framework's machine-checked library of formal theorems, shows that this coarse summary is enough to separate debit from credit. When a legal posting adds exactly one new channel to the ledger, addressed to a particular account and side, the boundary profile of the new state differs from the old one in exactly one place: the count for that account and side has increased by one. The theorem proves that from the two boundary profiles alone, before and after, one can recover the posting: which account was touched and whether it was a debit or a credit. The posting's address is encoded in the shape of the boundary, not in any extra label attached to the event.

This separation is not a free choice. The framework proves that a boundary profile cannot be constant across all states; some states must have different profiles, otherwise the profile would carry no information at all. The theorem also shows that the profile determines the full nonnegative ledger state: if two states have the same boundary profile, they have the same debit and credit entries. The count is not a lossy hash; it is a complete description of the state, for states that respect the nonnegativity condition.

In Recognition Science, this result is a step toward a larger goal: showing that the ledger's own structure, not an external bookkeeper, determines where events land. The framework models every committed unit as an active posted bit, and this theorem shows that the boundary profile, a purely structural feature, recovers the posting. The result is model-internal: it holds within the C3 all-ones encoding, where every channel is either active or not. It does not yet bridge to the physical layer of the framework, where pair-kernel source normalization and remaining physical equality live. That bridge remains open.

What the theorem does not claim is just as important. It does not claim that the boundary profile is the only way to separate debit from credit, nor that it works for all possible ledger states. It requires the nonnegativity condition. It does not claim that the physical bridge to the framework's deeper structure is complete. And it does not claim that the framework's constants, such as hbar or G, play any role in this result; the forcing path here is independent of them.

/-- Debit vs credit from the same state yield different boundary profiles
at equal total aperture. -/
theorem boundaryProfile_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 = ledgerCommittedUnits Lc ∧
      boundaryProfile Ld ≠ boundaryProfile Lc := by
  intro L0 k Ld Lc
  have hn : NonnegLedger (d := d) L0 := ⟨fun _ => le_rfl, fun _ => le_rfl⟩
  have hz := ownerCount_post_zero (d := d)
  refine ⟨by rw [hz.2.2.1, hz.2.2.2], ?_⟩
  intro heq
  have hD : boundaryProfile Ld (k, Side.debit) = 1 := by
    simpa [boundaryProfile, Ld] using hz.1
  have hC : boundaryProfile Lc (k, Side.debit) = 0 := by
    have hcnt : ownerCount Lc k Side.debit = ownerCount L0 k Side.debit := by
      simp [Lc, ownerCount_post hn k Side.credit k Side.debit]
    change ownerCount Lc k Side.debit = 0
    rw [hcnt]
    change Int.natAbs (L0.debit k) = 0
    simp [L0]
  have : boundaryProfile Ld (k, Side.debit) = boundaryProfile Lc (k, Side.debit) :=
    congrFun heq (k, Side.debit)
  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]

/-- 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 theorem does not claim that the boundary profile is the only way to separate debit from credit. The theorem does not claim that the physical bridge to the framework's deeper structure is complete. The theorem does not claim that the framework's constants, such as hbar or G, play any role in this result.

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: