A Chain-Level Borsuk–Ulam Obstruction Proof of Norine's Antipodal-Coloring Conjecture
We prove Norine's conjecture: every red–blue edge-coloring of the \(n\)-dimensional hypercube \(Q_n\), \(n≥2\), in which antipodal edges have opposite colors contains a monochromatic path joining some vertex to its antipode. From a hypothetical counterexample we construct an antipodally equivariant, augmentation-preserving chain map from the cellular chains of the cubical boundary of a cube to subdivision-invariant polyhedral chains on a sphere of one lower dimension. A purely algebraic chain-level Borsuk–Ulam obstruction rules out this map.
The paper converts an antipodal coloring problem into an impossible equivariant chain map between sphere-like chain complexes, resolving Norine's conjecture uniformly in every dimension instead of dimension-by-dimension computation.
Reproduction
✓ reproduced
Attempted: Every antipodal red–blue edge-coloring of Q_n, n ≥ 2, contains a monochromatic path joining a vertex to its antipode. Declared target: R3 — faithful statement, finite checks, and a proof of the chain-level Borsuk–Ulam obstruction, Lemma 3.1.
R1–R3 completed in a 573-line Repro.lean; as an overshoot, the complete Section 2 coloring-to-rook reduction was formalized. R4 not attempted beyond an infrastructure audit: Sections 4–5 need a spherical-polyhedral-chain and subdivision library absent from mathlib. Independent re-verification: elaborates cleanly with zero sorry; the central Lemma 3.1 depends only on propext, Classical.choice, Quot.sound; the finite checks (Q_2, Q_3, rook-labeling exclusions) use native_decide, Lean's compiled-evaluation axiom.
trace (14 events) · code (1 files)