Functional analysis · Topology · Formal proof
Transfinite contractive propagation and the ball fixed point property in C(K)
Which compact Hausdorff spaces K ensure that every nonexpansive self-map of the closed unit ball of C(K, ℝ) has a fixed point? This paper proves that they are exactly the extremally disconnected spaces.
Explore the main results alongside their Lean statements, or download the manuscript and its formalization.
The ball fixed point characterization
Theorem 1.2 · Corollary 5.4Mathematical statement
Let K be a compact Hausdorff space. The real Banach space C(K) has the ball fixed point property if and only if K is extremally disconnected.
⟺
K is extremally disconnected.
Here BFPP concerns every nonexpansive self-map of the whole closed unit ball, equipped with the supremum norm. Extremal disconnectedness means that the closure of every open set is open.
theorem hasBFPP_iff_extremallyDisconnected [T2Space K] :
HasBFPP C(K, ℝ) ↔ ExtremallyDisconnected KContext: namespace BFPP; K : Type*; [TopologicalSpace K] [CompactSpace K]
Read the Lean statement
[CompactSpace K] is supplied by the surrounding context, and [T2Space K] expresses the Hausdorff assumption. C(K, ℝ) is mathlib’s space of real continuous functions with its supremum norm.
HasBFPP quantifies over all maps of the closed unit ball and all proofs that their Lipschitz constant is at most one. The symbol ↔ records both implications. The proof of the extremally disconnected case is included in the project, using lattice suprema and invariant intervals.
A transfinite fixed point obstruction
Theorem 5.2Mathematical statement
Suppose that K is a compact Hausdorff F-space which is not extremally disconnected. There are an uncountable regular initial ordinal κ, a nonempty closed bounded convex set
and nonexpansive maps
𝒥 : 𝒟 → BC(K, ℝ),
𝒫 : 𝒟 → 𝒟,
such that 𝒫 is a transfinite contractive propagator and both 𝒜 ∘ 𝒥 ∘ 𝒫 and T = 𝒥 ∘ 𝒫 ∘ 𝒜 have no fixed points.
theorem exists_transfinite_realization (hF : IsFSpace K) (hED : ¬ ExtremallyDisconnected K) :
∃ κ : Ordinal.{u}, κ.card.ord = κ ∧ κ.card.IsRegular ∧ ℵ₀ < κ.card ∧
∃ D : Set (BoundedFamily (OrdinalIndex κ)),
D.Nonempty ∧ IsClosed D ∧ Bornology.IsBounded D ∧ Convex ℝ D ∧
∃ (A : UnitBall C(K, ℝ) → D) (J : D → UnitBall C(K, ℝ)) (P : D → D),
LipschitzWith 1 A ∧ LipschitzWith 1 J ∧ LipschitzWith 1 P ∧ IsTCP D P ∧
(∀ z, A (J (P z)) ≠ z) ∧
LipschitzWith 1 (fun f => J (P (A f))) ∧ (∀ f, J (P (A f)) ≠ f)Context: namespace BFPP; open Set Order Cardinal; universe u; K : Type u; [TopologicalSpace K] [CompactSpace K] [T2Space K]
Read the Lean statement
The only topological hypotheses beyond compactness and Hausdorffness are hF : IsFSpace K and hED : ¬ ExtremallyDisconnected K. The domain and all three maps are constructed in the conclusion.
κ.card.ord = κsays that the ordinal is initial;κ.card.IsRegularasserts regularity;ℵ₀ < κ.cardasserts uncountability.D.Nonempty,IsClosed D,Bornology.IsBounded D, andConvex ℝ Dstate the four required properties of the coefficient domain.IsTCP D Prequires a constant initial coordinate, nonexpansive rules on actual successor prefixes, and an upper or lower envelope at every nonzero limit.∀ z, A (J (P z)) ≠ zexcludes coefficient fixed points. The last line independently records nonexpansiveness and the absence of fixed points on the whole unit ball.
BoundedFamily (OrdinalIndex κ) realizes ℓ∞(κ). The discrete topology in this definition applies only to the coefficient index set; the topology of K remains arbitrary under the stated assumptions.
The obstruction also acts on the complex ball
Remark 5.5Mathematical statement
For every compact Hausdorff space K which is not extremally disconnected, there exists a fixed-point-free nonexpansive map
The construction takes real parts, applies the real map, and includes its output in the complex space. This result is the non-extremally-disconnected implication for complex scalars.
theorem exists_complex_fixedPointFree_of_not_ED [T2Space K] (hK : ¬ ExtremallyDisconnected K) :
∃ S : UnitBall C(K, ℂ) → UnitBall C(K, ℂ), LipschitzWith 1 S ∧ ∀ f, S f ≠ fContext: namespace BFPP; universe u; K : Type u; [TopologicalSpace K] [CompactSpace K]
Read the Lean statement
The theorem assumes ¬ ExtremallyDisconnected K and returns an actual map S. The real-part map is nonexpansive, and the inclusion of real functions is isometric. A fixed point of their composite would give a fixed point of the real construction.
The equivalence displayed in the first result is a statement about C(K, ℝ). The complex theorem displayed here makes only the implication written in its conclusion.
Inside the construction
Separate the metric estimate from the obstruction
The discrete recurrence in Subsection 1.2 of the paper provides the starting point:
Its transfinite counterpart combines rules at successor ordinals with tail envelopes at limit ordinals. The proof first builds a two-profile domain with a successor–limit delay. The delay preserves the tail constraint, but no admissible pair is a subsolution.
Analysis detects boundary deficits. Synthesis uses positive operators on ordinal C₀-spaces and a shared center. In the two-profile model, the comparison inequality 𝒜𝒥z ≤ z turns a hypothetical fixed point into a forbidden subsolution. An affine isometric encoding then places the construction on a single ordinal.
The necessary topological families come from a Boolean gap in the zero-dimensional case, and from transfinite sign extension in the remaining case. The F-space condition forces the cofinal lengths to be uncountable.