DirectedEdge
plain-language theorem explainer
DirectedEdge encodes an oriented pair of distinct vertices on the Q3 hypercube as a record with source and target in Fin 8 plus an inequality witness. Lattice modelers and string theorists reinterpreting the Ramanujan discriminant would cite it when counting the 24 directed flux channels on the double-entry ledger. The declaration is a plain structure definition that directly packages the adjacency condition without further computation.
Claim. A directed edge on the $Q_3$ hypercube is a triple $(s,t,a)$ where $s,t$ are elements of the 3-bit vertices (identified with Fin 8) satisfying $s ≠ t$, with $a$ the witness of adjacency.
background
The module reinterprets the exponent 24 in Ramanujan's modular discriminant Δ(τ) = η(τ)^24 as the number of directed flux degrees of freedom on the Q3 ledger. Q3 is the 3-dimensional hypercube with 8 vertices (the 8-tick positions) and 12 undirected edges; J-symmetry from the Recognition Composition Law forces each edge to carry flow in both directions, producing exactly 24 directed channels. Upstream, SpectralEmergence.of shows that the same Q3 structure simultaneously forces the gauge group SU(3)×SU(2)×U(1), three particle generations, and 24 chiral fermion flavors (= D × 2^D).
proof idea
This is a structure definition with no proof body. The three fields are introduced directly: source and target range over Fin 8, while adjacent is the proposition source ≠ target.
why it matters
The structure supplies the atomic object needed to count directed edges on the D=3 ledger, yielding the 24 that matches the Ramanujan tau function and Leech lattice dimension. It supports the RS claim (T8 and DIMENSIONAL_RIGIDITY) that 24 arises from double-entry flux on three spatial dimensions rather than 26 spacetime dimensions. Sibling declarations such as directed_edge_count and leech_dimension_eq_directed_flux build directly on this type to close the counting argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.