IsBalanced
plain-language theorem explainer
A window of eight integer signals is balanced exactly when their sum vanishes. This definition is cited in the mock theta correspondence to mark closed 8-tick configurations that carry no net debt. It is introduced as a direct equating of the predicate to the zero-sum condition, supplying the base case for all subsequent debt and phantom lemmas.
Claim. A map $w : [8] → ℤ$ is balanced when $∑_{i=0}^7 w(i) = 0$.
background
The module treats an 8-tick window as a map from eight discrete positions to integer signal values. Balance is the zero-sum condition on these values, which the module identifies with a closed window free of pending debt. This usage parallels the ledger-algebra definition of a balanced page, where the computed balance of events equals zero.
proof idea
The declaration is a direct definition that sets the balanced predicate equal to the vanishing of the sum over the eight indices. No lemmas or tactics are invoked; the equality is the primitive notion.
why it matters
It supplies the zero-debt condition used by the downstream theorem balanced_iff_zero_debt, which equates balance to vanishing balance debt. The definition anchors the Ramanujan bridge by identifying closed 8-tick windows with true modular symmetry, consistent with the eight-tick octave of the forcing chain. It leaves open the explicit construction of the phantom-light projection for windows that remain unbalanced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.