shadow_is_unique
plain-language theorem explainer
Any integer accumulated sum s has a unique integer t satisfying s + t = 0. Researchers modeling mock theta functions or phantom balance in Recognition Science cite this to fix the compensating shadow term. The term-mode proof supplies the witness -s, dispatches the equality via ring, and settles uniqueness via linarith.
Claim. For any integer $s$, there exists a unique integer $t$ such that $s + t = 0$.
background
In the module on mock theta functions and phantom light, an unclosed 8-tick window carries an accumulated debt represented by the integer sum s. The shadow is the unique future compensation t that restores exact balance, satisfying s + t = 0. This algebraic fact mirrors Zwegers' addition of a non-holomorphic shadow that completes a mock theta function to a harmonic Maass form.
proof idea
The proof is a direct term-mode construction. It exhibits the witness -s, proves the equality s + (-s) = 0 by the ring tactic, and establishes uniqueness by showing any other satisfying t must coincide with -s via linarith.
why it matters
This result supplies the uniqueness step used by debt_forces_unique_future and phantom_shadow_uniqueness. It connects the mock modular defect to the phantom light projection that closes the eight-tick window (T7) and restores full symmetry. The declaration touches the open question of how pending balance debt constrains the configuration space of unclosed windows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.