AllDimensionalBoundaryAPI
plain-language theorem explainer
Packages the all-dimensional cubical boundary interface: every finite higher-dimensional chain of face certificates carries a second-boundary map into integer-valued functions on n-bit configurations, and that map is identically zero. Anyone citing the Delta-native cubical complex or the all-dimensional boundary headline uses this bundle. It is a pure structure definition, not a proved theorem.
Claim. An all-dimensional boundary API consists of (i) a second-boundary assignment sending each finite higher-dimensional chain $C$ in dimension $n$ to a function $\partial^2 C : \{\text{configs of $n$ binary distinctions}\} \to \mathbb{Z}$, and (ii) the square-zero law $\partial^2 C \equiv 0$ for every such chain.
background
In the Primitive Recognition Calculus, geometry is built from independent binary distinctions. A configuration of $n$ channels is a map $\mathrm{Fin}, n \to \mathrm{Bool}$: each channel sits on one side of its distinction. Higher-dimensional face certificates package the local cubical face data needed to form chains; a higher chain is simply a finite list of those certificates.
The second boundary of a chain is the pointwise integer sum of the second boundaries of its faces, evaluated on configurations. The algebraic demand is the classical cubical identity $\partial^2 = 0$: after two boundary steps the signed contributions cancel, so the display is the zero function on every configuration.
This module sits on the cubical chain complex layer of the foundation stack. Upstream canonical objects (trace closure repeating the primitive distinction act, arithmetic initiality, dyadic real protocols) fix the ambient recognition setting; the present structure only records the boundary API shape those layers feed.
proof idea
No proof body: this is a structure declaration. It names two fields, the second-boundary operator on higher chains and the square-zero axiom that the operator is identically zero as a function on configurations. Inhabitants are supplied elsewhere by pairing HigherChain.secondBoundary with the lemma that every finite higher chain has vanishing second boundary.
why it matters
Gives a single named interface for the all-dimensional $\partial^2 = 0$ law that the Delta-native cubical complex must satisfy. The immediate consumer is the canonical instance that wires the higher-chain second boundary and its vanishing lemma into this API, which then supports the all-dimensional cubical boundary headline: every finite higher-dimensional cubical chain whose second boundary decomposes into codimension-2 square contributions is null-homologous at the second step.
In the Recognition foundation this is the multi-dimensional extension of the primitive distinction calculus toward a genuine cubical chain complex, the combinatorial substrate on which higher recognition geometry (and eventually the forcing of $D = 3$ and the eight-tick octave) is stated. It does not itself force dimension or tick structure; it only freezes the boundary API those later steps quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.