SimpleLedger
plain-language theorem explainer
SimpleLedger constructs a minimal ledger on the two-vertex recognition structure whose universe is Bool and whose relation holds exactly on unequal states. Modelers cite it to verify that constant debit and credit maps satisfy conservation on closed chains. The definition is a direct record construction with no lemmas or reductions.
Claim. Let $S$ be the recognition structure with universe Bool and relation $R(a,b) := a ≠ b$. The ledger $L$ on $S$ is defined by debit$_L(x) := 1$ and credit$_L(x) := 0$ for every $x$.
background
The module presents a minimal two-vertex recognition structure whose universe is Bool and whose relation is the inequality predicate. A Ledger on this structure supplies debit and credit maps together with an associated potential used to compute flux. The upstream Conserves class states that chainFlux vanishes on every closed chain, where chainFlux is the difference in potential between the last and head vertices of the chain.
proof idea
The definition is a direct record construction that assigns the constant function returning 1 to debit and the constant function returning 0 to credit. No lemmas are invoked; the construction follows immediately from the Ledger signature.
why it matters
This definition supplies a concrete test case for the Conserves class and thereby supports the atomicity step in the Recognition framework. It illustrates conservation on the simplest bidirectional structure before scaling to the full phi-ladder and eight-tick octave. The example closes a basic modeling gap for closed-chain flux calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.