balanced_iff_zero_debt
plain-language theorem explainer
An 8-tick window is balanced precisely when its balance debt over the full length vanishes. Researchers modeling mock theta functions as unclosed windows in Recognition Science would cite this equivalence to link neutrality with zero pending compensation. The proof is a one-line wrapper that rewrites via the balanced_has_zero_debt lemma and simplifies the sum definition of IsBalanced.
Claim. Let $w$ be a map from the 8-element index set to the integers. Then $w$ is balanced (its signal sum equals zero) if and only if the balance debt of $w$ at step 8 under the reflexive bound equals zero.
background
Window8 is the type of 8-tick windows, each an assignment of integer signal values to the eight positions. IsBalanced holds exactly when the sum of these eight values is zero, which the module identifies with a closed window and therefore with a true modular form. The balance debt function returns the unique compensating value required to reach total sum zero; when the window length is already 8 the reflexive bound le_refl 8 is supplied. This sits inside the RamanujanBridge.MockThetaPhantom module, whose setting equates unclosed 8-tick windows with mock theta functions and their required future compensation with the phantom shadow.
proof idea
The proof is a one-line wrapper. It rewrites the biconditional using the sibling lemma balanced_has_zero_debt, then applies simp to unfold IsBalanced into the explicit sum predicate.
why it matters
The result supplies the direct equivalence between the IsBalanced predicate and vanishing debt inside an 8-tick window, which is the algebraic step needed to identify closed windows with true modular forms in the mock-theta correspondence. It therefore supports the module's central claim that the phantom shadow is exactly the future compensation required to close the window. In the broader framework this reinforces the eight-tick octave (T7) where balanced configurations carry zero defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.