Holography Owner Indexed Horizon Cut Free Assignment Not Boundary Profile

The boundary profile

A ledger, a discrete record of events, can be viewed as a collection of channels, each holding a bit that is either active or not. In the Recognition Science framework, a horizon cut groups these channels by owner, where an owner is an account paired with a side, debit or credit. The boundary profile of a ledger state is the function that records, for each owner, how many channels that owner has. This profile is a coarse summary: it counts channels per owner but discards which specific channels are active.

The theorem free_assignment_not_boundaryProfile states a limitation of this summary. It proves that no single natural number n can serve as the boundary profile value for every owner in every possible ledger state. In plainer terms, the count of channels per owner is free to vary; it is not forced to be a constant across all accounts and all states. The proof works by contradiction, showing that if such a universal constant existed, it would contradict the existence of ledger states with different numbers of committed units.

This result is model-internal. It holds within a specific encoding called the C3 all-ones encoding, where every committed unit is represented as an active posted bit. The theorem does not claim that the boundary profile is unconstrained in any physical sense. It only says that within this formal model, the profile is not pinned to a single value by the definitions alone.

What the declaration does not claim is equally important. It does not say that boundary profiles are arbitrary or that they carry no information. Other theorems in the same file show that the profile does separate debit from credit and can recover a posting from two states. The force of free_assignment_not_boundaryProfile is narrower: it rules out one specific kind of rigidity, namely a constant profile, and thereby keeps the model flexible enough to represent varied ledger states.

/-- 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

/-- Fiber-size profile of the owner-indexed cut: cut shape data by owner. -/
def boundaryProfile {d : Nat} (L : LedgerState d) : Fin d × Side → Nat :=
  fun p => ownerCount L p.1 p.2

What this page does not claim

The boundary profile is unconstrained or carries no information about the ledger state. The theorem applies outside the C3 all-ones encoding or to any physical system directly. The freedom of the boundary profile has a direct physical consequence in the framework.

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: