# Bounded-degree coboundary expanders

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Bounded-degree coboundary expanders in every dimension](../../preprints/Bounded-degree-coboundary-expanders-in-every-dimension-September-24-2026/paper.pdf)

## Scope

The formalization constructs bounded-degree $\mathbb F_2$ coboundary expanders in every dimension $d\ge3$. For each such $d$, it gives finite pure connected $d$-dimensional simplicial complexes with vertex counts tending to infinity, one uniform bound on top-dimensional degree at each vertex, and one positive coboundary-expansion constant in every degree below $d$. The constants may depend on $d$. The graph and two-dimensional cases used for the paper's all-positive-dimensions conclusion are separate.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Bounded-degree coboundary expanders in dimensions at least three | [CoboundaryExpanders.lean](../ComparatorChallenges/CoboundaryExpanders.lean) |