thirteen_congruence_eligible
plain-language theorem explainer
13 satisfies the congruence-eligible predicate by being prime and coprime to 24. Number theorists extending Ramanujan congruences via the Q3 bridge cite this to place the next prime after 11 in the set {5,7,11}. The proof is a direct term construction that applies decidability to the two conjuncts of the predicate.
Claim. $13$ is a prime number satisfying $13$ coprime to $24$.
background
In the CongruenceQ3Bridge module a prime p counts as congruence-eligible exactly when it is coprime to 24. The definition therefore excludes 2 and 3, so the Ramanujan congruence primes become the three smallest primes greater than 3 that meet the coprimality test. The module derives both the mock-theta orders {3,5,7} and the congruence primes {5,7,11} from the single integer 24 = directed_flux(Q3), using the factorization 24 = 8 × 3 to separate the mock-only case 3 from the congruence-only case 11.
proof idea
The proof is a one-line term wrapper that builds the pair witnessing primality of 13 together with coprimality of 13 and 24. It discharges both conjuncts by invoking the decidability tactic on the concrete numeric predicates.
why it matters
The declaration adds 13 to the arithmetic list of congruence-eligible primes that the module unifies under the Q3 structure. It completes the explicit verification that {5,7,11} are precisely the smallest primes coprime to 24 and larger than 3, thereby supporting the claim that the Ramanujan offsets themselves are determined by the modular inverse of the directed flux count. In the Recognition framework the result sits inside the eight-tick octave (T7) that forces the period 24 and the spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.