ledger_algebra_certificate
plain-language theorem explainer
The ledger algebra certificate asserts that events in the ledger group cancel when paired with their conjugates, that conjugation is its own inverse, that four paired events form a neutral window, and that graded ledgers conserve net flux at every vertex. Modelers of flow conservation on graphs or double-entry accounting systems would cite it. The proof assembles four prior results in a single term.
Claim. Let $E$ be the abelian group of ledger events under addition, with conjugation sending each event $e$ to its negative. Then $e + (-e) = 0$ for all $e$, the double application of conjugation recovers $e$, every window built from four paired events is neutral, and for any graded ledger $L$ with $n$ vertices the net flux vanishes at each vertex $v$.
background
A ledger event is a signed integer flow on an edge, positive for debit and negative for credit, forming the group structure $(Z, +, 0)$. Its conjugate is the negation. A graded ledger assigns such events to the edges of a graph on $n$ vertices and requires inflow to equal outflow at every vertex by definition. The certificate collects the algebraic facts that make global balance follow from local pairing and grading. It draws on the proved fact that paired events sum to zero, the involution property of conjugation, the neutrality theorem for windows of four paired events, and the net-flux-zero property of graded ledgers.
proof idea
The proof is a term-mode wrapper that directly supplies the four conjuncts by referencing the lemmas paired_event_sum_zero, conj_involution, neutralWindow_isNeutral, and GradedLedger.netFlux_zero.
why it matters
This declaration serves as the central certificate for ledger algebra, confirming double-entry cancellation, involution, neutrality of paired windows, and vertex conservation. It underpins the module's claim that antisymmetric edges imply global balance and net flux zero at all vertices. No downstream uses appear yet; the result closes the algebraic verification step for graded structures in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.