we-solve (beta)

Math-2600 · mathematics · Combinatorics

Bounded-degree coboundary expanders in each dimension at least three

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every integer $d>=3$, do constants $D,\epsilon >0$ and connected pure finite d-dimensional simplicial complexes with vertex counts tending to infinity exist such that each vertex belongs to at most D top faces and every $F_2$ cochain below top dimension satisfies ||delta $f||>=\epsilon $ dist(f,B)?

Short English statement

For every integer $d>=3$, do constants $D,\epsilon >0$ and connected pure finite d-dimensional simplicial complexes with vertex counts tending to infinity exist such that each vertex belongs to at most D top faces and every $F_2$ cochain below top dimension satisfies ||delta $f||>=\epsilon $ dist(f,B)?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2600-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2600

Bounded-degree coboundary expanders: The manuscript’s result quantifies over every d>=3 and supplies connected pure finite complexes with vertex count tending to infinity, bounded incident top faces at each vertex, and one epsilon for every 0<=i<d. The F_2 norm is the standard normalized top-face-induced weighted Hamming norm defined in eq:weights; B^0 consists of constants (augmented cochains). Those norm/B^0 conventions must accompany the displayed target for its notation to be precise.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

Bounded-degree coboundary expanders in each dimension at least three

OpenAI's claim

Bounded-degree coboundary expanders: For each $d\ge3$, the paper claims arbitrarily large finite $d$-complexes with bounded vertex incidence and positive $\mathbb F_2$ coboundary expansion in every lower degree. The constants may depend on the fixed dimension.

Mathematical statement of the claimed result

Mathematical claim 1.
For each integer $d\ge3$ there are finite connected pure $d$-dimensional simplicial complexes $X_m$ with $|X_m(0)|\to\infty$ and constants $D<\infty$, $\epsilon>0$ such that each vertex belongs to at most $D$ top faces. Over $\mathbb F_2$, put $w_i(\sigma)=\#\{\tau\in X_m(d):\sigma\subset\tau\}/(\binom{d+1}{i+1}|X_m(d)|)$ and $\|f\|_i=\sum_{f(\sigma)\ne0}w_i(\sigma)$. With $\delta_i f(\tau)=\sum_{\sigma\subset\tau,\ |\sigma|=i+1}f(\sigma)$, $B^i=\operatorname{im}\delta_{i-1}$ and $B^0$ the constants, the claimed inequality is \[\|\delta_i f\|_{i+1}\ge\epsilon\min_{b\in B^i}\|f-b\|_i\quad(0\le i<d).\] Constants are uniform in $m,i,f$, while depending on the fixed dimension.

Outline of the argument

Bounded-degree coboundary expanders: An infinite coset complex is built from a congruence subgroup of a polynomial special linear group over a fixed finite field. Its growing finite congruence quotients have fixed local groups, hence bounded degrees. Acyclicity and quotient cohomology vanishing are combined with local spectral expansion; taking the required skeleton preserves the normalized expansion inequalities.

Formal verification

Family 177 describes Lean coverage for the weighted coboundary inequalities for growing complexes in each fixed dimension at least three.

Bounded-degree coboundary expanders: The manuscript links CoboundaryExpanders.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →