Side
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.