arxiv: 2605.08274 · v2 · submitted 2026-05-08 · 🧮 math.LO

Recognition: 2 theorem links

· Lean Theorem

Bourbaki--Zorn Normal Forms for Maximality Arguments

You-Chang Liu

Pith reviewed 2026-05-13 07:50 UTC · model grok-4.3

classification 🧮 math.LO

keywords Bourbaki-Witt theoremfixed-point theoremsZorn maximalitypartially ordered setswell-ordered subsetsleast upper boundsprogressive mapsmaximal elements

0 comments

The pith

Least upper bounds for nonempty well-ordered subsets suffice to force fixed points for every progressive self-map on a poset.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper isolates the minimal completeness condition needed for Bourbaki-Witt fixed-point theorems by defining Bourbaki towers as well-ordered sequences built by applying the map at successors and taking least upper bounds at limits. It proves that the existence of least upper bounds just for nonempty well-ordered subsets is enough to produce a largest such tower whose bound is a fixed point inside the tower. This yields both the fixed-point result under a strictly weaker hypothesis than chain completeness and, via an additional selector on upper cones, a maximality principle that every such poset contains a maximal element. A reader cares because the argument makes explicit a reusable architecture that separates the well-ordered case from stronger completeness assumptions used in standard Zorn-type proofs.

Core claim

Given a progressive self-map on a partially ordered set, a Bourbaki tower is a well-ordered trajectory whose successor stages are generated by the map and whose limit stages are given by least upper bounds of earlier stages. If every nonempty well-ordered subset has a least upper bound, then a largest Bourbaki tower exists, its least upper bound belongs to the tower, and that bound is a fixed point of the map. Consequently no strictly progressive self-map can exist, and the same hypothesis plus a choice selector on strict upper cones implies the poset has a maximal element.

What carries the argument

A Bourbaki tower: a well-ordered trajectory in the poset whose successors are obtained by applying the progressive map and whose limits are least upper bounds of earlier stages; the argument constructs a largest one and shows its least upper bound lies inside it and is fixed.

If this is right

Every progressive self-map has a fixed point.
No strictly progressive self-map can exist.
The poset has a maximal element once a choice selector on strict upper cones is added.
The fixed-point theorem holds under well-ordered completeness rather than full chain completeness.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same tower construction might be adapted to prove fixed points when completeness is assumed only for countable well-ordered subsets.
The obstruction to strictly progressive maps could be used to derive choice-free versions of other maximality results in algebra.
The normal-form view suggests that many Zorn-style proofs can be rewritten by first building the well-ordered tower and only then invoking choice on the remaining cones.

Load-bearing premise

That a largest Bourbaki tower exists and that the least upper bound of the entire tower is itself an element of the tower.

What would settle it

A concrete poset in which every nonempty well-ordered subset has a least upper bound, yet some progressive self-map has no fixed point, or the poset has no maximal element.

read the original abstract

We isolate a normal-form mechanism underlying Bourbaki--Witt fixed-point arguments and least-upper-bound versions of Zorn-type maximality principles. Given a progressive self-map on a partially ordered set, we define a Bourbaki tower as a well-ordered trajectory whose successor stages are generated by the map and whose limit stages are given by least upper bounds of earlier stages. We prove that least upper bounds for nonempty well-ordered subsets are sufficient to force a fixed point for every progressive self-map. Thus the fixed-point statement is obtained under a weaker completeness hypothesis than the usual chain-complete form of the Bourbaki--Witt theorem. The proof proceeds by constructing a largest Bourbaki tower. The least upper bound of this largest tower belongs to the tower itself and is a fixed point of the map. As a consequence, strictly progressive self-maps cannot exist in such posets. Combining this obstruction with a choice selector on strict upper cones yields a concise maximality principle: if every nonempty well-ordered subset has a least upper bound, then the poset has a maximal element. The contribution is methodological rather than axiomatic. The paper makes explicit a reusable proof architecture connecting well-ordered Bourbaki--Witt fixed points, strict progression obstructions, and least-upper-bound versions of Zorn-type maximality arguments.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper extracts an explicit normal-form for Bourbaki towers that lets fixed-point results run on well-ordered lubs alone, but the largest-tower construction needs checking to rule out circularity with the later maximality step.

