Source and verification
This article explains family 177 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.
🏷️ From graph cuts to face expansion
A finite simplicial complex is a collection of finite vertex sets closed under taking subsets. A face with vertices has dimension . A pure -dimensional complex has every face contained in a -face.
Work with zero-one functions on faces, adding values modulo two. An -cochain records a selected set of -faces. Its coboundary records the -faces containing an odd number of selected -faces. Applying coboundary twice gives zero: each smaller face is encountered twice.
For , a cochain is a set of vertices, and its coboundary is exactly the graph cut. This is the elementary model for the higher-dimensional question.
🏷️ Weighted norms and the correct comparison space
Sample a top-dimensional face uniformly, then an -face within it uniformly. The resulting face weight is
The norm is the total weight of faces where . It is a probability, not an unnormalized face count.
Write for cocycles and for coboundaries. In degree zero, is defined to be the constant functions. The distance from to either space is the least weighted number of faces that must be changed to enter it.
Manuscript claim
For every fixed , there are connected pure -dimensional complexes with vertex counts tending to infinity and constants , such that each vertex belongs to at most top-dimensional faces and
The constants may depend on but not on , , or . (OpenAI, 2026)
The graph and two-dimensional cases are supplied by separate earlier results. The new theorem stated here begins at dimension three.
🏷️ Why vanishing is an additional requirement
An inequality against would say that a cochain with small coboundary is close to some cocycle. It would not eliminate cocycles that are not coboundaries.
If , then , whereas its distance from is positive in a finite complex with positive face weights. The claimed inequality therefore forces in every degree below . In topological language, the corresponding reduced cohomology vanishes.
The source separates two obligations: quantitative expansion towards cocycles and the qualitative equality of cocycles with coboundaries. They must hold for the same sequence of complexes. Combining an expansion theorem for one family with a vanishing theorem for an unrelated family would not suffice.
The degree condition also deserves care. Bounding the number of top faces through each codimension-one face is weaker than bounding the number through each vertex. Complexes with a complete lower-dimensional skeleton can satisfy the former condition while vertex degrees diverge. The theorem asserts the stronger vertex bound.
🏷️ Construction and local geometry
The manuscript builds finite quotients of one higher-dimensional complex, then takes their -dimensional skeleta. The ambient dimension is chosen larger, at , to leave room for the vanishing argument. The local building blocks are fixed finite objects, giving a uniform vertex-incidence bound, while the quotient sizes tend to infinity.
The construction uses polynomial matrices and congruence quotients. Those algebraic subjects are not developed here; their required outputs are concrete: growing finite complexes, fixed local incidence patterns, and vanishing in the stated range.
Geometrically, the infinite complex is filtered by layers inside an affine building. Each attachment is controlled by a finite opposition complex. Acyclicity of these attachments in the necessary range transfers the contractibility of the ambient building into partial homology vanishing for the constructed complex.
🏷️ From limiting information to each finite level
A delicate passage concerns the congruence tower. An available stability theorem initially gives information about an inverse system, not an immediate assertion at every level. The manuscript also obtains surjectivity of the relevant transition maps, using odd indices and coefficients modulo two.
The elementary principle is worth isolating. Suppose a system has surjective transition maps and is pro-zero, meaning that for each fixed level some later map into it is zero. A map that is both zero and surjective can have only the zero target. Hence each level vanishes. Without surjectivity, pro-zero information would not imply levelwise vanishing.
Further stabilization and averaging steps transfer the required vanishing to the finite quotient complexes. This is the principal qualitative input beyond the existing quantitative expansion theorem.
🏷️ Comparing skeleton weights
The quantitative theorem is first applied on a larger skeleton. Passing to the -skeleton changes the sampling weights: top faces are now -faces rather than chambers of the ambient complex.
Uniform upper and lower bounds on the number of chambers through a -face compare the two systems. The common normalization factor appears in successive cochain degrees and cancels in the expansion inequality, leaving constants independent of the quotient size. Finally, replacing by using vanishing gives the asserted coboundary expansion.
🏷️ Key steps and proof outlines
Separate the quantitative and qualitative inputs
The construction uses an ambient dimension and vertex types. Fix one sufficiently large odd prime power once and for all, and let be the resulting finite ambient complexes. The algebraic construction is needed for three precise outputs: a uniform local incidence pattern, quotient sizes tending to infinity, and homology vanishing through degree . The discussion below uses these outputs and explains how they enter the expansion proof, without developing the underlying matrix-group theory. (OpenAI, 2026)
The known quantitative expansion theorem applies to , the -skeleton of , and gives
with independent of . The manuscript verifies that its finite quotients preserve the required local pieces and their intersections. This is necessary because its quotient parameter is a power of a polynomial, rather than the irreducible-polynomial quotients in the cited construction. The expansion theorem is invoked only after those recognition conditions are checked.
Why an inverse-system theorem is not yet finite-level vanishing
The source first obtains stabilization maps between homology spaces of successive matrix sizes. Its available theorem says their cokernels form a pro-zero inverse system: for every fixed level , some later transition into that cokernel is zero. This alone permits nonzero individual cokernels.
A separate transfer map supplies surjectivity. The index between two congruence levels is odd, and coefficients are modulo two. The composition “transfer to the deeper level, then include back” multiplies a homology class by that odd index, hence is the identity over . Therefore the inclusion-induced transition is surjective, as are the induced transitions on cokernels.
Elementary closure principle
A pro-zero inverse system with surjective transition maps is zero at every level. For a fixed target level, choose a sufficiently late transition that is zero; being surjective too, it forces the target space to be zero.
Applying this to the stabilization cokernels gives ordinary surjectivity at each fixed level. The source then uses two spare coordinates to show that every elementary conjugation acts trivially on the relevant homology: every class can be represented on the complementary coordinates, where that conjugation does nothing. Generation transfers the conclusion to the full required action.
Finally, averaging over the finite odd-order quotient is exact over . Together with the trivial action, it identifies the congruence-level homology with the already vanishing homology of the ambient construction. The geometric comparison identifies this with for . Duality gives the cohomology vanishing. These are distinct steps: stability, surjectivity, trivial action, and averaging each remove a different possible obstruction.
Verify growth and the stronger vertex-degree bound
Write , a fixed number independent of . The construction gives exactly chambers through each vertex. A chamber containing a vertex has at most choices of a -face through that vertex. Hence the -skeleton has vertex incidence bound
This counts top-dimensional faces through a vertex, not merely faces through a codimension-one face. On the other hand, the finite quotient contains at least elements, and its type classes have size equal to the quotient size divided by . Thus
The same fixed local data therefore permits both unbounded size and bounded vertex incidence.
Compare the two sampling norms with a common factor
Let be any pure -complex and its -skeleton. Suppose each -face lies in between and chambers. Put
In degree , the skeleton’s uniform face weight is the ambient weight multiplied by , where counts chambers through that face. Averaging over containing -faces gives, in every lower degree,
The same comparison holds for distances to any common subspace. In the source, panel chamber counts are constant, so the weights on equal ambient weights; for -faces, . Consequently
The last step uses the preceding cohomology vanishing for ; in degree zero, connectedness and the augmented (reduced cohomology) convention give , the constant cochains. Thus in every required degree, and the common normalization cancels. Thus the final constant is independent of quotient size and cochain degree, as required.
See Also
- Ramanujan graphs treats spectral expansion in dimension one, with exact eigenvalue bounds.
- Thin spanning trees uses graph cuts and weighted quadratic forms, the degree-zero starting point for the present analogy.
🏷️ Manuscripts and verification scope
- Bounded-degree coboundary expanders in every dimension — pinned manuscript and companion source.
The family scope page describes selected formalization coverage. The page selects dimensions at least three, coefficients modulo two, bounded top-dimensional incidence at vertices, and expansion in every lower degree. The graph and two-dimensional cases are separate inputs. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.
OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.