TwoFaceCert
plain-language theorem explainer
A finite 2-face certificate packages one square face inside an n-channel distinction cube: a base configuration, two channel indices, and an integer coefficient. Anyone proving local cubical ∂²=0 cites this as the atomic ledger entry. The structure is pure data; the associated boundary-of-boundary map is the ambient face operator applied to those fields.
Claim. For $n\in\mathbb{N}$, a finite 2-face certificate is a tuple $(w_0,i,j,c)$ with base configuration $w_0:\{0,\ldots,n-1\}\to\{\mathrm{false},\mathrm{true}\}$, channel indices $i,j\in\{0,\ldots,n-1\}$, and coefficient $c\in\mathbb{Z}$. Its boundary-of-boundary is the integer-valued chain on configurations obtained by applying the ambient two-face boundary-squared operator at $(w_0,i,j)$ scaled by $c$.
background
The ambient space is the $n$-channel distinction cube. A configuration is a map $w:\mathrm{Fin},n\to\mathrm{Bool}$: each channel is an independent binary distinction (on one side or the other). Difference operators flip a single channel while holding the rest fixed; faces and their boundaries are built from those flips.
In this module the goal is a ledger-style cubical $\partial^2=0$ without a full singular homology API. A 2-face is the square spanned by two channels $i$ and $j$ at a fixed base vertex. The certificate records exactly the data needed to evaluate the ambient operator faceBoundaryBoundary on that square: base config, the two indices, and an integer weight.
Upstream, Config n is the configuration type; the boundary-of-boundary display is defined on that type. Related singular-simplex face maps appear elsewhere in the foundation stack, but here the geometry is purely cubical and discrete on the Boolean cube.
proof idea
No proof: this is a structure definition. Four fields (base, i, j, coeff) assemble the certificate. The companion projection TwoFaceCert.boundaryBoundary is a one-line wrapper that feeds those fields into MultiDistinctionGeometry.faceBoundaryBoundary. Downstream square-zero theorems then apply the ambient identity ambient_two_face_square_zero to each certificate.
why it matters
This is the atomic unit of the finite cubical $\partial^2=0$ ledger in Primitive Recognition Calculus. Parent results twoFaceCert_boundary_squared_zero and twoFaceCert_list_boundary_squared_zero show every single certificate and every finite list of them has vanishing boundary-of-boundary; finite_two_face_ledger_square_zero is the headline packaging that fact.
HigherFaceCert in AllDimensionalCubicalBoundary stores a List (TwoFaceCert n) as its codimension-2 ledger, so higher-dimensional face certificates reduce $\partial^2=0$ to finite sums of these squares. In the Recognition stack this is scaffolding for discrete chain-complex structure on multi-distinction geometry (the Boolean $n$-cube of independent distinctions), not yet the full forcing chain T0–T8, but a local algebraic prerequisite for recognition calculus on cubes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.