neutralWindow_isNeutral

formal source

 133    | ⟨7, _⟩ => e₄.conj
 134
 135/-- **PROVED: A window of paired events is neutral.** -/
 136theorem neutralWindow_isNeutral (e₁ e₂ e₃ e₄ : LedgerEvent) :
 137    (neutralWindow e₁ e₂ e₃ e₄).isNeutral := by
 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. -/
 145structure GradedLedger where
 146  /-- Number of vertices -/
 147  n : ℕ
 148  /-- Events on edges (indexed by source, target) -/
 149  edges : Fin n → Fin n → ℤ
 150  /-- Conservation at each vertex: inflow = outflow -/
 151  conservation : ∀ v : Fin n,
 152    (Finset.univ.sum fun u => edges u v) =
 153    (Finset.univ.sum fun w => edges v w)
 154
 155/-- The **net flux** through a vertex. -/
 156def GradedLedger.netFlux (L : GradedLedger) (v : Fin L.n) : ℤ :=
 157  (Finset.univ.sum fun u => L.edges u v) -
 158  (Finset.univ.sum fun w => L.edges v w)
 159
 160/-- **PROVED: Net flux is zero at every vertex (conservation).** -/
 161theorem GradedLedger.netFlux_zero (L : GradedLedger) (v : Fin L.n) :
 162    L.netFlux v = 0 := by
 163  unfold netFlux
 164  have h := L.conservation v
 165  omega
 166