directed_edge_count
plain-language theorem explainer
The directed edge count for dimension d equals twice the undirected hypercube edge count, encoding bidirectional flows required by J-symmetry on the recognition ledger. Researchers reinterpreting the exponent 24 in Ramanujan's modular discriminant and the Leech lattice dimension cite this when separating the mathematical count from string-theory dimensional claims. The definition is a direct algebraic doubling of the cube_edges function.
Claim. For natural number $d$, the directed edge count is $2d·2^{d-1}$, obtained by doubling each undirected edge of the $d$-hypercube to account for both flow directions.
background
The module interprets the number 24 as the count of directed flux modes on the Q3 double-entry ledger rather than extra spatial dimensions. Cube_edges supplies the base count of undirected edges via the formula $d·2^{d-1}$, which for $d=3$ yields 12. The double-entry rule follows from J-symmetry: $J(x)=J(1/x)$ forces every flow to have a reciprocal, so each edge must be tracked in both orientations.
proof idea
One-line definition that applies cube_edges to the input dimension and multiplies the result by 2.
why it matters
This definition supplies the flux count used by directed_edges_Q3 to prove equality to 24 and by leech_dimension_eq_directed_flux to equate it with the Leech lattice dimension. It fills the T8 step (D=3 forced) while preserving the modular discriminant exponent as the partition function over 24 directed modes, correcting the string-theory reading of 24 transverse dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.