Pith. sign in

REVIEW 6 major objections 4 minor 8 references

On Effective Banach-Mazur Games and an application to the Poincar\'e Recurrence Theorem for Category

T0 review · 6 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper effectivizes the Banach-Mazur game and uses it to prove an effective Poincaré recurrence theorem for category, showing non-recurrent points form an effective first category set.

desk verdict A genuinely interesting attempt at an effective Banach-Mazur characterization, but the load-bearing converse in Theorem 4.3 is not proven, and Theorems 4.10 and 5.5 inherit or add serious gaps. read the letter →

arxiv 2506.11118 v2 pith:MEOUE3MS submitted 2025-06-09 math.LO cs.LOmath.DS

Prajval Koul , Satyadev Nandakumar This is my paper
classification math.LOcs.LOmath.DS MSC 03F6037B2054H05
keywords effectivefirstcategoryBanach-MazurgametopologycomputableT0spacePoincarérecurrencetopologicaldynamicsanalysismeagersets
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper effectivizes the classical Banach-Mazur game, in which two players alternately choose nested open sets and one player wins if the eventual intersection avoids a target set. Its central claim is that in a strongly computable T0 space, the second player has an effective winning strategy exactly when the target set is of effective first category: a computably enumerable union of effectively nowhere dense sets. This equivalence is then used as a game-theoretic tool to prove an effective categorical Poincaré recurrence theorem: for a bounded computably enumerable open region of Euclidean space with a computable homeomorphism that admits no non-empty open wandering set, all points except an effective first category set are recurrent. The paper also shows by the same route that the complement of the set of Liouville numbers is an effective first category set, so Liouville numbers are effectively co-meager.

What carries the argument

The load-bearing object is the effective Banach-Mazur game: two players alternately pick nested basic open sets from a strongly computable T0 space, player 2 being restricted to choices computable from the previous moves, and player 2 wins when the intersection of all chosen sets lies inside the complement of the target set. The surrounding effective topology supplies the quantitative notions the game needs: a c.e. open set is a computable-enumerable union of basic open sets; a set is effectively nowhere dense if every basic open set contains a uniformly computable non-empty basic open subset avoiding it; and an effective first category set is a c.e. union of effectively nowhere dense sets. The characterization theorem works because in a strongly computable T0 space disjointness of basic open sets is decidable, which lets the converse proof enumerate maximal disjoint families and lets the forward proof select, at each move, the first basic open set inside the complement of the next nowhere-dense layer. In the recurrence application, the mechanism is the set $F_n(E) = \{x \in E : (\forall j > n)\; T^{-j}x \notin E\}$, whose union over $n$ is exactly the non-recurrent points of $E$; each $F_n(E)$ is shown to be effectively nowhere dense, so the game gives an effective winning strategy for player 2.

What would settle it

A concrete way to test the characterization is to exhibit a strongly computable T0 space in which a computable greedy selection of pairwise disjoint basic open sets is never maximal, or in which the diagonal intersection $\bigcap_{n\geq 1} \bigcup H_n$ contains a point outside $C$; either would break the converse of Theorem 4.3.

Watch

Extended reading notes

Core claim

The paper's central discovery is Theorem 4.3: in a strongly computable T0 space $(X,\tau,\beta,\nu)$ with $M \sqcup C = X$, the effective Banach-Mazur game $\mathrm{BM}_{\langle M,C\rangle}$ has an effective winning strategy for player 2 if and only if $M$ is of effective first category in $X$. The forward direction builds a computable strategy for player 2 directly from a c.e. enumeration of effectively nowhere dense sets covering $M$; the converse extracts such an enumeration from any effective winning strategy by assembling maximal computable families of pairwise disjoint basic open sets. On top of this characterization, the paper proves Theorem 5.5, the effective Poincaré recurrence theorem for category: in a bounded c.e. open region $X \subseteq \mathbb{R}^n$ with a computable homeomorphism $T$ admitting no non-empty open wandering set, the set of non-recurrent points of $X$ under $T$ is of effective first category. The same game-theoretic criterion yields the corollary that the set of non-Liouville numbers is an effective first category set.

Load-bearing premise

The converse half of the main characterization assumes that the computable greedy selection of pairwise disjoint basic open sets is maximal with dense union, and that the diagonal intersection of these families is a legal play consistent with the second player's winning strategy; that assumption is asserted rather than proved.

Editorial extensions

If this is right

  • Effective first category sets are exactly those for which the second player can force the play computably into the complement, giving a game-theoretic certificate of effective meagerness.
  • The effective Poincaré recurrence theorem for category says that in any bounded c.e. open region with a computable homeomorphism and no non-empty open wandering set, every point outside an effectively meager set recurs infinitely often under forward iterates of the homeomorphism.
  • The effective Banach-Mazur game supplies a uniform winning strategy for player 2 on the non-recurrent set, so the proof is constructive and avoids the axiom of choice used in the classical converse.
  • The Liouville-number corollary follows directly: the non-Liouville numbers form an effective first category set, hence Liouville numbers are effectively co-meager.
  • The second version of the game extends the characterization locally: in a complete computable metric space, player 1 has an effective winning strategy exactly when the target set is of effective first category at some point.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • An extension the authors do not state: the same game-theoretic certificate might characterize effective first category in other computable topological spaces whose basic open sets have decidable disjointness, not just strongly computable T0 spaces.
  • The 'no non-empty open wandering set' assumption in Theorem 5.5 is probably removable in some cases; the proof only uses it to ensure that each $F_n(E)$ has a non-empty c.e. open set in its complement, so weaker hypotheses that guarantee this would give the same conclusion.
  • The Liouville example suggests the effective game is a useful sanity-check for genericity in computable analysis: sets that are small in measure or dimension, like Liouville numbers, can still be topologically large in the effective sense.
  • The constructive, choice-free proof of the converse is itself a contribution to effective descriptive set theory, since it replaces the classical Zorn's lemma argument with a greedy computable enumeration.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

6 major / 4 minor

Summary. The paper defines two effective versions of the Banach-Mazur game: one on strongly computable T0 spaces in which Player 2 is restricted to computable strategies (Section 4.1), and one on complete computable metric spaces in which Player 1 is so restricted (Section 4.2). The main characterization, Theorem 4.3, claims that Player 2 has an effective winning strategy in BM_{M,C} if and only if M is of effective first category. Theorem 4.10 claims a dual pointwise characterization for Player 1. These results are applied to show that the non-Liouville numbers form an effective first category set (Theorem 4.12) and to establish an effective category version of the Poincaré recurrence theorem (Theorem 5.5).

Significance. If correct, the paper would supply a constructive, choice-free characterization of effective meagerness with applications to effective dynamics. The forward direction of Theorem 4.3 is a plausible and explicit construction, and the paper rightly identifies the effective game as a natural tool. However, the converse of Theorem 4.3 and both directions of Theorem 4.10 rest on unproved inclusions, illegal moves, or invalid game transformations, and Theorem 5.5 relies on a stronger non-wandering hypothesis than is assumed. Because the characterization is the load-bearing step for all later applications, the central claims are not currently supported.

