neutralWindow_isNeutral
plain-language theorem explainer
A window assembled from four ledger events by inserting each with its conjugate sums to zero total flow. Ledger algebra work in Recognition Science cites this to confirm double-entry balance inside eight-event blocks. The proof is a one-line simplification that unfolds the window constructor, the sum over Fin 8, and conjugate cancellation.
Claim. Let $e_1,e_2,e_3,e_4$ be signed integer flows. The eight-event window formed by the sequence $e_1,-e_1,e_2,-e_2,e_3,-e_3,e_4,-e_4$ has total sum zero.
background
LedgerEvent is a signed integer flow on an edge, positive for debit and negative for credit, carrying the additive group structure of the integers. Window8 packages eight such events and supplies a sum operation that totals their flows. neutralWindow builds a concrete Window8 by placing four input events together with their conjugates to occupy the eight positions.
proof idea
The proof is a one-line simp that unfolds Window8.isNeutral, Window8.sum, neutralWindow, LedgerEvent.conj, and Fin.sum_univ_eight. The resulting expression reduces to the sum of four pairs, each event plus its negation, which cancels identically.
why it matters
This supplies the fourth clause of the ledger_algebra_certificate theorem, which verifies that eight-window neutrality follows from four paired events. The certificate as a whole confirms the abelian group structure, conjugation involution, paired cancellation, and net flux zero at vertices. It thereby supports the conservation properties required for the ledger factorization in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.