congruence_primes_product
plain-language theorem explainer
The arithmetic identity establishes that the product of the three smallest primes coprime to 24 and exceeding 3 equals 385. Researchers examining Ramanujan partition congruences or the Q3-directed flux lattice in Recognition Science would cite this result. The proof is a direct numerical normalization that evaluates the multiplication without invoking further lemmas.
Claim. The product of the congruence primes satisfies $5 × 7 × 11 = 385$.
background
The module unifies Ramanujan's mock theta orders {3,5,7} with congruence primes {5,7,11} through the single integer 24, identified as directed_flux(Q3). Congruence primes are defined as the three smallest primes p satisfying gcd(p,24)=1 and p>3, so that 5,7,11 arise while 3 is excluded by divisibility and 11 exceeds the 8-tick window. Upstream results supply the basic constants one in LogicInt, LogicRat, Spin, and PhiClosed, together with the point constructor for rational intervals; these underwrite the numerical arithmetic performed by norm_num.
proof idea
This is a one-line wrapper that applies the norm_num tactic to evaluate the product directly.
why it matters
The declaration supplies the explicit product value required to locate the Ramanujan offset one above the flux-lattice point 16×24+1. It closes the arithmetic step inside the module's unification of mock theta orders and partition congruences, where 24=8×3 forces the observed overlap and divergence between the two sets. No downstream theorems yet depend on it, and it touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.