major comments (6)
  1. [§4.1.1 (Theorem 4.3, converse)] The assertion that 'Since f_i is part of the winning strategy for P2, we have ∩_{n≥1} ∪H_n ⊆ C' is not justified. A winning strategy constrains the intersection of the moves within each single play; from x ∈ ∪H_n for every n one only obtains, for each n, some n-chain whose top contains x. These chains need not be nested and need not belong to one play consistent with the strategy, so no argument shows that x lies on a single play whose intersection avoids M. The inclusion is load-bearing: it is the step from a winning strategy to effective meagerness, and it is inherited by Theorems 4.12 and 5.5.
  2. [§4.1.1 (Theorem 4.3, converse)] The claim that 'By construction, H_n is a maximal family of disjoint collection of basic open sets within X' is not established. The greedy procedure selects tops from a fixed computable enumeration of n-chains; a basic open set that is not the top of any n-chain need never be considered, so the family may fail to be maximal, and ∪H_n need not be dense. The density of ∪H_n is needed for the subsequent step that (∪H_n)^c is effectively nowhere dense.
  3. [§4.2 (Theorem 4.10, proof)] The first move G1 = G ∪ M is not an element of the class G of basic open sets and need not be open at all, so it is not a legal move. Moreover, the later step asserts that the modified game BM_{G1∩M, X\(G1∩M)} has a winning strategy for the new Player 2 and then invokes Theorem 4.3; no argument is given that a Player 1 winning strategy in the original game yields a Player 2 winning strategy in the modified game. The converse direction of Theorem 4.10 is therefore unsupported.
  4. [§4.2 (Theorem 4.10, forward direction)] The appeal to Cantor's lemma is invalid as written. The sets G_{2n-1} are open balls with diam G_{2n-1} < 1/n, but Cantor's lemma requires a decreasing sequence of non-empty closed sets with diameters tending to 0. A decreasing sequence of open balls with diameters tending to 0 can have empty intersection, so the conclusion that ∩_{n≥1} G_n is a singleton does not follow.
  5. [§5 (Theorem 5.5, proof)] The non-wandering assumption gives, for every non-empty open E, the existence of some i≠j with T^{-i}(E) ∩ T^{-j}(E) ≠ ∅; it does not imply E ∩ T^{-(k+1)}(E) ≠ ∅ for each fixed k. The proof's set H = E ∩ T^{-(k+1)}(E) may therefore be empty, so the strategy's requirement that G_{2n-1} \ F_n(E) contain a non-empty c.e. open set is not established. In addition, the non-wandering hypothesis is applied to the fixed region E, whereas in the game Player 1 may choose an arbitrary basic open set G_{2n-1}; the proof does not explain how to obtain a non-empty open subset of G_{2n-1} \ F_n(E).
  6. [§4.3 (Theorem 4.12, proof)] The labels of the game are inconsistent. The proof begins with BM_{E,E^c} and a strategy for Player 2, but the concluding calculation E^c ∩ ∩G_n = ∅ shows ∩G_n ⊆ E, which is the winning condition for Player 2 in BM_{E^c,E}, not in BM_{E,E^c}. The theorem's conclusion that E^c is effectively meager may be provable directly from the explicit union representation, but the game-theoretic argument as written does not follow from the stated game.
minor comments (4)
  1. [§1] There are several typographical slips, including 'Computable Toplogy' in the keywords and 'an easy application' in the introduction.
  2. [§4.1.1] The displayed equations after 'Now, ∩_{n≥1} G_n =' contain typesetting artifacts (e.g., stray 'H' and missing set-difference symbols) that make the argument difficult to parse.
  3. [§4.2] Definition 4.6 uses the tuple (X,ρ,W,ν) with W ⊆ Σ* and then applies ν to elements of W as if they were points; this is inconsistent with the representation ν of the basis used earlier and should be clarified.
  4. [§5 (Theorem 5.5)] The proof states F_1(E) ⊇ F_2(E) ⊇ F_3(E) ⊇ ..., but by the definition F_n(E) = {x∈E : (∀j>n) T^{-j}x ∉ E}, the sequence is increasing: F_1(E) ⊆ F_2(E) ⊆ F_3(E) ⊆ ... . This does not affect the equality N(E) = ∪_n F_n(E), but the displayed monotonicity is incorrect.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation is present: the effective Banach-Mazur characterization and its applications do not reduce to their inputs by construction, although the converse of Theorem 4.3 contains an omitted proof that is a correctness gap rather than circularity.

full rationale

