Holography Owner Indexed Horizon Cut Boundary Profile Eq Iff Owner Counts

The boundary profile

In the Recognition Science framework, a ledger (a discrete record of committed units) tracks how many units each account holds on each side, debit or credit. The boundary profile of a ledger is the table of these counts, organized by account and side. The theorem boundaryProfile_eq_iff_ownerCounts states that two ledgers have identical boundary profiles if and only if, for every account and side, the owner counts are equal. This is a biconditional: profile equality and per-owner count equality are the same fact.

The result is proved in the machine-checked library of formal theorems. Its proof is direct: from profile equality, evaluate the profile at each account-side pair to get the count equality; from count equality, use function extensionality to conclude the profiles agree everywhere. The theorem is a definitional unfolding, not a deep structural result. It says the boundary profile is a complete invariant: it captures all the information in the owner counts, no more and no less.

What the theorem does not claim is more interesting. It does not say that the boundary profile determines the full ledger state. That is a separate theorem, boundaryProfile_determines_nonneg_state, which requires both ledgers to be nonnegative (no negative balances) and concludes equality of debit and credit arrays. The biconditional here is about the profile itself, not about reconstructing the ledger from it. It also does not claim that any assignment of counts is realizable: the theorem free_assignment_not_boundaryProfile shows that for any fixed number n, there exists a ledger whose boundary profile is not constantly n. Profiles are constrained by the ledger structure.

The practical consequence is that the boundary profile is a faithful shadow of the owner counts. When two ledgers are compared by their profiles, the comparison is exact: no information is lost in the profile, and no extra information is added. This makes the profile a sound basis for the framework's holographic claims, where boundary data is meant to stand in for the bulk state. The theorem certifies that the profile is not a lossy projection, at least with respect to owner counts.

theorem boundaryProfile_eq_iff_ownerCounts {d : Nat} (L L2 : LedgerState d) :
    boundaryProfile L = boundaryProfile L2 ↔
      ∀ k side, ownerCount L k side = ownerCount L2 k side := by
  constructor
  · intro h k side
    exact congrFun h (k, side)
  · intro h
    funext p
    exact h p.1 p.2

theorem boundaryProfile_eq_iff_ownerCounts {d : Nat} (L L2 : LedgerState d) :
    boundaryProfile L = boundaryProfile L2 ↔
      ∀ k side, ownerCount L k side = ownerCount L2 k side := by
  constructor
  · intro h k side
    exact congrFun h (k, side)
  · intro h
    funext p
    exact h p.1 p.2

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 boundary profile alone determines the full ledger state without a nonnegativity condition. Every assignment of counts to accounts and sides is a realizable boundary profile. The theorem connects the boundary profile to physical quantities like hbar or G.

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: