Transfinite propagationPaper & Lean formalization

The manuscript

The paper

Transfinite contractive propagation and the ball fixed point property in C(K)

Cleon S. BarrosoDepartment of Mathematics, Federal University of Ceará, Brazil

Open PDF ↗Download paper packageLaTeX source

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 C0-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.

Contents

  1. Introduction
  2. Transfinite contractive propagation systems
  3. Two-profile realization
  4. Inseparable families on compact F-spaces
  5. A single ordinal propagator and the BFPP characterization

Version in this site

This edition contains the author's final submission source, csb-BFPPCKsps-FV.tex, its matching 21-page PDF, and synchronized correspondence documentation (14 September 2026). It includes the Lean formalization paragraph and repository link. The mathematical statements and proofs are unchanged from the preceding editorial version.

Manuscript SHA-256:

feefe0f1af582753d5b22ada4baa01e87b1c1533706f47cd02d4c3c1b8ddc5ca

This is an author manuscript prepared for arXiv submission. The associated GitHub repository contains the Lean project and companion website.

How to read it with Lean

Start with the main characterization and the transfinite realization theorem. The source links open the exact declarations and their proofs. The correspondence map connects the intermediate constructions to their modules.

The formalization records mathematical results. Bibliographic attribution and the manuscript’s correspondence with those results require mathematical reading in addition to kernel checking.