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 carrying the two directions for a unit ledger posting in the d-account model. Ledger modelers cite it when distinguishing debit from credit to track signed changes in the phi vector. The definition is a direct two-constructor inductive with derived decidable equality and representation.

claimLet Side be the type whose elements are debit and credit.

background

The module models ledger updates in which each atomic tick posts exactly one unit to one account, either as debit or credit. AccountRS d is the minimal carrier RecognitionStructure whose universe is Fin d and whose recognition relation is the constant true predicate. LedgerState d is the type of Recognition.Ledger instances over AccountRS d, so each state carries separate debit and credit maps from Fin d to integers. Side appears in the post operation that produces the next ledger state from the current one.

proof idea

The declaration is an inductive definition introducing the two constructors debit and credit, followed by automatic derivation of DecidableEq and Repr. No tactics or lemmas are applied.

why it matters in Recognition Science

Side supplies the direction parameter required by the post function and therefore by every downstream ledger lemma, including legalAtomicTick_of_post, ledgerJlogCost_post, and minCost_monotoneStep_implies_postingStep. It completes the explicit posting model that converts a single atomic tick into a one-bit change in the induced parity pattern, linking the ledger language to the parity-adjacency results of LedgerParityAdjacency.

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.