read the letter

The main takeaway is that least upper bounds on nonempty well-ordered subsets suffice for the Bourbaki-Witt fixed-point theorem on progressive maps. The paper reaches this by defining Bourbaki towers as well-ordered trajectories closed under the map at successors and under lubs at limits, then showing a largest such tower exists whose lub is a fixed point. From there it blocks strictly progressive maps and, with a choice selector on upper cones, gets a Zorn-style maximality principle under the same weak hypothesis. That normal-form architecture and the explicit reduction are the genuinely new pieces; they are not spelled out in the usual citations of Bourbaki-Witt or Zorn. The write-up is clean on the reusable proof structure and does a good job separating the fixed-point obstruction from the maximality conclusion. The soft spot is exactly the one the stress-test flags: the argument asserts a largest tower whose lub stays inside the tower, but it is not obvious from the abstract how that maximality is secured using only well-ordered lubs. If the construction proceeds by transfinite recursion that stabilizes inside the poset, or by showing unions of tower chains remain towers, it works; if it leans on an unstated appeal to maximal towers, the later derivation of maximality becomes circular. The abstract does not resolve this, so the full text has to be checked there. This is for order theorists or people who apply fixed-point theorems and want sharper hypotheses. It is a methodological clarification rather than a big reorganization, but the architecture is honest and the claims are internally consistent on the given assumptions. It deserves a serious referee to verify the tower construction and confirm the normal form is not already implicit in the literature.

Referee Report

1 major / 2 minor

Summary. The manuscript isolates a normal-form mechanism for Bourbaki-Witt fixed-point arguments and least-upper-bound versions of Zorn-type maximality principles. Given a progressive self-map on a poset, a Bourbaki tower is defined as a well-ordered trajectory with successors generated by the map and limit stages given by lubs of earlier stages. The central claim is that lubs for nonempty well-ordered subsets suffice to force a fixed point for every progressive self-map, obtained as the lub of a largest Bourbaki tower (which belongs to the tower). This yields an obstruction to strictly progressive maps and, combined with a choice selector on strict upper cones, a maximality principle: such posets have maximal elements. The contribution is methodological, making explicit a reusable proof architecture.

Significance. If the construction of the largest Bourbaki tower is shown to be non-circular and to follow from the well-ordered lub hypothesis alone, the paper supplies a cleaner derivation of fixed-point results under strictly weaker completeness than the standard chain-complete Bourbaki-Witt theorem and directly links it to Zorn-style maximality. The explicit normal-form architecture is a useful clarification for order theory and set theory.

major comments (1)

[Proof of main theorem] Proof of the main fixed-point theorem (construction of largest Bourbaki tower): The existence of a largest Bourbaki tower is asserted and used to produce the fixed point as its lub. The manuscript must explicitly show how this largest tower is obtained using only the hypothesis that every nonempty well-ordered subset has a lub, without presupposing a maximality principle in the poset of all Bourbaki towers (which would be circular, since a Zorn-type maximality result is derived from the fixed-point statement later). Please specify whether transfinite recursion is employed and how the union of a chain of towers is shown to remain a Bourbaki tower whose lub lies inside it.

minor comments (2)

[Abstract] Abstract: The claim that 'the least upper bound of this largest tower belongs to the tower itself' should be expanded to indicate precisely why the lub is necessarily attained as a stage rather than merely existing in the poset.
[Definitions] Notation: The distinction between 'well-ordered trajectory' and 'chain' should be made uniform throughout; the former appears to be used for the specific successor/limit structure, but occasional slippage into 'chain' risks confusion with arbitrary chains.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed report and for identifying the need to clarify the construction of the largest Bourbaki tower to avoid any potential circularity. We will revise the manuscript accordingly.

read point-by-point responses

Referee: Proof of the main fixed-point theorem (construction of largest Bourbaki tower): The existence of a largest Bourbaki tower is asserted and used to produce the fixed point as its lub. The manuscript must explicitly show how this largest tower is obtained using only the hypothesis that every nonempty well-ordered subset has a lub, without presupposing a maximality principle in the poset of all Bourbaki towers (which would be circular, since a Zorn-type maximality result is derived from the fixed-point statement later). Please specify whether transfinite recursion is employed and how the union of a chain of towers is shown to remain a Bourbaki tower whose lub lies inside it.

