Erdős–Rado negative stepping-up for ordinal order types
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-08-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-08-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-08-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'