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

Side

show as:
view Lean formalization →

Side is the inductive type with constructors debit and credit that labels the direction of a unit posting in a d-account ledger. Ledger modelers cite it when formalizing atomic updates that increment exactly one coordinate of the phi vector by +1. The declaration is a plain inductive definition deriving decidable equality and representation, with no proof obligations.

claimLet Side be the two-element type whose elements are the posting directions debit and credit.

background

The module models ledger states over the carrier AccountRS d, defined as the recognition structure with universe Fin d and the trivial relation R that holds for every pair. LedgerState d is the type Recognition.Ledger (AccountRS d), whose phi component records the integer difference debit minus credit at each account. The post operation, which depends on Side, applies a single unit change to either the debit or credit vector at a chosen account k.

proof idea

The declaration is an inductive definition introducing the two constructors debit and credit, followed by deriving DecidableEq and Repr. It is consumed directly by the match expression inside the definition of post.

why it matters in Recognition Science

Side supplies the discrete choice required to turn the abstract parity-adjacency lemma into an explicit ledger posting model. It is used in downstream theorems such as legalAtomicTick_of_post and ledgerJlogCost_post, which verify that each single post satisfies the monotone and unit-cost conditions. Within the Recognition framework this supports the transition from vector lemmas to ledger-shaped atomic ticks that change phi by exactly one unit while preserving the J-cost structure.

scope and limits

formal statement (Lean)

  68inductive Side where
  69  | debit
  70  | credit
  71deriving DecidableEq, Repr
  72
  73/-- Apply a single unit post (either debit or credit) at account `k`. -/

used by (18)

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

depends on (2)

Lean names referenced from this declaration's body.