Holography Ledger State Horizon Context Active Exterior Bits Mk Ledger Cut

The ledger's exposed face

A ledger is a discrete record of events. In this framework, each event is a posting: one account gains a unit of debit or credit, and the ledger moves from one state to the next. The horizon is the ledger's boundary, the face it presents to anything outside it. The exposed bits are the entries on that face, and the question is what they record.

The declaration activeExteriorBits_mkLedgerCut answers that question for the simplest case. When a ledger has committed n units, meaning the total absolute size of all its debits and credits is n, the cut built from that ledger has exactly n exposed bits. The proof is a theorem in the framework's machine-checked library of formal theorems: it derives the equality activeExteriorBits (mkLedgerCut n) = n from the definitions alone, with no extra assumptions about the ledger's contents.

This is a counting fact, not a physical law. It says the boundary faithfully reports the ledger's size, nothing more. The exposed bits do not distinguish which accounts hold which balances, nor whether a particular entry was a debit or a credit. A separate theorem in the same library shows that a cut with all bits set to one cannot tell a debit posting from a credit posting. The count is exact; the identity of the entries is not.

What the declaration does not claim is wider. It does not say that the exposed bits determine the ledger's full state, only its total committed size. It does not say that every possible boundary reading arises from some ledger, only that the cut built from a ledger shows its size. And it does not introduce any new physical constants or parameters: the exposed bit is computed from the ledger's unit commitment, never chosen freely.

The payoff is a clean separation. The boundary of a ledger can be trusted to carry one piece of information, its size, and the framework proves that trust is well placed. What the boundary cannot carry, the identity of the entries behind it, is left to other structures. This is the first step in showing that a legal atomic tick, one posting event, is exactly a moving cut extension: the boundary grows by one, and the exposed count grows by one, together.

private theorem activeExteriorBits_mkLedgerCut (n : Nat) :
    activeExteriorBits (mkLedgerCut n) = (n : ℤ) := by
  unfold activeExteriorBits mkLedgerCut ofExteriorReading exteriorReading
  simp [postedBitValue_one, compA]

/--
Obstruction witness: debit and credit posts from the zero ledger are distinct
legal ticks of equal committed size. Their all-ones cuts are HEq (same aperture
count). Totals alone do not yield a separating exterior-channel enumeration
(C7/C6 escalation trigger).
-/
theorem allOnes_cut_does_not_separate_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 Ldebit := post L0 k Side.debit
    let Lcredit := post L0 k Side.credit
    Ldebit ≠ Lcredit ∧
      ledgerCommittedUnits Ldebit = ledgerCommittedUnits Lcredit ∧
      NonnegLedger (d := d) L0 ∧
      LegalAtomicTick (d := d) L0 Ldebit ∧
      LegalAtomicTick (d := d) L0 Lcredit ∧
      HEq (cutOfLedgerState Ldebit) (cutOfLedgerState Lcredit) := by
  intro L0 k Ldebit Lcredit
  have hn : NonnegLedger (d := d) L0 := ⟨fun _ => le_rfl, fun _ => le_rfl⟩
  have hunits :
      ledgerCommittedUnits Ldebit = ledgerCommittedUnits Lcredit := by
    simp [Ldebit, Lcredit, ledgerCommittedUnits_post hn]
  refine ⟨?_, hunits, hn, legalAtomicTick_of_post L0 k Side.debit,
    legalAtomicTick_of_post L0 k Side.credit, ?_⟩
  · intro heq
    have : Ldebit.debit k = Lcredit.debit k := congrArg (fun M => M.debit k) heq
    simp [Ldebit, Lcredit, post] at this
  · change HEq (mkLedgerCut (ledgerCommittedUnits Ldebit))
        (mkLedgerCut (ledgerCommittedUnits Lcredit))
    rw [hunits]

/-- Exposed bit of a legal atomic tick: computed as `1` from unit L1 commitment. -/
def postedBitOfLegalAtomicTick {d : Nat} {L L' : LedgerState d}
    (_h : LegalAtomicTick (d := d) L L') : ZMod 2 :=
  1

What this page does not claim

The exposed bits determine the ledger's full state. Every possible boundary reading arises from some ledger. The declaration introduces new physical constants or parameters.

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: