finite_two_face_ledger_square_zero
plain-language theorem explainer
Every finite ledger of certified 2-faces on an n-channel distinction cube has vanishing total boundary-of-boundary. Anyone citing the cubical ∂²=0 law at the finite-certificate level uses this headline. The proof is a one-line reexport of the list-induction lemma that already sums local square-zero identities.
Claim. For every $n \in \mathbb{N}$ and every finite list of 2-face certificates on the $n$-channel distinction cube, the pointwise sum of their boundary-of-boundary chains is the zero function on configurations: $\sum_F \partial\partial F \equiv 0$.
background
In the primitive recognition calculus, an $n$-channel configuration is a map $\mathrm{Fin}, n \to \mathrm{Bool}$: each channel is a binary distinction. The multi-distinction geometry supplies face operators and a boundary-of-boundary map on pairs of channels.
A two-face certificate packages a base configuration, two channel indices $i,j$, and an integer coefficient. Its boundary-of-boundary is the integer-valued chain obtained by applying the geometric $\partial\partial$ operator at that face. The local cubical identity already gives $\partial\partial = 0$ on each such face.
This module assembles those local certificates into finite ledgers without a full homology API. The upstream list lemma states that any finite list of certificates has zero total boundary-of-boundary by additive induction on the list.
proof idea
One-line term wrapper: apply twoFaceCert_list_boundary_squared_zero at the given $n$ and face list. That upstream lemma proceeds by induction on the list (nil case is funext to the zero function; cons case adds a single face whose own $\partial\partial$ vanishes and uses the inductive hypothesis). No extra algebra is done here.
why it matters
Doc-comment frames this as the finite cubical certificate headline: the local square-zero law is stable under finite collections of certified 2-faces, the strongest all-finite strengthening available without a homology API.
Downstream it feeds strongClosureCertificate in Delta-native strong closure, which assembles the closed Delta-native theorem surface (real forgetful display, generable carrier, certified analytic and transformer protocols). In the Recognition foundation this is the discrete cubical $\partial^2=0$ fact supporting chain-level consistency of multi-distinction geometry, prior to continuum or forcing-chain physics (T5–T8).
It does not open new physics constants; it closes a scaffolding gap so finite 2-face ledgers can be cited as identically closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.