Open Research Index

Tucker's Lemma: Full Combinatorial & Topological Parity Suite in 1D and 2D

Noah Cohen

Palomar Registrypalomar/PALOMAR-2026-09-03-000007Sep 3, 2026math.COscore 0

A complete machine-checked Lean 4 formalization of Tucker's Lemma (Albert W. Tucker, 1945) and the combinatorial Borsuk–Ulam theorem in 1D and 2D without artificial conditions. Formalizes four foundational pillars: (1) 1D discrete sign-change parity and antipodal interval subdivision lemma; (2) 2D combinatorial double counting of face doors and modulo-2 parity conservation on edge-pseudomanifolds; (3) the boundary cycle engine on 2D edge-pseudomanifolds with an enumerated cyclic boundary (CyclicBoundaryPseudomanifold2D) under antipodal boundary labeling, proving that non-complementary…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-03-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-03-000007/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-03-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'