neutralWindow_isNeutral
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish neutrality for windows without explicit pairing.
- Does not extend to non-integer or continuous flows.
- Does not prove conservation across multiple connected windows.
- Does not address the J-cost function or phi-ladder directly.
Lean usage
theorem use_neutralWindow_isNeutral (e1 e2 e3 e4 : LedgerEvent) : (neutralWindow e1 e2 e3 e4).isNeutral := neutralWindow_isNeutral e1 e2 e3 e4formal statement (Lean)
136theorem neutralWindow_isNeutral (e₁ e₂ e₃ e₄ : LedgerEvent) :
137 (neutralWindow e₁ e₂ e₃ e₄).isNeutral := by
proof body
Term-mode proof.
138 simp [Window8.isNeutral, Window8.sum, neutralWindow, LedgerEvent.conj, Fin.sum_univ_eight]
139
140/-! ## §4. The Graded Ledger -/
141
142/-- A **graded ledger** assigns events to vertices of a graph.
143 The grading ensures conservation at each node:
144 inflow = outflow at every vertex. -/