two_time_unique
plain-language theorem explainer
Given a two-time boundary condition that pairs a forward accumulation with its compensating backward requirement under an explicit balance equation, the backward value is forced to be the exact negation of the forward value. Researchers modeling mock theta functions as unclosed 8-tick windows or Zwegers-style shadows as phantom light projections would cite this to establish uniqueness of the boundary data. The proof is a one-line linear-arithmetic reduction that directly invokes the embedded balance hypothesis.
Claim. Let $ttbc$ be a two-time boundary condition consisting of an integer forward accumulation $a$, an integer backward requirement $b$, and the relation $a + b = 0$. Then $b = -a$.
background
The module interprets Ramanujan's mock theta functions as partition functions on unclosed 8-tick windows whose modular defect is identified with a pending phantom magnitude. True modular forms correspond to perfectly balanced windows (sum zero), while mock theta functions carry an explicit balance debt that is resolved only by adding a non-holomorphic shadow term. In the RS reading this shadow is phantom light: the projection of future balance requirements that constrain the present configuration backward in time.
proof idea
One-line wrapper that applies linear arithmetic to the balance field of the TwoTimeBoundaryCondition structure, which directly encodes forward_accumulated + backward_required = 0 and therefore yields the required negation.
why it matters
The result supplies the uniqueness clause for the two-time boundary condition inside the mock-theta-to-phantom correspondence. It thereby closes the algebraic step that lets the anti-holomorphic shadow be recovered deterministically from the holomorphic part, consistent with the eight-tick octave and the phantom-light interpretation of Zwegers' completion. No downstream uses are recorded yet; the declaration sits as a local closure for the Ramanujan-bridge section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.