odd_prime_lt_8_in_mock_orders
plain-language theorem explainer
Odd primes less than 8 are precisely 3, 5 or 7. Researchers modeling mock theta functions via unclosed 8-tick windows cite this to establish exhaustiveness of Ramanujan's families. The argument obtains a lower bound of 2 from the prime property and then performs exhaustive case analysis on the integers up to 7.
Claim. Let $p$ be a natural number. If $p$ is prime, $p < 8$, and $p ≠ 2$, then $p = 3 ∨ p = 5 ∨ p = 7$.
background
The module interprets mock theta functions as descriptions of systems resolving balance debt within an 8-tick window. True modular forms correspond to closed windows with zero phantom magnitude, while the mock case carries a structured defect. This small arithmetic lemma verifies that the admissible orders in the mock setting coincide exactly with the odd primes below 8. The framework routinely enumerates small exhaustive sets, as seen in the complete lists of seven plot families, eight kinship systems, seven modes, and seven ore classes. The primality predicate here is the standard one on natural numbers.
proof idea
The proof begins by applying the two_le property of primes to derive 2 ≤ p. It then invokes interval_cases to partition the possible values of p into the integers from 2 to 7. The resulting six cases are resolved individually: reflexivity dispatches the matches to 3, 5 and 7, while the remaining cases are ruled out by contradiction with the oddness or primality assumptions.
why it matters
The result supplies the forward direction for the biconditional that characterizes the precise set of odd primes below 8. This closes the classification of Ramanujan's three families in the mock theta correspondence, consistent with the eight-tick octave of the Recognition Science framework. It touches no open questions but completes a local arithmetic check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.