faceVertex
plain-language theorem explainer
Names the four corners of the oriented 2-face spanned by two binary channels inside an ambient n-cube: start from a base configuration and set channels i and j to chosen sides. Anyone writing discrete chains or checking ∂² = 0 on multi-distinction geometry cites it. The body is a double pointwise update of the base map.
Claim. Fix $n\in\mathbb{N}$, a base configuration $b:\{0,\ldots,n-1\}\to\{0,1\}$, channel indices $i,j$, and side choices $\beta_i,\beta_j\in\{0,1\}$. The face vertex is the configuration that equals $b$ off $\{i,j\}$ and takes values $\beta_i$ at $i$ and $\beta_j$ at $j$.
background
In this module a configuration of $n$ independent binary distinctions is a map $\mathrm{Config},n := \mathrm{Fin},n\to\mathrm{Bool}$: each channel sits on one of two sides. The ambient space is the $n$-dimensional binary cube. A 2-face is the square obtained by varying two channels $i$ and $j$ while holding the remaining channels fixed at a base configuration.
The discrete chain complex on that cube needs explicit 0-chains supported at the four corners of each such square. Those corners are exactly the four side pairs $(\beta_i,\beta_j)\in{0,1}^2$. The present definition packages one corner as a full ambient configuration so that indicator functions and signed sums can be written without ad-hoc casework.
Downstream, the oriented boundary-of-boundary 0-chain for the face is assembled from eight signed vertex indicators (two per edge of the square). That expression is left unsimplified so its vanishing is precisely the statement $\partial^2=0$ on every 2-face.
proof idea
Pure definition, not a proof. The body is the composition of two pointwise updates: first set channel $i$ of the base to $\beta_i$, then set channel $j$ of the result to $\beta_j$. No lemmas are invoked; Mathlib's Function.update supplies the map surgery.
why it matters
This is the vertex constructor for the multi-distinction chain complex. Its sole recorded consumer is faceBoundaryBoundary, which writes the eight-term 0-chain for the oriented 2-face spanned by $i$ and $j$ (bottom, right, top, left edges) and whose vanishing is the cancellation statement $\partial^2=0$ on every ambient binary cube.
In the Recognition foundation, configurations of independent binary distinctions are the primitive geometric objects before continuum limits or Clifford structure. Having named face vertices lets the discrete exterior calculus sit on the same cube that later feeds eight-tick and $D=3$ forcing arguments, without smuggling continuum topology. The definition itself closes no open question; it is scaffolding for the $\partial^2=0$ identity on 2-faces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.