The paper's central claim, Theorem 4.3, is not circular. The forward direction constructs an explicit effective winning strategy for P2 from a c.e. union of effective nowhere dense sets, and the converse attempts to recover such a union from chains generated by a winning strategy. Neither direction defines its conclusion into its assumptions. The later results, Theorems 4.10, 4.12, and 5.5, invoke Theorem 4.3 as a lemma rather than assuming its conclusion; no fitted parameter is renamed as a prediction, and no load-bearing step is justified solely by a self-citation. The main concern is an omitted proof in the converse of Theorem 4.3, Section 4.1.1: the assertion 'By maximality, ∪H_n is a dense open set' is not established by the greedy construction, and the claim 'Since fi is part of the winning strategy for P2, we have ∩ ∪ H_n ⊆ C' is unsupported because a winning strategy constrains individual plays, not the union of tops from different chains. This is a derivation gap or correctness risk, not an equivalence-by-construction, so it does not raise the circularity score.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The paper introduces no fitted constants or new physical/mathematical entities. It relies on standard definitions from computable analysis and a few unproven premises specific to the proofs, the most serious being the maximality of H_n and the non-wandering intersection property.

assumptions (6)
  • domain assumption Strongly computable T0 spaces have decidable disjointness of basic open sets (used to select disjoint n-chains).
    Definition 4.1 postulates that ν(u) ∩ ν(v) = ∅ is decidable; the proof of Theorem 4.3 relies on this to pick pairwise disjoint basic open sets.
  • standard math Cantor's intersection lemma for complete metric spaces (decreasing closed sets with diameters tending to 0 have non-empty singleton intersection).
    Invoked in Theorems 4.10 and 5.5 to conclude the nested plays converge to a point.
  • ad hoc to paper The computable enumeration of n-chains in Theorem 4.3 yields a maximal family H_n whose union is dense in X.
    The converse of Theorem 4.3 asserts this without proof; a greedy selection of disjoint sets does not generally yield a maximal or dense family.
  • ad hoc to paper If P2 has a winning strategy, then ∩_{n≥1} ∪ H_n ⊆ C, where H_n are the tops of the n-chains used in the strategy.
    This is the central step in the converse of Theorem 4.3; no argument shows that a point in the intersection of the unions corresponds to a single play consistent with the strategy.
  • ad hoc to paper The non-existence of non-empty open wandering sets for T implies E ∩ T^{-(k+1)}(E) ≠ ∅ for each k and for each basic open set E ⊆ X.
    Theorem 5.5 needs a non-empty open set disjoint from F_k(E) inside every basic open set, but the wandering condition only guarantees some pair of iterates intersect, not the specific index or arbitrary open subsets.
  • domain assumption Every non-empty c.e. open set in a computable metric space contains a non-empty basic open set (Lemma 4.9).
    Used in Theorem 4.10 to ensure P1 can always find a smaller basic open set avoiding M_k.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On Effective Banach-Mazur Games and an application to the Poincar\'e Recurrence Theorem for Category." pith.science (2026). https://pith.science/paper/MEOUE3MS

