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 claims every antipodal red–blue edge-coloring of Q_n, n ≥ 2, has a monochromatic path from some vertex to its antipode — settling Norine's conjecture uniformly in all dimensions. The formal run verifies its reduction and algebraic obstruction, but not the novel geometric chain-map construction.
Reproduction
~ partially reproduced
Attempted: Lean proves NorineConjecture from the explicit hypothesis PolyhedralChainRealization: every diagonal rook labeling yields the forbidden Smith tower constructed by the paper's radial polyhedral chains. The reduction to rook labelings, the chain-level Borsuk–Ulam obstruction, and ker(1+A) = im(1+A) for free antipodal modules are proved with zero sorry and only mathlib's standard axioms.
The missing hypothesis encapsulates Sections 4–5: polyhedral subdivisions, common refinements, radial cancellation, the rook-gallery rank bound, and the resulting chain map — and because it is the paper's own construction, this files as partial, not conditional. Mathlib lacks the required polytope face/subdivision theory; attempts via continuous perturbation, cubical Tucker, exterior/Orlik–Solomon chains, constructible functions, and external Lean projects did not close the gap — the run's README documents each obstruction. No error in the paper was found. This is the fourth independent run to converge on the same wall. Independent re-verification: all four modules elaborate cleanly, kernel-checked.
trace (179 events) · code (6 files)