Edge
plain-language theorem explainer
Four labeled, oriented sides of the unit square: bottom, top, left, right. This is the discrete edge basis for 1-chains in the multi-distinction square geometry. Anyone counting face boundaries, Gray-code flips, or cube-face tallies at D=3 cites it. The declaration is a plain inductive enumeration with decidable equality.
Claim. The oriented edge set of the square is the four-element type $\{B,T,L,R\}$ (bottom, top, left, right), equipped with decidable equality.
background
In MultiDistinctionGeometry the recognition square is treated as a single 2-cell whose combinatorial skeleton supports integer chain groups. Vertices are a separate type; edges are these four oriented sides. The module comment states that 0-chains and 1-chains are free abelian groups on those generators, while the 2-chain group is simply $\mathbb{Z}$ (one face).
A 1-chain is then a map from this edge type into $\mathbb{Z}$. The boundary of the face is the counterclockwise combination bottom $+$ right $-$ top $-$ left. That convention matches the usual singular or cubical orientation used later in CircleWindingChain and FaceWinding.
Upstream name collisions (other B, T, L, face symbols in cosmology and simplicial modules) are unrelated; here the four constructors are purely the square's sides.
proof idea
No proof: an inductive type with four nullary constructors, deriving DecidableEq and Repr. The mathematical content is the enumeration itself.
why it matters
This edge basis is the carrier for C1 (integer 1-chains) and for the boundary maps d1, d2 in the same module, including the identity $\partial^2=0$. Downstream, FaceWinding reads which bit flips along each edge of the Gray-code 8-cycle; CircleWindingChain uses oriented edge support for free singular 1-chains and cyclic family terms; AlphaDerivation's D=3 face count sits in the same cubical counting stack. In the RS forcing picture the square is the 2-skeleton piece that, once lifted to the 3-cube, feeds the eight-tick octave (T7) and the D=3 spatial count (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.