@misc{pith2026250611118,
  author       = {Pith},
  title        = {Pith review of: On Effective Banach-Mazur Games and an application to the Poincar\'e Recurrence Theorem for Category},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MEOUE3MS}},
  note         = {Machine review of arXiv:2506.11118}
}
read the original abstract

The classical Banach-Mazur game characterizes sets of first category in a topological space. In this work, we show that an effectivized version of the game yields a characterization of sets of effective first category. Using this, we give a proof for the effective Banach Category Theorem. Further, we provide a game-theoretic proof of an effective theorem in dynamical systems, namely the category version of Poincar\'e Recurrence. The Poincar\'e Recurrence Theorem for category states that for a homeomorphism without open wandering sets, the set of non recurrent points forms a first category (meager) set. As an application of the effectivization of the Banach-Mazur game, we show that such a result holds true in effective settings as well.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

8 extracted references · 7 canonical work pages

  1. [1844]

    17 L. R. Lisagor. The Banach-Mazur game.Mathematics of the USSR-Sbornik, 38(2):201–216, 1981.doi:10.1070/SM1981v038n02ABEH001229. 18 J. H. Lutz. Resource-bounded Baire category and small circuits in exponential space. In Proceedings of the Second Structure in Complexity Theory Conference, pages 81–91,

    work page doi:10.1070/sm1981v038n02abeh001229 1981

  2. [1896]

    Computable versions of baire’s category theorem

    STACS 2026 5:14 Effective Banach-Mazur Games and Poincaré Recurrence 4 Vasco Brattka. Computable versions of baire’s category theorem. In Jirí Sgall, Ales Pultr, and Petr Kolman, editors,Mathematical Foundations of Computer Science 2001, 26th International Symposium, MFCS 2001 Marianske Lazne, Czech Republic, August 27-31, 2001, Proceedings, volume 2136 o...

    work page 2026

  3. [1980]

    26 John C

    doi: 10.1007/978-1-4684-9339-9_22. 26 John C. Oxtoby. The Banach-Mazur game and Banach category theorem. InContributions to the theory of games, vol. 3, Ann. of Math. Stud., no. 39, pages 159–163. Princeton Univ. Press, Princeton, NJ,

    work page doi:10.1007/978-1-4684-9339-9_22

  4. [1981]

    Computable metrization.Math

    10 Tanja Grubba, Matthias Schröder, and Klaus Weihrauch. Computable metrization.Math. Log. Q., 53(4-5):381–395, 2007.doi:10.1002/MALQ.200710009. 11 Heinrich Hilmy. Sur la récurrence ergodique dans les systèmes dynamiques.Rec. Math. [Mat. Sbornik] N.S., 7/49:101–109,

    work page doi:10.1002/malq.200710009 2007

  5. [1992]

    Category version of the Poincaré recurrence theorem.Topology Appl., 154(14):2709–2713, 2007.doi:10.1016/j.topol.2007.05.004

    20 Peter Maličký. Category version of the Poincaré recurrence theorem.Topology Appl., 154(14):2709–2713, 2007.doi:10.1016/j.topol.2007.05.004. 21 R. Daniel Mauldin, editor.The Scottish Book. Birkhäuser/Springer, Cham, second edition,

    work page doi:10.1016/j.topol.2007.05.004 2007

  6. [2001]

    5 Josef M

    URL: https://doi.org/10.1007/3-540-44683-4_20,doi:10.1007/3-540-44683-4\_20. 5 Josef M. Breutzmann, David W. Juedes, and Jack H. Lutz. Baire category and nowhere differentiability for feasible real functions. InAlgorithms and Computation. ISAAC 2001, volume 2223 ofLecture Notes in Computer Science, pages 219–230. Springer, Berlin, Heidelberg, 2001.doi:10....

    work page doi:10.1007/3-540-44683-4_20

  7. [2002]

    30 Nitest Vijayvargiya

    URL:https://www.sciencedirect.com/science/article/pii/ S0304397501001025,doi:10.1016/S0304-3975(01)00102-5. 30 Nitest Vijayvargiya. Poincare non-recurrent points form an effective measure zero set. Master’s thesis, Indian Institute of Technology Kanpur,

    doi:10.1016/s0304-3975(01)00102-5

  8. [2015]

    22 Jan Mycielski, S

    Mathematics from the Scottish Café with selected problems from the new Scottish Book, Including selected papers presented at the Scottish Book Conference held at North Texas University, Denton, TX, May 1979.doi:10.1007/978-3-319-22897-6. 22 Jan Mycielski, S. Swierczkowski, and A. Zipolhkeba. On infinite positional games.Bull. Acad. Polon. Sci. Cl. III., 4...

    work page doi:10.1007/978-3-319-22897-6 1979

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.