Window8
plain-language theorem explainer
Window8 defines a block of eight ledger events, each an integer flow on an edge. Researchers tracking aggregate balance and debt in the Recognition ledger algebra cite this structure when building neutral windows from paired events or computing running sums. The declaration is a direct structure introduction that equips the type with a total-flow sum and a zero-sum neutrality predicate.
Claim. A window is a function $events : Fin 8 → LedgerEvent$, where each LedgerEvent carries a signed integer flow (positive for debit, negative for credit) and the events form the additive group of integers.
background
LedgerEvent is the basic object: a structure whose sole field is an integer flow, equipped with addition, negation and zero so that the set of events forms the group (ℤ, +, 0). Positive flow denotes debit and negative flow denotes credit. The Window8 structure simply packages eight such events under a single name for collective operations.
proof idea
The declaration introduces the structure with a single field events : Fin 8 → LedgerEvent. The sum is obtained by Finset.univ.sum over the flows of those events. isNeutral is the predicate asserting that this sum equals zero.
why it matters
Window8 supplies the basic eight-event object that neutralWindow and the balanceDebt family in the Ramanujan bridge both consume. It realizes the eight-tick window required by the octave periodicity (T7) in the forcing chain and thereby enables the transition from individual events to aggregate neutrality and debt statements used throughout the mock-theta analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.