Holography Ledger State Horizon Context Ledger Committed Units Legal Atomic Tick

The committed-unit successor

A ledger is a discrete record of events, and in Recognition Science a legal atomic tick is the smallest allowed event: a single posting that moves value from one account to another. The framework's machine-checked library of formal theorems proves that such a tick always increases the committed unit count by exactly one. The committed unit count is the total absolute value, in whole units, that the ledger has recorded across all debit and credit entries. The theorem ledgerCommittedUnits_legalAtomicTick_succ states this precisely: for any nonnegative ledger state L, if a legal atomic tick takes L to L', then the committed units of L' equal the committed units of L plus one.

This successor fact is the hinge that connects the ledger to a horizon context. The framework defines a horizon context as a local record with a horizon length, and the committed unit count becomes that horizon length. The theorem T1 shows that after a legal atomic tick, the horizon record of the new state equals the extended horizon record of the old state: the horizon grows by one. A companion theorem, T1_heq, states the same identity at the level of the whole context, not just its record. Together they mean the ledger's own arithmetic, not any external parameter, drives the boundary of the local description.

The framework also proves that a legal atomic tick is a genuine transfer. The theorem legalAtomicTick_nonzero_transfer shows the new state differs from the old, and the theorem reverse_not_legalAtomicTick shows the reverse move is never legal. A further result, same_event_projections, bundles these facts: a legal atomic tick is a posting step, its induced moving-step heat equals one, and its horizon record extends by one. The heat value is the exposed bit computed from the tick's unit commitment, never a free parameter.

The theorem does not claim that every unit increase comes from a legal atomic tick, nor that the ledger's committed units alone determine the full physical state. The docstring names a residual: all-ones exterior readings from totals alone do not separate distinct posting steps that share a pre-state. The successor fact is a necessary condition on legal ticks, not a complete description of them.

theorem ledgerCommittedUnits_legalAtomicTick_succ {d : Nat} {L L' : LedgerState d}
    (hn : NonnegLedger (d := d) L) (h : LegalAtomicTick (d := d) L L') :
    ledgerCommittedUnits L' = ledgerCommittedUnits L + 1 := by
  obtain ⟨k, side, rfl⟩ := legalAtomicTick_implies_PostingStep (d := d) h
  exact ledgerCommittedUnits_post hn k side

/--
Make-or-break theorem T1: a legal atomic tick increments the horizon record by
exactly one. Because contexts are subsingleton up to record
(`context_eq_of_record_eq`), this is the content of
`contextOfLedgerState (postState) = extendContext (contextOfLedgerState (preState))`
once the aperture index is identified by `ledgerCommittedUnits_legalAtomicTick_succ`.
-/
theorem T1 {d : Nat} {L L' : LedgerState d}
    (hn : NonnegLedger (d := d) L)
    (h : LegalAtomicTick (d := d) L L') :
    (contextOfLedgerState L').horizonRecord =
      (extendContext (contextOfLedgerState L)).horizonRecord := by
  change ledgerCommittedUnits L' = ledgerCommittedUnits L + 1
  exact ledgerCommittedUnits_legalAtomicTick_succ hn h

/-- P3 bundle. -/
theorem legalAtomicTick_nonzero_transfer {d : Nat} {L L' : LedgerState d}
    (h : LegalAtomicTick (d := d) L L') :
    L ≠ L' ∧ PostingStep (d := d) L L' :=
  ⟨legalAtomicTick_ne h, legalAtomicTick_is_PostingStep h⟩

/-- Reverse of a legal atomic tick is not a legal atomic tick (monotonicity). -/
theorem reverse_not_legalAtomicTick {d : Nat} {L L' : LedgerState d}
    (h : LegalAtomicTick (d := d) L L') :
    ¬ LegalAtomicTick (d := d) L' L := by
  intro hrev
  obtain ⟨k, side, rfl⟩ := legalAtomicTick_implies_PostingStep (d := d) h
  rcases hrev with ⟨⟨hmonoD, hmonoC⟩, _⟩
  cases side with
  | debit =>
    have hle : L.debit k + 1 ≤ L.debit k := by simpa [post] using hmonoD k
    omega
  | credit =>
    have hle : L.credit k + 1 ≤ L.credit k := by simpa [post] using hmonoC k
    omega

/--
Same-event packaging: posting step, unit heat, and context-record extension are
projections of one legal tick. Cut equality does **not** recover the changed
account (see `allOnes_cut_does_not_separate_debit_credit`).
-/
theorem same_event_projections {d : Nat} {L L' : LedgerState d}
    (hn : NonnegLedger (d := d) L)
    (h : LegalAtomicTick (d := d) L L') :
    PostingStep (d := d) L L' ∧
      movingStepHeat (cutOfLedgerState L) (cutOfLedgerState L') = 1 ∧
      (contextOfLedgerState L').horizonRecord =
        (extendContext (contextOfLedgerState L)).horizonRecord :=
  ⟨legalAtomicTick_implies_PostingStep h,
    induced_movingStepHeat_eq_one hn h,
    T1 hn h⟩

What this page does not claim

The theorem does not claim that every unit increase comes from a legal atomic tick. The theorem does not claim that the committed units alone determine the full physical state. The theorem does not claim that distinct posting steps sharing a pre-state are separated by their exterior readings.

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