Encyclopedia Holography Holography Ledger Owner Map Cut Heat Eq Owner Map Ne Debit Credit

ARTICLE 3 claims 3 theorems

Holography Ledger Owner Map Cut Heat Eq Owner Map Ne Debit Credit

A machine-checked theorem shows that in a discrete ledger, a single debit and a single credit, at the same aperture, can be told apart by where they sit in the record.

Verify this page

The owner map cut

A ledger, a discrete record of events, can be organized by owner. Each committed unit, each entry that counts, is assigned to a canonical owner: an account and a side, debit or credit. The assignment follows a fixed rule: owners are listed in lexicographic order, and each owner gets a contiguous block, a bucket, of positions. The owner map is the function that sends each unit's position to its owner.

The theorem heat_eq_ownerMap_ne_debit_credit proves a separation fact. Take a ledger with at least one account. Post a single debit to one account, then, in a separate run, post a single credit to the same account. The two resulting ledgers have the same number of committed units. The theorem states that the owner map of the debit-ledger differs from the owner map of the credit-ledger at the same aperture, the same position index. The two postings are not interchangeable: the record itself distinguishes debit from credit.

The proof is constructive. The declaration postingOfBoundaryStep reads only the two ledger states, before and after, and recovers which owner and side were posted. A companion theorem, ownerMap_separates_debit_credit, supplies the explicit inequality. The construction never copies from a tick proof; it works directly from the owner-map boundary data. The forcing path uses no physical constants: no sourceScale, no hbar, no G, no Real.pi. The axioms are limited to the standard three: propext, Classical.choice, Quot.sound.

In Recognition Science, this is a boundary-native cut. The framework models a legal tick as an owned boundary extension: the posting is recoverable from the owner-map data alone. The theorem does not claim that this carrier connects to pair-kernel physical source normalization or to RemainingPhysicalEquality; that bridge remains open. It does not claim that any particular physical system obeys this ledger. It claims only that within the discrete ledger model, one legal tick is an owned boundary extension, and debit versus credit leave different traces in the owner map.

THEOREM heat_eq_ownerMap_ne_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
heat_eq_ownerMap_ne_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:672 
theorem heat_eq_ownerMap_ne_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
    NonnegLedger (d := d) L0 ∧
      movingStepHeat (cutOfLedgerState L0) (cutOfLedgerState Ld) =
        movingStepHeat (cutOfLedgerState L0) (cutOfLedgerState Lc) ∧
      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 hn : NonnegLedger (d := d) L0 := ⟨fun _ => le_rfl, fun _ => le_rfl⟩
  refine ⟨hn, ?_, (ownerMap_separates_debit_credit d).2.2⟩
  rw [induced_movingStepHeat_eq_one hn (legalAtomicTick_of_post L0 k Side.debit),
    induced_movingStepHeat_eq_one hn (legalAtomicTick_of_post L0 k Side.credit)]
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 heat_eq_ownerMap_ne_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean
heat_eq_ownerMap_ne_debit_credit · IndisputableMonolith/Holography/LedgerOwnerMapCut.lean:672 
theorem heat_eq_ownerMap_ne_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
    NonnegLedger (d := d) L0 ∧
      movingStepHeat (cutOfLedgerState L0) (cutOfLedgerState Ld) =
        movingStepHeat (cutOfLedgerState L0) (cutOfLedgerState Lc) ∧
      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 hn : NonnegLedger (d := d) L0 := ⟨fun _ => le_rfl, fun _ => le_rfl⟩
  refine ⟨hn, ?_, (ownerMap_separates_debit_credit d).2.2⟩
  rw [induced_movingStepHeat_eq_one hn (legalAtomicTick_of_post L0 k Side.debit),
    induced_movingStepHeat_eq_one hn (legalAtomicTick_of_post L0 k Side.credit)]

What this page does not claim

This theorem does not bridge to pair-kernel physical source normalization or RemainingPhysicalEquality. This theorem does not claim any specific physical system obeys this ledger. This theorem does not derive any physical constant such as 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/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