A four-point lattice set separates maximal discrete Borsuk number from the cube characterization proposed in Conjecture 3.

Conjecture 3 of Brose, De Loera, López-Campos, and Torres is false as stated in dimension 2: an explicit four-point set has discrete Borsuk number 4, but its convex hull is not unimodularly equivalent to any lattice square. The witness and the failure of the printed biconditional are formalized in Lean 4.30.0, making the small counterexample a kernel-checked refutation rather than a numerical observation.

The conjecture appears in On Lattice Diameter Segments and A Discrete Borsuk Partition Problem (arXiv:2508.20009 v1, posted 27 August 2025), where it characterizes bounded lattice sets whose discrete Borsuk number is 2^d. The preprint was still v1-only on 11 June 2026, and no posted resolution was found. The authors were notified privately.

The frozen statement

The arXiv LaTeX source at paper/sections/Borsuk.tex, line 76, states: “Let S ⊂ Z^d be a bounded set. Then β_Z(S) = 2^d if and only if conv(S) is unimodularly equivalent to a d-cube [0,m]^d for any m ∈ N.”

The result

Let S_A = {(0,0), (1,0), (0,1), (3,5)}. Every pairwise difference is primitive, so the lattice diameter is 1 and β_Z(S_A) = 4 = 2². On the other hand, |conv(S_A) ∩ Z²| = 7. Unimodular equivalence preserves lattice-point counts, while |[0,m]² ∩ Z²| = (m+1)² ≠ 7 for every m. Thus the d = 2 instance, and therefore the all-dimensions biconditional as printed, fails.

Borsuk.witnessA_kills_conjecture3
Borsuk.conjecture3_counterexample
Borsuk.conjecture3_false

The Lean project contains no sorry, admit, added axiom, native_decide, or unsafe. The axiom audit reports exactly [propext, Classical.choice, Quot.sound].

Artifacts

Limitations

The refutation is of the biconditional as printed; the dimension-2 instance suffices because it quantifies over all dimensions. The witness does not refute the unstated full-set variant S = conv(S) ∩ Z^d. Designed follow-up witnesses B and C were stretch goals and are not claimed.

The kernel guarantees the Lean statements. Their correspondence with the paper's definitions is human-checked against its LaTeX and documented in the reading kit and status report. The result has not been externally refereed. Corrections will be logged, dated, and never silent.