Topological spaces — flashcards
Every card the map can derive about Topological spaces — definitions, statements, attribution, and the edges it sits on.
Theorems 11
State: Borsuk–Ulam theorem.
Every continuous map f : Sⁿ → ℝⁿ sends some antipodal pair to the same point: f(p) = f(−p) for some p. The n in both places is the content — a phrasing that drops either one is a different, false claim.
derived from st/borsuk-ulam by the statement rule
State: Tucker's lemma.
In an antipodally-labelled triangulation of the n-ball, with labels ±1,…,±n and antipodal boundary vertices carrying opposite-signed labels, some edge joins two vertices with the same value and opposite sign. The combinatorial, Sperner-style statement equivalent to Borsuk–Ulam.
derived from st/tucker by the statement rule
State: The stolen necklace theorem.
A necklace with k types of jewels, each present in an even number of beads, can be fairly split between two thieves using at most k cuts — and k is tight: arranged as k contiguous blocks, one per type, every block needs an internal cut, so 'at most k' cannot be improved in general.
derived from st/necklace-splitting by the statement rule
State: Necklace-splitting is PPA-complete.
Finding a fair two-thief split of a necklace is PPA-complete already at the simplest case — two thieves, the friendliest group action a proof by Borsuk–Ulam could ask for. Filos-Ratsikas & Goldberg, 2018 (arXiv:1805.12559). This refutes the hypothesis that k-thief difficulty tracks the availability of free ℤ/k actions on spheres: hardness is present at the friendliest case there is, so it is an artefact of the topological proof route rather than an obstruction inherent to the problem.
derived from st/necklace-ppa by the statement rule
State: Any non-negative-deficit construction achieves exact fairness at the midpoint; its one-sided bound does not reverse.
Two results, and the 2026-09 mining pass corrected the statement of both. (1) THE ONE-SIDED LEMMA. The bound is A_c(t) <= ceil(t*rho_c): no color ever runs more than one bead ahead of its proportional share. It is ONE-SIDED, and the natural two-sided version — a matching lower bound A_c(t) >= floor(t*rho_c) — is FALSE, with an explicit counterexample at x >= 4 reaching a deficit of 23/22. Earlier filings named the lemma 'one-sided' without stating the inequality or recording that the symmetric version fails, which left the asymmetry looking like a proof artifact rather than a fact about the construction. (2) THE MIDPOINT-EXACTNESS THEOREM. At the checkpoint t = y/2 the split is exactly fair. (3) 'GREEDY' NAMES AN INVARIANT CLASS, NOT AN ALGORITHM. The result does not depend on the argmax tie-break — it holds for ANY rule that only ever serves a color with non-negative deficit. The argmax largest-remainder rule is one member of that class and was previously filed as if it were the hypothesis; the tie-break question was explicitly asked in lemma-harvest-prompt.md section 3, the answer came back as the broader class, and this entry did not move until the 2026-09 mining pass. Corrected 2026-08 (retained): an earlier version wrongly conditioned this on a discrepancy statistic D <= 4/3. That statistic was never computed for greedy-built arrangements at all — only for independent random ones, in a separate, unrelated, single-batch numerical experiment (400 trials, three colors, twelve beads, not reproduced or tested at other sizes) with no completed proof behind it. The two results were conflated in translation from a summary and are unrelated.
derived from st/greedy-midpoint by the statement rule
State: c(w)=1 bounds discrepancy, tightly, but not the other way round.
For 3-color, 12-bead balanced necklace arrangements (4 beads of each color), exhaustive enumeration of all 34,650 distinct arrangements shows c(w)=1 ⟹ D ≤ 4/3, with no exceptions, and the bound is tight — 4/3 is achieved. The converse, once believed and stated on this map, is false: D ≤ 4/3 does not imply c(w)=1. 10,584 of the 34,650 arrangements (about 30%) have D ≤ 4/3 yet require two or three cuts, and fixing D at exactly 1 does not even determine c(w) — it splits close to evenly between one cut and two. D is necessary but far from sufficient.
derived from st/necklace-discrepancy-boundary by the statement rule
State: Every triangle is isosceles.
Because |x + y|_p = max(|x|_p, |y|_p) exactly when the two differ, among any three ultrametric distances the two largest are equal. The metric intuition imported from ℝ fails at the first triangle.
derived from st/isosceles by the statement rule
State: Every p-adic ball is clopen.
Balls in ℚ_p are simultaneously open and closed, so ℚ_p is totally disconnected — and yet not discrete, since ℤ is dense in ℤ_p.
derived from st/clopen-balls by the statement rule
State: Every point of a ball is its centre.
If c ∈ B(a, r) then B(c, r) = B(a, r). Two balls are therefore either disjoint or nested; partial overlap is impossible.
derived from st/ball-center by the statement rule
State: ℤ_p is compact.
ℤ_p is a closed subset of the product of the finite discrete spaces ℤ/pⁿℤ, hence compact by Tychonoff — or directly, by pigeonholing digits. ℚ_p is only locally compact.
derived from st/zp-compact by the statement rule
State: Perfectoid spaces.
A tilting equivalence relating characteristic 0 and characteristic p geometry, which turned a long list of separate p-adic comparison results into instances of one construction.
derived from st/perfectoid by the statement rule
Names and dates 9
Borsuk–Ulam theorem — who, and when?
Karol Borsuk, conjectured by Stanisław Ulam, 1933.
derived from st/borsuk-ulam by the attribution rule
Tucker's lemma — who, and when?
Albert W. Tucker, 1946.
derived from st/tucker by the attribution rule
The stolen necklace theorem — who, and when?
Charles Goldberg and Douglas West, 1985.
derived from st/necklace-splitting by the attribution rule
Necklace-splitting is PPA-complete — who, and when?
Aris Filos-Ratsikas and Paul Goldberg, 2018.
derived from st/necklace-ppa by the attribution rule
Every triangle is isosceles — who, and when?
Hasse, Schnirelmann, Teichmüller and others, 1920s–1930s.
derived from st/isosceles by the attribution rule
Every p-adic ball is clopen — who, and when?
Hasse, Schnirelmann, Teichmüller and others, 1920s–1930s.
derived from st/clopen-balls by the attribution rule
Every point of a ball is its centre — who, and when?
Hasse, Schnirelmann, Teichmüller and others, 1920s–1930s.
derived from st/ball-center by the attribution rule
ℤ_p is compact — who, and when?
Hasse, Schnirelmann, Teichmüller and others, 1920s–1930s.
derived from st/zp-compact by the attribution rule
Perfectoid spaces — who, and when?
Peter Scholze, 2012.
derived from st/perfectoid by the attribution rule
Formalisation 4
What is Every triangle is isosceles called in Mathlib?
IsUltrametricDist.dist_eq_max_of_dist_ne_dist — Mathlib.Topology.MetricSpace.Ultra.Basic
derived from st/isosceles by the binding rule
What is Every p-adic ball is clopen called in Mathlib?
IsUltrametricDist.isClopen_ball — Mathlib.Topology.MetricSpace.Ultra.Basic
derived from st/clopen-balls by the binding rule
What is Every point of a ball is its centre called in Mathlib?
IsUltrametricDist.ball_eq_of_mem — Mathlib.Topology.MetricSpace.Ultra.Basic
derived from st/ball-center by the binding rule
What is ℤ_p is compact called in Mathlib?
PadicInt.compactSpace — Mathlib.NumberTheory.Padics.ProperSpace
derived from st/zp-compact by the binding rule
Connections 5
Under the Degeneracy lens, how do Topological spaces and Graph theory & combinatorial proof relate? [Degeneracy]
The stolen-necklace argument solves the continuous division problem first — cuts anywhere on a real interval — and recovers the discrete, integer-bead necklace by sliding each cut to the nearest bead boundary. The discrete problem is an un-arbitrary restriction of the continuous one, arrived at from outside the transcript this schema was originally admitted from.
derived from degeneracy:topology→graph-theory by the connection rule
What is the correspondence between Graph theory & combinatorial proof and Topological spaces? [Correspondences]
A discrete, antipodally-labelled triangulation of the ball (Tucker, 1946) is the combinatorial equivalent of a continuous antipodal map on the sphere (Borsuk–Ulam, 1933) — the same relation Sperner's lemma has to Brouwer's fixed point theorem. The via is the whole edge: encode a necklace cut as a point on Sⁿ so that the antipodal map exactly swaps the two thieves, and the topological theorem hands back a fair division for free.
derived from correspondences:graph-theory→topology by the connection rule
What is the correspondence between Boolean algebra and Topological spaces? [Correspondences]
Boolean algebras ↔ compact totally disconnected Hausdorff spaces, as an anti-equivalence of categories. Pure logic ↔ pure geometry.
derived from correspondences:boolean-algebra→topology by the connection rule
Under the Correspondence test lens, how do Division algebra ladder and Topological spaces relate? [Correspondence test]
REFUTED as proposed. The instinct that a complex-analytic proof of the necklace theorem wouldn't generalize was right; the reason given (a quaternion/division-algebra obstruction) was wrong. The actual obstruction is Adams' Hopf-invariant-one theorem — non-parallelisability of spheres — related territory, wrong mechanism.
Recorded as refuted: this edge was drawn and then withdrawn.
derived from correspondence-test:division-algebras→topology by the connection rule
In Mathlib, what is the import relation between p-adic numbers and Topological spaces? [Dependency (Mathlib)]
`Mathlib.NumberTheory.Padics.Hensel` imports `Mathlib.Topology.Algebra.Polynomial`, `Mathlib.Topology.MetricSpace.CauSeqFilter`. Read off Mathlib/NumberTheory/Padics/Hensel.html. No human asserted this edge.
derived from dependency:p-adic-numbers→topology by the connection rule
Concepts 1
What is Topological spaces, in one sentence?
Geometry stripped down to nearness and continuity, with no distances or angles.
derived from topology by the concept rule