Transfinite contractive propagation and the ball fixed point property in \texorpdfstring{$C(K)$}{C(K)}
Cleon S. Barroso
math.FA
Sep 14, 2026 · v1
TL;DR
The paper's main results are formalized in a companion Lean 4 repository built on Mathlib, mapping each paper statement to its formal counterpart.
Abstract
We prove that, for a compact Hausdorff space $K$, the real Banach space $C(K)$ has the ball fixed point property if and only if $K$ is extremally disconnected. The new implication is obtained by constructing a fixed-point-free nonexpansive self-map of the whole closed unit ball whenever $K$ is a compact $F$-space which is not extremally disconnected. The construction uses a transfinite contractive propagation system with two increasing profiles. A successor–limit delay preserves their tail constraint and has no subsolution in the profile domain. Analysis records boundary deficits; positive operators on ordinal $C_0$-spaces and a common center determined by the two tails yield a nonexpansive synthesis satisfying an order domination inequality. The required topological families are obtained from a gap in a maximal Boolean chain in the zero-dimensional case, and from a transfinite extension of signs otherwise. The argument works in ZFC and resolves the question posed by Avilés, Japón, Lennard, Martínez-Cervantes, and Stawski.
Problem
Which compact Hausdorff spaces K make C(K) have the ball fixed point property, meaning every nonexpansive self-map of the closed unit ball has a fixed point? Avilés et al. asked whether this happens exactly when K is extremally disconnected. The open case was compact F-spaces that are not extremally disconnected.
Approach
For such K, the author builds a fixed-point-free nonexpansive self-map of the unit ball of C(K) from a transfinite contractive propagation system with two increasing profiles. A successor-limit delay operator preserves the tail constraint and admits no subsolution. Positive operators on ordinal C_0-spaces and a common center then give a nonexpansive synthesis. The required topological families come from a gap in a maximal Boolean chain (zero-dimensional case) or from a transfinite extension of signs (otherwise). A companion Lean 4/Mathlib formalization accompanies the results.
Results
In ZFC, C(K) has the ball fixed point property if and only if K is extremally disconnected, answering the question of Avilés, Japón, Lennard, Martínez-Cervantes and Stawski. The results are formalized in Lean 4 with Mathlib.
