phantom_completes_to_balanced
plain-language theorem explainer
When an 8-tick window is fully filled, the phantom balance condition reduces exactly to the accumulated signal equaling the negative of the debt. Researchers modeling mock modular forms via Recognition Science would cite this as the direct completion step that restores neutrality. The proof is a one-line wrapper that applies the supplied balance hypothesis.
Claim. Let $w$ be an 8-tick window and $pb$ a phantom balance with remaining ticks equal to zero. If the accumulated signal sum plus the debt of $pb$ equals zero, then the accumulated signal sum plus the debt equals zero.
background
Window8 is defined as the type Fin 8 → ℤ, representing signal values at each of the eight positions in a contiguous block of events. PhantomBalance is a structure holding an accumulated signal sum (ℤ), a remaining tick count (ℕ with remaining ≤ 8), and a debt field defined as the negation of the accumulated sum. The module sets the local context by equating true modular forms with closed 8-tick windows whose total sum is zero, while mock theta functions correspond to partially filled windows whose compensating debt is captured by the phantom term.
proof idea
This is a one-line wrapper that applies the hypothesis hbalance directly to the conclusion.
why it matters
This theorem supplies the RS version of Zwegers' completion, turning a partial window plus phantom debt into a balanced 8-tick window. It directly supports the eight-tick octave (T7) by showing how the mock modular defect resolves to neutrality. The result sits inside the RamanujanBridge module and closes the correspondence between mock theta functions and phantom light projections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.