HigherChain
plain-language theorem explainer
A higher chain in an n-channel cube is simply a finite list of higher-dimensional face certificates. Anyone citing the all-dimensional cubical ∂²=0 API or the Delta-native boundary package will use this type. The declaration is a one-line type synonym for List of those certificates; no proof content.
Claim. For each natural number $n$, a higher-dimensional chain is a finite list of higher-dimensional face certificates in the $n$-channel cube (each certificate carrying a face dimension and a ledger of codimension-2 square cancellations).
background
In the primitive recognition calculus, an $n$-channel configuration is a map from $n$ binary distinction channels to sides (Bool). Cubical faces in that cube are certified not by full geometric data but by finite ledgers of codimension-2 square cancellations, which is enough to display the second boundary.
A higher-dimensional face certificate records an intended face dimension together with a list of two-face certificates. Its second-boundary display is the sum of the boundary-of-boundary displays of those squares. The present abbreviation packages finitely many such face certificates into a single chain object, the natural domain for an all-dimensional second-boundary map.
The module sits in the Foundation layer that builds a Delta-native cubical boundary API: every finite higher chain should have vanishing second boundary, the cubical form of $\partial^2=0$.
proof idea
Pure definition: the abbreviation equates a higher chain of dimension parameter $n$ with a List of higher face certificates at that $n$. No tactics, no lemmas. Downstream code defines the chain second boundary by folding the face second-boundary displays and proves vanishing by induction on the list.
why it matters
This type is the carrier for the all-dimensional finite boundary API required by the Delta plan. It is the domain of HigherChain.secondBoundary and of the theorem that every finite higher chain has zero second boundary. That theorem, together with the face-level vanishing result, assembles into the headline that every finite higher-dimensional cubical chain with second boundary decomposed into codimension-2 square certificates has vanishing second boundary.
Downstream, the canonical Delta-native API packages the chain second-boundary map and the square-zero law, and the headline conjunction cites both face and chain vanishing. In Recognition terms this is scaffolding for multi-channel distinction geometry underlying the forcing chain's dimensional and octave structure, not yet a full singular homology computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.