twenty_four_eq_8_times_3
plain-language theorem explainer
The arithmetic identity 24 equals 8 times 3 is recorded as a verified fact inside the Q3 unification of mock theta orders and partition congruences. Workers on Ramanujan's mock theta functions and partition congruences cite this factorization to separate the set {3,5,7} from {5,7,11} via the directed flux count. The proof is a direct normalization that confirms the prime factorization 24 equals 2 cubed times 3.
Claim. The natural number 24 equals 8 multiplied by 3.
background
The module treats 24 as the directed flux count of the Q3 structure. This single integer forces the mock theta orders to be the odd primes p with gcd(p,8)=1 and p<8, while the congruence primes are the three smallest primes p with gcd(p,24)=1 and p>3. Because 24 factors as 8 times 3, the prime 3 divides the flux and therefore appears only among mock orders, while 11 exceeds the 8-tick window and appears only among congruence primes. The overlap at 5 and 7 follows directly from coprimality to 24 together with the bound p<8.
proof idea
One-line wrapper that applies norm_num to the arithmetic identity.
why it matters
The identity supplies the explicit factorization 24=8 times 3 that the module uses to explain the overlap between mock theta orders and congruence primes. It anchors the claim that both sets are determined by the single directed flux count of Q3. In the broader framework this factorization aligns with the eight-tick octave of period 2 cubed, separating the mock-only prime 3 from the congruence-only prime 11.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.