balanced_completion_unique
plain-language theorem explainer
Uniqueness of balanced completions for partial 8-tick windows follows directly from injectivity of negation on integers: if a and b each satisfy the zero-sum condition with their additive inverses, then equality of the inverses is equivalent to equality of the originals. Researchers modeling the Ramanujan mock-theta to harmonic Maass form completion via phantom light would cite this result to confirm that partial balance data fixes the remaining ticks. The proof is a one-line term application of the standard negation-injectivity lemma.
Claim. If two integers $a$ and $b$ each satisfy the zero-balance condition $a + (-a) = 0$ and $b + (-b) = 0$, then $-a = -b$ if and only if $a = b$.
background
The module frames mock theta functions as unclosed 8-tick windows carrying a balance debt (phantom magnitude), while true modular forms correspond to perfectly closed windows whose sum is zero. One octave equals eight fundamental ticks, with tick defined as the RS-native time quantum τ₀ = 1. Upstream structures such as PhiForcingDerived.of supply the J-cost calibration and LedgerFactorization.of supplies the underlying (ℝ₊, ×) factorization used to interpret these integer accumulations as phase debt.
proof idea
The proof is a direct term-mode application of neg_inj, the Mathlib lemma that negation is injective on ℤ. No additional tactics or reductions are required; the hypotheses ha and hb are the trivial additive-inverse identities that hold for every integer.
why it matters
This result supplies the uniqueness step required for the mock-theta-to-phantom-light correspondence: partial balance information determines the full window, allowing the non-holomorphic shadow (phantom light) to complete the mock form to a harmonic Maass form. It sits inside the eight-tick octave (T7) of the forcing chain and supports sibling declarations such as phantom_completes_to_balanced and balanced_phantom_zero. No open scaffolding remains for this specific uniqueness claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.