mock_orders_sum_relation
plain-language theorem explainer
The sum 3 + 5 + 7 + 9 equals the directed flux of the Q₃ graph. Researchers linking Ramanujan's mock theta orders to partition congruences would cite this to anchor the mock set {3,5,7} plus 9 inside the flux value 24. The proof is a one-line simplification that unfolds the flux definition and the edge count.
Claim. $3 + 5 + 7 + 9 = 24$, where 24 is twice the number of undirected edges in the Q₃ graph.
background
The module shows that both mock theta orders {3,5,7} and congruence primes {5,7,11} are selected by the single integer 24 = directed_flux(Q₃). directed_flux_Q3 is defined as twice Q3_edge_count, and Q3_edge_count is defined as 12, so the flux equals 24. The upstream theorem Q3_edge_count from CubeSpectrum establishes the edge count via the handshaking lemma Q3_edges = Q3_degree * Q3_vertices / 2.
proof idea
The term proof applies simp to the definitions directed_flux_Q3 := 2 * Q3_edge_count and Q3_edge_count := 12, reducing the left-hand side directly to 24.
why it matters
This identity supplies the arithmetic link that lets the module equate the mock orders sum to the flux 24, which in turn forces the overlap {5,7} and the divergence at 3 and 11. It sits inside the Q₃ unification of Ramanujan data and connects to the eight-tick octave via 24 = 8 × 3. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.