MockModularDefect
plain-language theorem explainer
MockModularDefect encodes the non-holomorphic error of a mock theta function as a non-negative real magnitude that vanishes precisely when the form is modular. Researchers mapping Ramanujan's q-series to Recognition Science's 8-tick balance debt would cite this structure when constructing the phantom-light correspondence. It is supplied as a bare structure definition whose three fields record the magnitude, its non-negativity, and the zero-modularity equivalence.
Claim. A mock modular defect is a real number $m$ satisfying $m = 0$ if and only if the associated form is modular, together with the assertion $m ≥ 0$.
background
The module interprets mock theta functions as partition functions on partially filled 8-tick windows. A true modular form corresponds to a closed window whose sum is zero; a mock theta function records the pending compensation, called phantom balance, whose size is the defect magnitude. Upstream, the defect functional is taken from LawOfExistence.defect, which equals the J-cost for positive arguments, while the tick unit is supplied by Constants.tick as the fundamental RS time quantum.
proof idea
Direct structure definition. The three fields are declared explicitly: magnitude as a real, magnitude_nonneg as the inequality 0 ≤ magnitude, and zero_iff_modular as the biconditional with the simplified modular predicate.
why it matters
The structure supplies the domain type for MockThetaPhantomCorrespondence, the hypothesis that maps mock defects to phantom balances and thereby identifies Zwegers' shadow with the constraint from future 8-tick neutrality. It therefore occupies the Ramanujan-bridge step that links the classical mock-modular completion to the T7 eight-tick octave of the forcing chain. The open question it leaves is replacement of the placeholder equivalence by a full modular-form predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.