pith. sign in
module module high

IndisputableMonolith.Algebra.LedgerAlgebra

show as:
view Lean formalization →

The LedgerAlgebra module supplies the group structure for signed integer flows that model debit and credit events on edges. Category builders in RecognitionCategory cite it to ground balanced ledger constructions. The module consists of type definitions and elementary group lemmas imported from Cost and Mathlib.

claimA ledger event is an element of the additive group $(\mathbb{Z}, +, 0)$, where a positive value denotes a debit and a negative value denotes a credit.

background

Recognition Science tracks physical flows through ledger events. The module imports Mathlib and the Cost module to equip the integers with their standard additive group structure. The supplied doc-comment states that a ledger event is a signed integer flow on an edge, positive for debit and negative for credit, forming the group $(\mathbb{Z}, +, 0)$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the RecognitionCategory construction that assembles recognition structures from ledger primitives. It supplies the base group operations required before graded ledgers and windowed balance checks appear in downstream algebra.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (19)