TwoTimeBoundaryCondition
plain-language theorem explainer
The TwoTimeBoundaryCondition structure encodes an unclosed 8-tick window as a pair of integers summing to zero, with the forward component capturing accumulated holomorphic data and the backward component encoding the anti-holomorphic phantom debt constraint. Researchers working on mock theta completions or RS ledger balance would cite this when modeling future requirements that project backward onto the present state. The declaration is a direct structure definition with three fields and no proof body.
Claim. A two-time boundary condition consists of integers $f, b$ together with the relation $f + b = 0$, where $f$ is the forward accumulated component and $b$ is the required backward component.
background
The module treats mock theta functions as descriptions of unclosed 8-tick windows whose partition functions carry a mock modular defect. This defect is identified with the Phantom Magnitude, the pending future debt that constrains the current configuration. Zwegers' non-holomorphic shadow completes the mock theta to a harmonic Maass form; the module equates this shadow with Phantom Light, the projection of future balance requirements. The DOC_COMMENT states that the completion $f + g^* = ĥ$ is the two-time boundary condition of the RS 8-tick ledger.
proof idea
This is a structure definition with no proof body. The three fields are introduced directly: forward_accumulated and backward_required as integers, and balance as the equality forward_accumulated + backward_required = 0. No lemmas or tactics are invoked.
why it matters
The structure supplies the type used by the downstream theorem two_time_unique, which extracts the relation backward_required = -forward_accumulated. It supplies the concrete object for the mock theta to phantom light correspondence described in the module DOC_COMMENT, linking the 8-tick octave (T7) and the phantom debt that restores full symmetry when included. It closes the local scaffolding for unclosed windows in the RamanujanBridge development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.