2607.19276v1 / README.md
all files
# Reproduction report: Norine's antipodal-coloring conjecture
## Verdict
**Partial.** The graph-theoretic reduction and the algebraic obstruction are
fully machine checked, but the paper-specific radial polyhedral-chain
construction is not formalized. Consequently this repository does **not**
claim an unconditional Lean proof of Theorem 1.1.
The strongest assembled theorem is:
```lean
theorem Norine.norine_conjecture_of_polyhedralChainRealization
(hpoly : Norine.PolyhedralChainRealization) :
Norine.NorineConjecture
```
Here `PolyhedralChainRealization` says exactly that, for every `K ≥ 2`, a
diagonal rook labeling constructs the forbidden finite Smith tower packaged by
`ForbiddenChainMap (K - 2)`. This is Proposition 5.7 plus the source tower and
the target properties from Sections 3--5. It is an explicit theorem
hypothesis, not a Lean axiom. It is also too close to the paper's main new
construction to qualify as the permitted kind of deep external theorem, so the
verdict is not “reproduced.”
## Files
- `Norine/Basic.lean`
- Defines cube vertices, coordinatewise antipodes, cube adjacency, symmetric
two-edge-colorings, monochromatic connectivity, and rook labelings.
- Proves sanity/equivalence results:
- `monoConnected_iff_walk` identifies the path predicate with a finite walk
in the selected color subgraph.
- `rookLabelingEquivNaive` proves the coordinate presentation is equivalent
to the paper's literal map into
`Ωᵣ = {(a,b) : Fin r × Fin r // a ≠ b}` with coordinate swapping.
- Proves the complete Section 2 reduction. From a counterexample it takes
red connected components, labels `x` by `(p(x),p(Ax))`, pads both the cube
and label set, and constructs
`RookLabeling (n + r) (n + r)`.
- `norine_of_diagonal_rook` proves Theorem 1.1 from Theorem 2.3.
- `Norine/ChainObstruction.lean`
- Proves the descending norm argument of Lemma 3.1 over `F₂ = ZMod 2`.
- `norm_tower_aug_zero` is the target-side descent.
- `chain_level_borsuk_ulam` is the complete finite-tower obstruction.
- `ForbiddenChainMap` packages precisely the data used by the obstruction,
and `forbiddenChainMap_isEmpty` proves that package has no inhabitant.
- `Norine/AntipodalModule.lean`
- Proves the algebraic content of Lemma 4.7 for a finite antipodal
refinement. If `A` is a fixed-point-free involution of a finite basis,
then on coefficient functions over `F₂`,
`ker (1 + A) = range (1 + A)`.
- The proof explicitly chooses one side of every antipodal orbit and does not
assume semisimplicity.
- `Norine/Reproduction.lean`
- Declares the one remaining proposition-level interface,
`PolyhedralChainRealization`.
- Assembles the checked layers and contains `#print axioms` audits.
## Exact statement formalized
`Cube n` is `Fin n → Bool`. Two vertices are adjacent when one coordinate
differs and all others agree. An `EdgeColoring n` is a symmetric
`Cube n → Cube n → Bool`; values on nonedges are ignored. It is antipodal when
```text
color (A x) (A y) = !(color x y)
```
for every cube edge `xy`. `HasMonochromaticAntipodalPath` asks for a vertex
`x`, a color `b`, and a finite walk from `x` to `A x` in the spanning subgraph
of color `b`. Thus `NorineConjecture` states, for every `n ≥ 2`, exactly the
paper's Theorem 1.1.
The use of a walk is harmless and standard: deleting repetitions from a finite
walk produces a graph-theoretic path with the same endpoints. More
importantly, the definition cannot make the theorem easier by admitting
nonedges, since every step is an edge of `cubeGraph n`.
## What remains
The missing proof of `PolyhedralChainRealization` requires all of the following
paper-specific infrastructure:
1. spherical pointed polyhedral cones and their face lattices;
2. face-to-face subdivisions and finite antipodally invariant common
refinements;
3. the quotient of free polyhedral chains by every subdivision relation;
4. well-defined facet boundary on that quotient and `∂² = 0`;
5. radial chains of positive root cones;
6. the degenerate radial cancellation identity (Lemma 5.4);
7. the rook-gallery rank bound (Lemma 5.1);
8. Freudenthal gallery chains and the composite equivariant chain map.
Mathlib at commit `7779d601f7103882175b3125539d5d1232911f5e`
contains finitely generated/dual-finitely-generated convex cones, but no
polytope face lattice, polytopal subdivision, common-refinement, or
subdivision-chain theory. The gap is therefore not an elaboration issue: the
subject needed by Sections 4--5 is absent.
## Approaches attempted
1. **Direct transcription of the paper.** The graph reduction, chain
obstruction, and free antipodal-module calculation were completed. The
route stopped at the missing polyhedral subdivision/face theory described
above.
2. **Replace polyhedral chains by a continuous Borsuk--Ulam map.** Radially
extending root labels over Freudenthal simplices fails when zero lies in a
root convex hull. The rook rank lemma says such zeros are degenerate, but a
simultaneous small perturbation can turn a degenerate zero into a robust
interior zero; generic perturbation does not remove all of them. This is
exactly why the paper works at chain level.
3. **Signed Tucker shortcut.** The map
`(a,b) ↦ sign(b-a) * min(a,b)` is antipodal, uses `K-1` absolute labels, and
has no complementary pair on a rook-adjacent cube edge. However, Tucker's
lemma applies to all edges of a triangulation, including Freudenthal
diagonals. The stronger assertion that an antipodal labeling of cube
vertices must have a complementary *original cube edge* is false already
for `K = 3`; a local backtracking check found such labelings for every tested
`K = 3,4,5`.
4. **Exterior/Orlik--Solomon replacement.** Exterior powers make dependent
radial boundaries cancel algebraically, but the antipodal action then has
fixed basis directions (or becomes trivial in characteristic two), so
`ker(1+A)=im(1+A)` fails. Keeping positive-cone information restores the
free action and also restores the need for subdivision relations.
5. **Constructible-function associated graded.** Indicators of cones modulo
lower-dimensional support make subdivision identities easy and retain a
free antipodal action. The unresolved point is defining a representative-
independent codimension-one boundary with square zero. Proving that is
another formulation of the missing polyhedral-chain theory, not a shortcut.
6. **Existing formalization projects.** Tooling-only searches found verified
general Sperner infrastructure and verified one-/two-dimensional Tucker
fragments, but no general Tucker/Borsuk--Ulam theorem or polyhedral
subdivision-chain package that closes this gap.
No inconsistency or concrete counterexample to the paper was found. The
individual informal steps checked during the attempt—including the rook
gallery split-graph argument and the mod-two radial cancellation setup—appear
mathematically coherent.
## Network/tooling trace
The paper, its authors, and discussions/formalizations of this paper were not
searched. Network access was used only to look for general Lean tooling and
library coverage:
- Web searches for Lean 4 formalizations of Borsuk--Ulam, Tucker's lemma,
Sperner's lemma, and polytope/face/subdivision theory.
- Read-only requests to `https://leangenius.org` for the general entries
`borsuk-ulam-oq-03-oq-03`,
`borsuk-ulam-oq-03-oq-02`,
`sperner-ndim`,
`sperner-ndim-mathlib`,
`sperner-ndim-mathlib-oq-01`, and related listing metadata.
These were inspected in `/tmp`; no external source was copied into this
development.
## Verification
Toolchain:
```text
leanprover/lean4:v4.33.0-rc1
mathlib 7779d601f7103882175b3125539d5d1232911f5e
```
Commands:
```bash
cd repro
lake build Norine
lake env lean Norine/Reproduction.lean
rg -n '\\bsorry\\b|^\\s*axiom\\b|^\\s*opaque\\b' Norine
```
The build succeeds and the search returns no declarations. The axiom audit
reports only Mathlib's standard `propext`, `Classical.choice`, and
`Quot.sound`; there is no `sorryAx` and no added axiom.
---
## Bundled checkout: upstream mathlib README
The reproduction lives directly in the supplied full mathlib checkout. Its
original project README is retained below.
# mathlib4
[](https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16)
[](https://leanprover.zulipchat.com)
[](https://gitpod.io/#https://github.com/leanprover-community/mathlib4)
[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io).
It contains both programming infrastructure and mathematics,
as well as tactics that use the former and allow to develop the latter.
### Installation
You can find detailed instructions to install Lean, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html).
Alternatively, click on one of the buttons below to open a GitHub Codespace or a Gitpod workspace containing the project.
[](https://codespaces.new/leanprover-community/mathlib4)
[](https://gitpod.io/#https://github.com/leanprover-community/mathlib4)
### Using `mathlib4` as a dependency
Please refer to
[https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency)
### Experimenting
Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)?
For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html).
### Documentation
Besides the installation guides above and [Lean's general
documentation](https://docs.lean-lang.org/lean4/doc/), the documentation
of mathlib consists of:
- [The mathlib4 docs](https://leanprover-community.github.io/mathlib4_docs/index.html): documentation [generated
automatically](https://github.com/leanprover/doc-gen4) from the source `.lean` files.
- A description of [currently covered theories](https://leanprover-community.github.io/theories.html),
as well as an [overview](https://leanprover-community.github.io/mathlib-overview.html) for mathematicians.
- Some [extra Lean documentation](https://leanprover-community.github.io/learn.html) not specific to mathlib (see "Miscellaneous topics")
- Documentation for people who would like to [contribute to mathlib](https://leanprover-community.github.io/contribute/index.html)
Much of the discussion surrounding mathlib occurs in a [Zulip chat
room](https://leanprover.zulipchat.com/), and you are welcome to join, or read
along without signing up. Questions from users at all levels of expertise are
welcome! We also provide an [archive of the public
discussions](https://leanprover-community.github.io/archive/), which is useful
for quick reference.
### Contributing
The complete documentation for contributing to `mathlib` is located
[in the community contribution guide](https://leanprover-community.github.io/contribute/index.html).
Useful checkout commands include:
```shell
lake exe cache get
lake build
lake test
```
The project style, naming, and documentation guides are available from the
same contribution guide. The upstream repository also documents local HTML
documentation builds, Lean 3 migration, dependency updates, and its current
and past maintainer teams.