seven_congruence_eligible
plain-language theorem explainer
The theorem establishes that 7 is a prime coprime to 24, satisfying the eligibility condition for Ramanujan congruence primes. Researchers linking partition congruences to the Q3 structure would cite this when verifying the exact set {5,7,11}. The proof is a term-mode construction that builds the required conjunction by direct decision on primality and coprimality.
Claim. $7$ is a prime number with $gcd(7,24)=1$.
background
The CongruenceQ3Bridge module unifies Ramanujan's mock theta orders {3,5,7} and congruence primes {5,7,11} through the single number 24, identified as the directed flux of Q3. A prime p is congruence-eligible when it is coprime to 24, i.e., neither 2 nor 3, via the definition IsCongruenceEligible p := Nat.Prime p ∧ Nat.Coprime p 24. The module setting notes that 24 = 8 × 3 forces the overlap at {5,7} while separating 3 (mock-only) and 11 (congruence-only). The upstream definition of IsCongruenceEligible supplies the exact predicate used here.
proof idea
The proof is a term-mode construction that directly supplies the pair proving the conjunction in the definition of IsCongruenceEligible. It applies the decide tactic to confirm Nat.Prime 7 and Nat.Coprime 7 24 separately, yielding the required structure without further lemmas.
why it matters
This result feeds the parent theorem congruence_primes_are_three_smallest, which shows {5,7,11} are the three smallest primes coprime to 24 above 3, and supports overlap_is_exactly_5_7. It fills the arithmetic verification step for the congruence primes in the Q3 unification, tying to the eight-tick octave via 24 = 8 × 3 and the count of non-DC DFT modes in that window. No open questions remain; the verification for 7 is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.