twoFaceCert_list_boundary_squared_zero
plain-language theorem explainer
Any finite list of certified 2-faces in an n-channel distinction cube has vanishing total boundary-of-boundary: the fold of their individual ∂² contributions is the zero function on configurations. Homology and cubical-complex arguments in the Primitive Recognition Calculus cite this as the additive finite-ledger form of local ∂²=0. The proof is list induction, reducing each cons step to the single-certificate square-zero law.
Claim. For every $n \in \mathbb{N}$ and every finite list $F_1,\ldots,F_k$ of two-face certificates in the $n$-channel distinction cube, the configuration-wise sum $\sum_{\ell=1}^{k} (\partial\partial F_\ell)(w)$ equals $0$ for all configurations $w$. Equivalently, the fold of the certificates' boundary-of-boundary maps is the zero function.
background
In MultiDistinctionGeometry, 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. Face and difference operators act by flipping designated channels while holding the rest fixed, giving a cubical calculus of distinctions rather than a classical singular complex.
A TwoFaceCert packages a base configuration, two channel indices $i,j$, and an integer coefficient. Its boundary-of-boundary map is the ambient two-face operator faceBoundaryBoundary evaluated at those data. The single-certificate theorem already states that this map is identically zero: every finite 2-face certificate has zero boundary-of-boundary.
The present result lifts that local identity to finite additive ledgers. No full chain-complex or homology API is assumed; only lists of certificates and pointwise integer addition on configuration functions.
proof idea
Term-mode proof by induction on the list of certificates.
- Nil case: the fold is the constant-zero accumulator;
funextandsimpgive the zero function. - Cons case: apply
funextat a configuration $w$. The head certificate contributes zero bycongrFunoftwoFaceCert_boundary_squared_zero; the tail contributes zero by the inductive hypothesis.simpwithList.foldl_consassembles the sum to zero.
No geometric recomputation occurs here; additivity of the fold plus the single-face square-zero law suffice.
why it matters
This is the additive finite-certificate form of local cubical $\partial^2=0$ in the Primitive Recognition Calculus. Downstream, finite_two_face_ledger_square_zero is the headline wrapper: every finite 2-face ledger has zero total boundary-of-boundary, the strongest all-finite-2-face statement available without a full homology API.
It also discharges the higher-dimensional step: higherFace_secondBoundary_zero reduces a higher-face certificate's second boundary to a finite ledger of 2-face boundary-of-boundary terms and invokes this theorem to conclude that ledger vanishes. That closes the inductive bridge from certified 2-faces to all-dimensional face certificates in the cubical boundary complex.
In the Recognition foundation this underwrites a discrete, certificate-level chain complex on multi-distinction cubes, the combinatorial substrate for later forcing and recognition composition, without committing to classical singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.