mock_and_congruence_unified_by_Q3
plain-language theorem explainer
The theorem establishes that Ramanujan's mock theta orders {3,5,7} and congruence primes {5,7,11} are both forced by the single integer 24 equal to directed_flux(Q3). Number theorists studying mock modular forms or partition congruences would cite this for its unification of the two classical lists via one arithmetic parameter. The proof assembles the six-part conjunction by direct application of the mock-order characterization, coprimality facts, overlap lemma, divisibility, norm_num, and modular-inverse certificate.
Claim. The mock theta orders are exactly the primes satisfying $p=3$ or $p=5$ or $p=7$; the primes 5, 7, 11 are each coprime to 24; the primes that are both mock orders and congruence-eligible are exactly 5 and 7; 3 divides the directed flux of $Q_3$; 11 exceeds 8; and the Ramanujan offsets satisfy $24·4≡1 mod 5$, $24·5≡1 mod 7$, $24·6≡1 mod 11$.
background
IsMockOrder(p) holds precisely when p is prime, coprime to 8, and p<8, capturing primes that cannot close a k-periodic pattern inside one 8-tick window and therefore produce mock rather than true modular symmetry. IsCongruenceEligible(p) holds when p is prime and coprime to 24, i.e., neither 2 nor 3. The module sets out to explain the classical lists {3,5,7} and {5,7,11} by tracing both to the single number 24 = directed_flux(Q3), with 24=8×3 separating the mock-only prime 3 (divides 24) from the congruence-only prime 11 (exceeds 8).
proof idea
The tactic proof constructs the six-way conjunction by applying IsMockOrder_iff for the mock-order characterization, congruence_primes_coprime_24 for the coprimality conditions, overlap_is_exactly_5_7 for the intersection, three_divides_directed_flux for the divisibility, norm_num for the inequality 11>8, and congruence_offsets_are_flux_inverses for the modular-inverse relations on the offsets.
why it matters
This declaration supplies the main unification theorem of the RamanujanBridge module, showing both classical lists arise from the same Q3 directed-flux count. It draws directly on the eight-tick octave (T7) of the forcing chain, where the period-8 window defines the mock-order bound p<8, and on the spectral emergence of Q3 that produces exactly 24 chiral fermion flavors. The result supports the broader claim that Ramanujan's arithmetic patterns originate in the geometric structure of Q3; the physical reading of the flux remains a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.