Holography Ledger State Horizon Context Extend Context Context Of Ledger State

The ledger's horizon

A ledger state is a discrete record of accounts, each holding a debit and a credit value. In the Recognition Science framework, every such state carries a horizon, a natural number that counts the total committed units across all accounts, the sum of the absolute values of every debit and every credit. The declaration extendContext_contextOfLedgerState proves a precise fact about how this horizon behaves when the ledger changes.

The theorem states that extending the context of a given ledger state yields exactly the context of a new ledger state whose committed units are one greater. In plainer terms: if the ledger's total commitment is n, then the extended context is the context of a ledger with n plus one committed units. The proof is direct: the context of a ledger state is defined by its horizon record, and extending a context adds one to that record. The result follows by unfolding these definitions.

This fact matters because it connects two separate descriptions of the same event. A legal atomic tick, a single indivisible posting step, is defined both as a change in the ledger state and as an extension of the horizon context. The theorem shows these two views agree: the horizon of the new ledger state equals the extended horizon of the old one. The same event, seen from the ledger side or from the horizon side, produces the same count.

The declaration does not claim that every ledger state has a unique context, nor that the horizon determines the full state. Two different ledger states with the same total committed units share a context, but their individual account balances may differ. The theorem is about the horizon record alone, not about the internal distribution of debits and credits.

What the result establishes is a bridge: the framework's abstract notion of extending a horizon has a concrete realization in the ledger's committed units. A reader can now see that a legal tick, whatever else it does, always advances the horizon by one. That single fact anchors the ledger's dynamics to the framework's geometric language.

/-- Successor committed-units context is `extendContext` of the pre-state context. -/
theorem extendContext_contextOfLedgerState {d : Nat} (L : LedgerState d) :
    extendContext (contextOfLedgerState L) =
      mkLedgerContext (ledgerCommittedUnits L + 1) :=
  extendContext_mkLedgerContext (ledgerCommittedUnits L)

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

What this page does not claim

The theorem does not claim that a ledger state is uniquely determined by its horizon record. It does not claim that every horizon extension corresponds to a legal atomic tick. It does not claim anything about the internal distribution of debits and credits within a ledger state.

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: