congruence_prime_11_is_passive_edges
plain-language theorem explainer
The theorem identifies the passive edge count of the Q3 graph as exactly 11 by subtracting one from its total of twelve undirected edges. Researchers tracing the geometric origins of Ramanujan congruence primes would cite this to anchor the prime 11 in the cube spectrum structure. The proof is a direct simplification that applies the definition of the edge count.
Claim. The passive edge count satisfies $E_ {passive} = |E(Q_3)| - 1 = 11$, where $Q_3$ denotes the cube graph whose undirected edge count equals twelve.
background
Q3_edge_count is defined as the constant 12, the number of undirected edges in the cube graph Q3. The double-entry ledger interpretation doubles this to 24 directed edges, which equals the directed flux count used throughout the module. The local setting is the Q3 unification of Ramanujan's mock theta orders {3,5,7} and congruence primes {5,7,11}, where 24 forces the split: 11 appears only among the congruence primes because it exceeds 8 while remaining coprime to 24. The upstream result from CubeSpectrum confirms the same edge count via the handshaking lemma on Q3 vertices and degree.
proof idea
The proof is a one-line wrapper that applies the definition of Q3_edge_count. The simp tactic substitutes the constant 12 and performs the arithmetic reduction to 11.
why it matters
This declaration assigns the geometric origin of the congruence prime 11 as the passive edge count E_passive = edges(Q3) - 1. It completes the module's trichotomy of origins for the set {5,7,11}: 5 from the phi-equation discriminant, 7 from non-DC DFT modes in the eight-tick window, and 11 from the passive edges. The result supports the claim that 24 = directed_flux(Q3) determines both mock orders and congruence primes, with the passive count seeding alpha inverse. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.