eleven_congruence_eligible
plain-language theorem explainer
Eleven satisfies the eligibility predicate for Ramanujan congruence primes, which requires primality together with coprimality to 24. Researchers studying the Q3 unification of mock theta orders and partition congruences cite the result to place 11 inside the set {5,7,11}. The proof is a direct term that supplies the two decidable facts for these arithmetic properties.
Claim. $11$ is prime and satisfies $gcd(11,24)=1$.
background
The module establishes a Q3 unification in which mock theta orders are the odd primes below 8 that are coprime to 8, while congruence primes are the three smallest primes above 3 that are coprime to 24. The predicate IsCongruenceEligible therefore encodes exactly the arithmetic condition that a prime p is neither 2 nor 3. This definition is invoked to separate 11 from the mock-order set {3,5,7} while retaining it inside the congruence set.
proof idea
One-line term proof that constructs the required pair of decidable propositions: primality of 11 and coprimality of 11 to 24.
why it matters
The result is invoked by the downstream theorem that identifies {5,7,11} as the three smallest primes coprime to 24 above 3, thereby supplying the arithmetic reason Ramanujan encountered precisely these primes. It distinguishes 11 from the mock orders by the eight-tick bound while preserving the common overlap at 5 and 7, closing one link in the bridge between the forcing chain's T7 octave and the observed prime sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.