Encyclopedia Holography Holography Ledger Owner Map Cut Posting Of Boundary Step Of Post

ARTICLE 3 claims 3 theorems

Holography Ledger Owner Map Cut Posting Of Boundary Step Of Post

A single legal tick in a recognition ledger carries enough information to identify exactly which account and side it touched.

Verify this page

The posting theorem

The declaration postingOfBoundaryStep establishes a precise recovery property for a discrete record of events. In the framework's ledger model, each committed unit is assigned to a unique owner, an account paired with a side (debit or credit). The theorem states that if you take a ledger state and apply a single legal tick, which adds exactly one unit to a specific owner's count, then the posting function, which examines only the two ledger states, returns exactly that owner. In plainer terms: the record of the change itself contains enough information to say who was changed, with no need for any external annotation.

The proof works by reading only the two states, not by copying from a tick proof. The posting function looks at the difference in per-owner counts between the before and after states. The theorem shows that this difference uniquely identifies the owner whose count increased by one. It also shows that debit and credit produce different boundary functions at the same aperture, so the side is recoverable as well. This is a formal result in the machine-checked library of formal theorems, with no special axioms beyond the standard three.

In Recognition Science, this result is part of a larger arc. The framework models physical structure as arising from such discrete recognition events. This particular theorem is a step in showing that a single legal tick is an owned boundary extension: the posting is recoverable from the owner-map boundary data. It is a bridging result, connecting the abstract ledger to the notion of a boundary step. The next arc, which remains open, is to bridge from this occurrence-bearing carrier to pair-kernel physical source normalization.

The theorem does not claim that the posting function is computable in any practical sense; it uses a noncomputable choice operator. It also does not claim that any constant like hbar or G appears in this forcing path; the docstring explicitly notes that no such constants are used. The result is purely about the ledger structure itself.

THEOREM postingOfBoundaryStep_of_post · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
postingOfBoundaryStep_of_post · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:399 
theorem postingOfBoundaryStep_of_post {d : Nat} [NeZero d] {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    postingOfBoundaryStep L (post L k side) = (k, side) := by
  classical
  have hprop :
      ownerCount (post L k side) k side = ownerCount L k side + 1 ∧
        (∀ k' side', (k', side') ≠ (k, side) →
          ownerCount (post L k side) k' side' = ownerCount L k' side') := by
    constructor
    · simp [ownerCount_post hn k side k side]
    · intro k' side' hne
      simp [ownerCount_post hn k side k' side', hne]
  have hε :=
    Classical.epsilon_spec
      (p := fun p : Fin d × Side =>
        ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 + 1 ∧
          (∀ k' side', (k', side') ≠ p →
            ownerCount (post L k side) k' side' = ownerCount L k' side'))
      ⟨(k, side), hprop⟩
  set p := postingOfBoundaryStep L (post L k side)
  have hform := ownerCount_post hn k side p.1 p.2
  by_cases heq : (p.1, p.2) = (k, side)
  · exact heq
  · have h1 : ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 := by
      simpa [heq] using hform
    have h2 : ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 + 1 := hε.1
    omega
THEOREM postingOfBoundaryStep_of_post · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
postingOfBoundaryStep_of_post · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:399 
theorem postingOfBoundaryStep_of_post {d : Nat} [NeZero d] {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    postingOfBoundaryStep L (post L k side) = (k, side) := by
  classical
  have hprop :
      ownerCount (post L k side) k side = ownerCount L k side + 1 ∧
        (∀ k' side', (k', side') ≠ (k, side) →
          ownerCount (post L k side) k' side' = ownerCount L k' side') := by
    constructor
    · simp [ownerCount_post hn k side k side]
    · intro k' side' hne
      simp [ownerCount_post hn k side k' side', hne]
  have hε :=
    Classical.epsilon_spec
      (p := fun p : Fin d × Side =>
        ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 + 1 ∧
          (∀ k' side', (k', side') ≠ p →
            ownerCount (post L k side) k' side' = ownerCount L k' side'))
      ⟨(k, side), hprop⟩
  set p := postingOfBoundaryStep L (post L k side)
  have hform := ownerCount_post hn k side p.1 p.2
  by_cases heq : (p.1, p.2) = (k, side)
  · exact heq
  · have h1 : ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 := by
      simpa [heq] using hform
    have h2 : ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 + 1 := hε.1
    omega
THEOREM ownerMap_separates_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
ownerMap_separates_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:485 
theorem ownerMap_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 = 1 ∧
      ledgerCommittedUnits Lc = 1 ∧
      ownerMap Ld ⟨0, by
        have h := (ownerCount_post_zero (d := d)).2.2.1
        exact Nat.lt_of_lt_of_eq Nat.zero_lt_one h.symm⟩ ≠
      ownerMap Lc ⟨0, by
        have h := (ownerCount_post_zero (d := d)).2.2.2
        exact Nat.lt_of_lt_of_eq Nat.zero_lt_one h.symm⟩ := by
  intro L0 k Ld Lc
  have h := ownerCount_post_zero (d := d)
  refine ⟨h.2.2.1, h.2.2.2, ?_⟩
  have hd := ownerMap_of_unique_owner Ld k Side.debit h.2.2.1 h.1
  have hc := ownerMap_of_unique_owner Lc k Side.credit h.2.2.2 h.2.1
  intro heq
  exact (by decide : Side.debit ≠ Side.credit)
    (congrArg Prod.snd (hd.symm.trans (heq.trans hc)))

What this page does not claim

The posting function is not claimed to be computable in a practical sense. The theorem does not claim that any physical constant such as hbar or G appears in the forcing path. The theorem does not claim to bridge to pair-kernel physical source normalization; that remains an open target.

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/LedgerOwnerMapCut.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND