vertexIndicator
plain-language theorem explainer
Integer Kronecker indicator on the vertices of an n-channel binary cube: it returns 1 when the probe configuration equals a fixed vertex and 0 otherwise. Anyone assembling 0-chains for face boundaries in multi-distinction geometry cites it. The body is a one-line equality test into ℤ.
Claim. Fix $n\in\mathbb{N}$ and two configurations $a,w$ of $n$ independent binary channels (maps $\mathrm{Fin}\,n\to\{\mathrm{true},\mathrm{false}\}$). The vertex indicator is the integer $1$ if $w=a$ and $0$ otherwise.
background
In MultiDistinctionGeometry, a configuration is an assignment of a side to each of $n$ independent binary distinctions: $\mathrm{Config},n := \mathrm{Fin},n \to \mathrm{Bool}$. The ambient space is the $n$-dimensional binary cube whose vertices are these configurations.
The module builds discrete chains on that cube so that oriented 2-faces (pairs of channels) have well-defined boundaries. Vertices are the 0-skeleton; an integer-valued function on configurations is a 0-chain. The indicator isolates a single vertex as a basis 0-chain.
Downstream, the boundary-of-boundary expression for a 2-face is written as a signed sum of eight such indicators at the four corners of the face (each corner appears twice with opposite orientation).
proof idea
Pure definition: compare the two configurations by Boolean equality and emit $1$ or $0$ in $\mathbb{Z}$. No lemmas, no tactics.
why it matters
This is the atomic 0-cochain used to expand $\partial^2$ on every oriented 2-face of the multi-distinction cube. The immediate consumer is faceBoundaryBoundary, whose doc-comment states it is "the eight vertex terms contributed by the four oriented edges" and that its zero theorem is the cancellation $\partial^2=0$ for every 2-face in every ambient binary cube.
In the Recognition foundation, multi-distinction geometry is the discrete setting in which independent binary channels generate the cube whose homology underwrites the eight-tick octave structure (period $2^3$) and the forcing of $D=3$. A clean vertex basis is required before one can state that the discrete exterior derivative squares to zero on faces spanned by channel pairs.
It does not itself prove $\partial^2=0$; it only supplies the coefficients that make that identity a finite integer cancellation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.