Holography Ledger State Horizon Context Cut Of Ledger State Post Active Bits

The moving cut

A ledger, a discrete record of events, has a boundary: the number of committed units it has accepted. In the Recognition Science framework, that boundary is a cut, a horizon separating what has been recorded from what has not. The declaration cutOfLedgerState_post_activeBits proves a simple fact: when a legal atomic tick, a single indivisible posting, adds one unit to a nonnegative ledger, the cut's active exterior bits, the count of exposed boundary positions, increase by exactly one. The theorem states this equality formally: the active bits of the cut after the posting equal the active bits of the cut extended by one step.

The proof is a direct consequence of how the framework defines a ledger state. A ledger holds debits and credits as integers; its committed units are the sum of their absolute values. A posting to one account, on one side, increases that sum by one, provided the ledger starts nonnegative. The cut is built from that unit count, and its active bits are defined to equal that count. The theorem chains these definitions: the posting raises the unit count, the cut tracks it, and the active bits follow. No free parameters enter; the exposed bit is computed from the tick's unit commitment, never chosen.

The declaration does not claim that a posting is the only way to change a cut, nor that every cut extension corresponds to a legal tick. It does not assert that the cut's internal structure, such as which accounts hold which balances, is determined by the active bits alone. The theorem concerns the count of active bits, not the full state. It also does not claim that the reverse process, removing a unit, is legal; the framework proves separately that a legal atomic tick cannot be reversed.

What the theorem establishes is a consistency condition: the ledger's growth and the horizon's growth are locked together. Each legal posting moves the cut forward by one, and the active bits register that move. This is the framework's way of saying that a legal event and its boundary record are projections of the same tick, two views of one change.

/--
Cut T1 at the heat/bit level: the post-state all-ones cut and the posted-one
extension of the pre-cut have equal active exterior bit counts. Full `LocalCut`
equality is blocked by dependent aperture indices; heat is the occurrence content.
-/
theorem cutOfLedgerState_post_activeBits {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    activeExteriorBits (cutOfLedgerState (post L k side)) =
      activeExteriorBits (extendCut (cutOfLedgerState L) 1) := by
  have hs := ledgerCommittedUnits_post hn k side
  have hL : activeExteriorBits (cutOfLedgerState (post L k side)) =
      (ledgerCommittedUnits (post L k side) : ℤ) := by
    simpa [cutOfLedgerState] using activeExteriorBits_mkLedgerCut
      (ledgerCommittedUnits (post L k side))
  have hR : activeExteriorBits (extendCut (cutOfLedgerState L) 1) =
      activeExteriorBits (cutOfLedgerState L) + 1 := by
    rw [activeExteriorBits_extendCut, postedBitValue_one]
  have hpre : activeExteriorBits (cutOfLedgerState L) =
      (ledgerCommittedUnits L : ℤ) := by
    simpa [cutOfLedgerState] using
      activeExteriorBits_mkLedgerCut (ledgerCommittedUnits L)
  rw [hL, hR, hpre, hs]
  norm_num

theorem ledgerCommittedUnits_post {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    ledgerCommittedUnits (post L k side) = ledgerCommittedUnits L + 1 := by
  classical
  rcases hn with ⟨hd, hc⟩
  cases side with
  | debit =>
    unfold ledgerCommittedUnits
    have hD := sum_natAbs_post_debit hd k
    have hC : (∑ i : Fin d, Int.natAbs ((post L k Side.debit).credit i)) =
        (∑ i : Fin d, Int.natAbs (L.credit i)) := by
      apply Finset.sum_congr rfl; intro i _; simp [post]
    omega
  | credit =>
    unfold ledgerCommittedUnits
    have hD : (∑ i : Fin d, Int.natAbs ((post L k Side.credit).debit i)) =
        (∑ i : Fin d, Int.natAbs (L.debit i)) := by
      apply Finset.sum_congr rfl; intro i _; simp [post]
    have hC := sum_natAbs_post_credit hc k
    omega

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

What this page does not claim

The declaration does not claim that every cut extension corresponds to a legal atomic tick. It does not claim that the active bits determine the full ledger state, only the unit count. It does not claim that a posting can be reversed.

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: