{"id":"palomar/PALOMAR-2026-09-08-000003","url":"https://github.com/bjrtx/ordinal-step-up/tree/e46994fca709e3983061ef8d52a824b29a613ee4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-08-000003-v1.json","repo":"https://github.com/bjrtx/ordinal-step-up","tags":["math.LO","math.CO","msc:03E02","msc:05D10","set-theory","ordinals","ramsey-theory","lean"],"score":0,"title":"Erdős–Rado negative stepping-up for ordinal order types","trust":"high","domain":"math.LO","source":"palomar","authors":["Bruno Jartoux"],"reviews":0,"subject":"math.LO","summary":"A Lean 4 formalisation of the Erdős–Rado negative stepping-up lemma in its order-type form, for arities three and above and for at least two colours. Fix an ordinal kappa; a colour count mu ≥ 2; and a target order type theta = omega^alpha with alpha > 0, so that theta is additively indecomposable. The theorem proved is, for every natural number r: if some colouring of the (r+3)-subsets of kappa by ordinals below mu admits no monochromatic subset of kappa of order type theta, then some colouring of the (r+4)-subsets of 2^kappa admits none either, using the same number of colours. The…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-08","reactions":{},"formalized":true,"formalizes":[{"title":"\"A partition calculus in set theory\" by Erdős and Rado for readers from the twenty-first century","identifier":"https://eprints.illc.uva.nl/id/eprint/1797","relationship":"formalizes"}]}