← All papers
Expanders prevent Property (H)
math.FA
Sep 18, 2026 · v1
math.GT math.MG math.OA
TL;DR
Provides a Lean verification of the theorem that expander graphs equi-coarsely embedding into a Banach space prevent Property (H).
Abstract
We show that if a sequence of expander graphs equi-coarsely embeds into a Banach space, then this Banach space fails Kasparov and Yu's Property (H). Consequently, no Banach space with Property (H) can be coarsely universal for all countable groups. We provide a Lean verification of our results.
Problem
Kasparov and Yu's Property (H) for Banach spaces implies the Novikov conjecture for countable groups coarsely embedding into such spaces, raising the question of whether every countable group embeds into a Property (H) space.
Approach
The authors show that if a sequence of expander graphs equi-coarsely embeds into a Banach space, then that space fails Property (H). The proof uses the Poincaré inequality satisfied by expanders together with truncation and rescaling of coarse embeddings. The results are formally verified in Lean.
Results
No Banach space with Property (H) can be coarsely universal for all countable groups, since expanders obstruct coarse embedding into Property (H) spaces. The main results were verified in Lean.