Authors: The referee is correct that the current presentation is too concise and risks appearing circular. In fact, the proof employs transfinite recursion along the class of ordinals, justified by the lub hypothesis alone. We start with the empty tower or the minimal element if it exists, and recursively define the next element by applying the progressive map if it is not a fixed point, or at limit ordinals by taking the lub of the preceding well-ordered segment (which exists by assumption). This process yields a Bourbaki tower. To show it is the largest, we prove by induction that any Bourbaki tower is an initial segment of this recursively defined one. For the union of a chain of towers: suppose we have a chain of Bourbaki towers under inclusion. Their union is well-ordered because it is the union of a chain of well-orderings. Successor stages in the union are successors in some tower, hence generated by the map. For a limit stage in the union, the preceding elements form a well-ordered set whose lub is taken in some tower in the chain (since the chain is directed), and thus the lub is in the union. The lub of the entire union, if it exists, would be a fixed point if the map cannot progress further. We will add a new subsection detailing this construction and the verification that the union remains a tower, ensuring the argument uses only the given hypotheses. This revision will make the proof fully rigorous and non-circular. revision: yes

Circularity Check

0 steps flagged

Derivation is self-contained; no reduction to inputs by construction

full rationale

The paper constructs the largest Bourbaki tower directly from the lub hypothesis on nonempty well-ordered subsets and obtains the fixed point as the lub of that tower (which belongs to the tower by the construction). The subsequent maximality principle is derived as a consequence after the fixed-point result, not used as a prerequisite. No self-definitional loops, fitted parameters renamed as predictions, or load-bearing self-citations appear in the derivation chain. The argument remains a direct construction from the poset axioms and the stated completeness hypothesis.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The claim rests on the standard axioms of partial orders plus the domain assumption that nonempty well-ordered subsets have least upper bounds; the Bourbaki tower is an invented auxiliary concept with no independent evidence outside the proof.

axioms (1)

domain assumption Every nonempty well-ordered subset of the poset has a least upper bound
This is the central hypothesis invoked to ensure the largest tower has a fixed-point lub.

invented entities (1)

Bourbaki tower no independent evidence
purpose: To provide a well-ordered trajectory under the progressive map whose limit stages use lubs
Newly introduced auxiliary structure to organize the proof; no independent existence proof is given outside the construction.

pith-pipeline@v0.9.0 · 5520 in / 1270 out tokens · 34848 ms · 2026-05-13T07:50:40.071463+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear
We prove that least upper bounds for nonempty well-ordered subsets are sufficient to force a fixed point for every progressive self-map... The proof proceeds by constructing a largest Bourbaki tower.
IndisputableMonolith/Foundation/AlexanderDuality.lean alexander_duality_circle_linking unclear
if every nonempty well-ordered subset has a least upper bound, then the poset has a maximal element

Reference graph

Works this paper leans on

7 extracted references · 7 canonical work pages

[1]

Nicolas Bourbaki,Theory of Sets, Elements of Mathematics, Springer, 2004

work page 2004
[2]

B. A. Davey and H. A. Priestley,Introduction to Lattices and Order, 2nd ed., Cambridge University Press, 2002

work page 2002
[3]

Halmos,Naive Set Theory, Undergraduate Texts in Mathematics, Springer, 1974

Paul R. Halmos,Naive Set Theory, Undergraduate Texts in Mathematics, Springer, 1974

work page 1974
[4]

Thomas Jech,Set Theory, 3rd millennium ed., Springer Monographs in Mathematics, Springer, 2003

work page 2003
[5]

Kelley,General Topology, Graduate Texts in Mathematics, Vol

John L. Kelley,General Topology, Graduate Texts in Mathematics, Vol. 27, Springer, 1975

work page 1975
[6]

34, College Publications, 2011

Kenneth Kunen,Set Theory, Studies in Logic, Vol. 34, College Publications, 2011

work page 2011
[7]

5, Springer, 1998

Saunders Mac Lane,Categories for the Working Mathematician, 2nd ed., Graduate Texts in Mathematics, Vol. 5, Springer, 1998. 11

work page 1998