C1
plain-language theorem explainer
Integer-valued 1-chains on the four oriented edges of the unit square. Anyone building the cubical chain complex for multi-distinction geometry cites this as the ambient group for ∂₂ and ∂₁. The declaration is a one-line type synonym Edge → ℤ.
Claim. Write $C_1$ for the free abelian group of 1-chains on the square: maps from the oriented edge set $\{B,T,L,R\}$ into $\mathbb{Z}$.
background
Multi-distinction geometry models a single square face with four vertices and four oriented edges. Edges are the inductive type with constructors bottom, top, left, right. The module sets up the elementary cubical chain groups over $\mathbb{Z}$: 0-chains are integer functions on vertices, 1-chains are integer functions on edges, and the 2-chain group is simply $\mathbb{Z}$ (one face).
This is the discrete precursor to the Recognition Composition Law and the eight-tick forcing chain: before J-cost or $\phi$ appear, one needs a chain complex whose $d^2=0$ identity encodes closed recognition loops. The square is the minimal 2-cell that can carry a nontrivial boundary cycle.
proof idea
Pure definitional abbreviation: $C_1$ is identified with the function type from the edge inductive type into the integers. No proof obligations.
why it matters
Feeds the boundary maps $d_2:C_2\to C_1$ and $d_1:C_1\to C_0$ in the same module, and the packaged squareBoundaryPair in CubicalChainComplex, which asserts $d_1\circ d_2=0$. Downstream gravity and geometry developments (Regge convergence, Cayley–Menger non-flatness) reuse the same edge-indexed integer coefficients when they need a discrete 1-skeleton. In the broader RS foundation this is scaffolding for closed observable frameworks: a finite, countable state of distinctions with no continuous moduli, matching the (C3) finite-description clause.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.