Holography Owner Indexed Horizon Cut Posting Of Profiles Of Legal Atomic Tick

Reading a posting from its profiles

A posting is the smallest unit of change in a ledger: one account moves one unit from its debit side to its credit side, and nothing else moves. The declaration postingOfProfiles_of_legalAtomicTick is a machine-checked theorem about a specific way of encoding this idea. It says that if you know the complete shape of a ledger before a posting and the complete shape after it, you can identify exactly which account and which side received the new unit. The shape in question is the boundary profile: for every account and every side, the number of committed units held there.

The theorem works because a legal atomic tick, the framework's name for one indivisible posting step, changes exactly one entry in that profile. Every other account and side keeps its count unchanged. The declaration proves that the unique location where the count increased by one is the address of the posting itself, written as the pair (account, side). This is not a guess or a convention; it is a proved consequence of how the posting step is defined. The proof also shows that the posting's new channel, the slot that holds the posted unit, carries exactly that address, and that all previously existing channels keep their identities and readings intact.

In Recognition Science, a ledger is a discrete record of events, and the cost of recording each event is forced by the framework's core theorem. This declaration belongs to that setting. It is a model-internal result: it holds within a specific encoding called the C3 all-ones encoding, where every committed unit is represented as an active bit. The theorem is proved in the framework's machine-checked library of formal theorems, with axioms limited to the standard three: propositional extensionality, choice, and quotient soundness. No physical constants such as the reduced Planck constant or the gravitational constant appear in this forcing path.

The declaration does not claim that this owner-indexed encoding is the only way to represent postings, nor that it is the physically realized one. The bridge from this abstract carrier to the framework's pair-kernel source normalization remains open. It also does not claim that the boundary profile alone determines the full ledger state in general; that holds only for nonnegative ledgers, where no account holds a negative balance. The theorem is a precise statement about a chosen model, not a universal law of physics.

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

theorem channelInsert_preserves_reading {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side)
    (c : OwnerChannel L) :
    ownerReading (post L k side) (channelInsert hn k side c) =
      ownerReading L c := by
  simp [ownerReading]

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

/-- C3 MODEL encoding on the owner-structured type: every committed unit is active. -/
def ownerReading {d : Nat} (L : LedgerState d) : OwnerChannel L → ZMod 2 :=
  fun _ => 1

What this page does not claim

This result does not prove that the owner-indexed encoding is physically realized. It does not show that the boundary profile determines the ledger state for ledgers with negative balances. It does not derive any physical constant from the posting structure.

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: