IsMockOrder_iff
plain-language theorem explainer
The theorem states that a natural number p is a mock theta order precisely when p equals 3, 5, or 7. Researchers examining Ramanujan's mock theta functions or the arithmetic origins of partition congruences would cite this equivalence. The proof is a direct biconditional that applies the completeness lemma in one direction and exhaustive case analysis with decision tactics in the other.
Claim. Let $p$ be a natural number. Then $p$ is a mock theta order (i.e., $p$ is prime, coprime to 8, and $p < 8$) if and only if $p = 3$ or $p = 5$ or $p = 7$.
background
In the RamanujanBridge module the predicate IsMockOrder is defined by the conjunction of primality, coprimality to 8, and strict inequality below 8. Geometrically this encodes the failure of a k-periodic pattern to close inside one 8-tick window whenever gcd(k,8)=1, producing mock rather than true modular symmetry. The surrounding module unifies this set with the congruence primes via the single number 24 = directed_flux(Q3), noting that 3 divides 24 while 11 exceeds 8, leaving the overlap exactly at {5,7}.
proof idea
The proof constructs the biconditional explicitly. The forward direction applies the upstream lemma mock_orders_complete to the three defining assumptions of IsMockOrder. The converse performs case analysis on the disjunction p=3 or p=5 or p=7 and discharges each branch by the tactics decide and omega, which verify primality, coprimality to 8, and the bound p<8.
why it matters
This characterization is invoked directly by the parent theorems mock_and_congruence_unified_by_Q3 and overlap_is_exactly_5_7, which together establish that both mock theta orders and Ramanujan congruence primes are forced by the single arithmetic datum 24 = directed_flux(Q3). Within the Recognition Science framework it supplies the concrete content of the eight-tick octave (T7) by isolating the primes that cannot close inside the period-8 window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.