pith. machine review for the scientific record. sign in
def definition def or abbrev high

post

show as:
view Lean formalization →

The post operation defines the atomic update that increments either the debit or credit counter by one at a chosen account index k in a d-dimensional ledger. Researchers working on ledger conservation, parity adjacency, or eight-tick synchronization cite it as the primitive step that turns vector updates into explicit posting sequences. The definition is a direct case split on the Side constructor that constructs the new ledger record with the targeted counter incremented.

claimLet $L$ be a ledger state over $d$ accounts. For index $k$ and side $s$ (debit or credit), post$(L,k,s)$ is the state obtained by adding one to the $s$-counter at account $k$ while leaving the opposite counter unchanged.

background

LedgerState d is the abbreviation Recognition.Ledger (AccountRS d), where AccountRS d equips the set Fin d with the trivial recognition relation. Side is the inductive type carrying the two constructors debit and credit. The module documentation states that this supplies the explicit ledger-shaped model in which a tick posts exactly one unit to exactly one account, thereby changing the phi = debit - credit vector by ±1 at a single coordinate and inducing a one-bit parity change.

proof idea

The definition is a noncomputable match on the side parameter. Debit case returns a record whose debit function is incremented at k and whose credit function is copied unchanged; the credit case is symmetric. No lemmas are applied; the construction is direct.

why it matters in Recognition Science

This supplies the posting primitive used by sequential_preserves_conservation to lift single-step conservation to arbitrary finite schedules, and by the Gap45 physical-motivation lemmas (eight_tick, fibonacci_connection_explained) that close the 8-tick cycle. It realizes the ledger model required for the parity one-bit adjacency theorem and thereby connects to the eight-tick octave (T7) in the forcing chain.

scope and limits

formal statement (Lean)

  74noncomputable def post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) : LedgerState d := by

proof body

Definition body.

  75  classical
  76  exact match side with
  77  | Side.debit =>
  78      { debit := fun i => if i = k then L.debit i + 1 else L.debit i
  79      , credit := L.credit }
  80  | Side.credit =>
  81      { debit := L.debit
  82      , credit := fun i => if i = k then L.credit i + 1 else L.credit i }
  83

used by (22)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.