nonzero_accumulation_forces_phantom
plain-language theorem explainer
Nonzero accumulated signal in a partially filled 8-tick window forces strictly positive phantom magnitude. Researchers modeling the Ramanujan-Zwegers mock theta correspondence in Recognition Science would cite this to guarantee that balance debt registers as a nonzero shadow term. The proof is a term-mode reduction that rewrites phantomMagnitude via the debt definition, applies neg_ne_zero to the negated accumulation, and invokes positivity.
Claim. Let $pb$ be a PhantomBalance consisting of an integer accumulated signal $a$ and remaining ticks $r$ with $r ≤ 8$. If $a ≠ 0$, then the phantom magnitude of $pb$ is strictly positive.
background
PhantomBalance is the Recognition Science structure for the mock modular defect: an 8-tick window that has not yet reached neutrality. It stores the current accumulated integer signal sum together with the count of remaining ticks (constrained to be at most 8). The debt is defined as the negation of the accumulated sum; this quantity must be compensated to close the window and restore balance. In the module, true modular forms correspond to closed windows with zero debt, while mock theta functions describe open windows whose pending compensation appears as phantom magnitude.
proof idea
The term proof first simplifies phantomMagnitude using the debt definition, exposing an expression built from the absolute value of the negated accumulation. It then applies neg_ne_zero to obtain that the negated accumulation is nonzero, and finishes with the positivity tactic.
why it matters
This result supplies a basic positivity fact inside the MockThetaPhantom module and thereby supports the structural hypothesis that Zwegers' non-holomorphic shadow corresponds to Phantom Light. It directly encodes the consequence of the eight-tick octave (T7) for unclosed windows: any nonzero accumulation produces a nonzero phantom magnitude. As a proved statement it closes a minimal scaffolding point in the claimed mock theta ↔ phantom light correspondence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.