higherChain_secondBoundary_zero
plain-language theorem explainer
Every finite list of higher-dimensional face certificates has vanishing second boundary as a function on configurations. Algebraic topologists and RS foundation workers cite this when assembling the all-dimensional cubical boundary API. The proof is list induction: the empty chain is zero by definition, and the cons case adds a face whose second boundary is already zero to an inductive remainder that is zero.
Claim. For every natural number $n$ and every finite chain $C$ of higher-dimensional face certificates in dimension $n$, the second-boundary functional of $C$ is the zero map on configurations: $\partial^2 C \equiv 0$.
background
In the Primitive Recognition Calculus, a higher-dimensional face certificate packages a finite ledger of codimension-2 square (2-face) certificates. Its second boundary is the pointwise sum of those 2-face boundary-of-boundary terms on configurations Config n. A higher chain is simply a finite list of such face certificates; its second boundary is the fold of the individual second boundaries, starting from zero.
The sibling result higherFace_secondBoundary_zero already shows each face certificate has zero second boundary, because that second boundary is a finite ledger of zero 2-face $\partial^2$ terms. The present statement lifts that vanishing from single faces to arbitrary finite chains, which is the chain-level half of the all-dimensional cubical boundary package imported from CubicalChainComplex.
Locally this sits in the Foundation layer that supplies discrete cubical homology identities needed by the Delta plan, before Clifford or Hamiltonian bridges are invoked.
proof idea
Induct on the list structure of the higher chain. For the empty list, funext plus simplification of the fold definition gives the zero function. For cons F rest, apply funext at a configuration $w$, invoke higherFace_secondBoundary_zero on the head face $F$ (via congrFun), and the inductive hypothesis on rest. Simplify the fold-cons form of HigherChain.secondBoundary with those two zero summands to conclude the total is zero.
why it matters
This is the chain-level square-zero law for all-dimensional cubical boundaries in RS. It is wired directly into deltaCubicalBoundaryAPI as the square_zero field, and it is the middle conjunct of all_dimensional_cubical_boundary_headline, which states the full finite boundary API required by the Delta plan: every higher face, every higher chain, and the Delta-native API all have vanishing second boundary.
In the broader framework this is discrete homology bookkeeping supporting the recognition calculus that underwrites the forcing chain (eight-tick octave, $D=3$), not a continuum Stokes theorem. Closing $\partial^2=0$ at every finite dimension keeps the cubical ledger consistent before mass-ladder or coupling extractions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.