Vtx
plain-language theorem explainer
Four named vertices label the configurations of two binary channels on a square. Anyone building the multi-distinction complex, its oriented edges, or the 0- and 1-chains cites this carrier type. It is a plain inductive enumeration with decidable equality, not a proved statement.
Claim. The vertex set of the square is the four-point set $\{v_{00}, v_{01}, v_{10}, v_{11}\}$, one point for each configuration of two binary channels.
background
In the multi-distinction geometry module, two independent binary channels are treated as coordinates on a square. Each corner is a joint configuration: both off, first off and second on, first on and second off, or both on. The inductive type simply names those four corners.
The same module introduces oriented edges of the square (bottom, top, left, right) and the elementary cochain data $C^0$, $C^1$ with coboundaries $d_1$, $d_2$. The square is the smallest nontrivial multi-channel complex on which one can check $d^2=0$ and define vertex indicator functions.
Upstream name collisions (diamond lattice vertices in cosmology, trace-logic bottom/top, exp/log field $T$) share spelling only; the local meaning is the four two-channel configurations stated in the doc-comment.
proof idea
No proof. The declaration is an inductive type with four nullary constructors and derived DecidableEq and Repr instances. There is no tactic block or term obligation beyond the inductive specification itself.
why it matters
This carrier underpins the square complex used for multi-channel distinction calculus: edges, 0- and 1-cochains, the identity $d^2=0$, and vertex indicators all quantify over these four points. Downstream cosmology modules reuse the name for diamond-ball lattice points (centre, height, descent, edge lists), so the square vertices are the discrete prototype for interface geometry built from forced distinctions.
In the Recognition Science foundation layer this is scaffolding for primitive recognition calculus rather than a forcing-chain step (T5–T8). It fixes the finite state space on which multi-distinction boundaries and polarized interfaces are later counted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.