HigherFaceCert
plain-language theorem explainer
A higher-dimensional cubical face certificate in an n-channel distinction cube packages an intended face dimension together with a finite ledger of codimension-2 square (2-face) certificates. Anyone proving ∂²=0 for all-dimensional finite cubical chains cites this carrier. It is a pure data structure: no proof content beyond field packaging.
Claim. For each channel count $n\in\mathbb{N}$, a higher-dimensional cubical face certificate consists of a natural number $\mathrm{dim}$ (the intended face dimension) and a finite list of 2-face certificates in the $n$-channel cube. Each 2-face certificate records a base configuration $w\in\{\mathrm{true},\mathrm{false}\}^n$, a pair of distinct channel indices, and an integer coefficient. The associated second-boundary display is the pointwise sum, over that list, of the boundary-of-boundary displays of the 2-face certificates.
background
The ambient setting is the Primitive Recognition Calculus cubical chain complex on $n$ independent binary distinctions. A configuration is a map $\mathrm{Config},n:=\mathrm{Fin},n\to\mathrm{Bool}$: each channel sits on one of two sides. The difference operators along channels generate the cubical faces of the distinction cube.
A 2-face certificate (from the cubical chain complex module) is a finite certificate of a single square: base configuration, two channel indices $i,j$, and an integer coefficient. Its boundary-of-boundary display is already known to vanish identically, which is the elementary $\partial^2=0$ identity on squares.
Higher faces need not be stored geometrically. For the second-boundary identity it is enough to keep the finite ledger of all codimension-2 square cancellations that the face induces. That is exactly what this structure records, together with a bookkeeping dimension field.
proof idea
Definitional packaging only: two fields, no axioms. The companion second-boundary map folds the ledger, summing each 2-face certificate's boundary-of-boundary display at a configuration $w$. Vanishing of that sum is not proved here; it is discharged later by applying the listwise 2-face $\partial^2=0$ lemma to twoFaceLedger.
why it matters
This is the atomic carrier for the all-dimensional finite cubical boundary API in the Delta plan. Downstream, every higher face has zero second boundary because its second boundary is a finite ledger of zero 2-face boundary-of-boundary terms. Finite lists of such certificates form higher chains, whose second boundaries likewise vanish by folding. The headline theorem packages both vanishings (and the matching API projection) as the all-dimensional finite $\partial^2=0$ statement required by the plan.
In the Recognition forcing chain this sits under the discrete geometric scaffolding that supports eight-tick and $D=3$ arguments: once cubical boundaries square to zero in every dimension on finite certificates, higher chain complexes can be used without analytic remainder terms. It does not itself force dimension or period; it supplies the algebraic hygiene those steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.