conj_involution
plain-language theorem explainer
Conjugation on a ledger event, defined via negation of its integer flow, satisfies the involution property that two applications recover the original event. Researchers formalizing double-entry bookkeeping and abelian group structure in Recognition Science cite this result to anchor the ledger algebra. The proof executes case analysis on the event constructor then simplifies directly against the conjugate definition.
Claim. For any ledger event $e$ whose flow is an integer, the conjugate of the conjugate equals $e$.
background
A ledger event consists of a signed integer flow on an edge, positive for debit and negative for credit, equipped with the additive group structure on the integers. Its conjugate is the negation of that flow. The LedgerAlgebra module assembles these events into pages and windows that enforce balance, relying on the basic LedgerEvent structure and its negation operation.
proof idea
Case analysis on the LedgerEvent constructor reduces the goal to the definition of conjugation as negation; simplification then discharges the equality.
why it matters
The result supplies the involution clause in the ledger algebra certificate, which verifies that events form an abelian group, paired events cancel, and net flux vanishes at vertices. It is also referenced in the phi-ring certificate to confirm that Galois conjugation behaves as an involution. This algebraic step precedes the construction of neutral eight-tick windows and graded conservation in the simplicial ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.