Metrizable betweenness relations on six points: exact counts, and a four-fact obstruction
Abstract
A metric d on a finite set induces the ternary relation d(x,z)+d(z,y)=d(x,y), read as "z lies between x and y", and a ternary relation is metrizable when some metric induces it. A recent census of metrizable betweenness relations on n points prints b₆=7 238 428 and leaves the number bar b₆ of isomorphism classes unknown. We recompute the census by exact integer face enumeration of the metric cone MET₆ — 296 extreme rays by double description over ℤ, then a bitmask closure search over faces, with no linear programming at any point — and obtain b₆=7 221 418,qquad bar b₆ = 11 610,qquad bar c₆ = 10 287. The published b₆ is too large by 17 010; the corrected value now carried by the OEIS is right, and the two counts up to isomorphism, which are single-source there, are confirmed by an unrelated method. Behind the count is a structural fact. We isolate a six-point identity among eight triangle slacks which forces one "checkerboard" of four betweenness facts as soon as the complementary one holds, and use it to exhibit a ternary relation Bᵃˢᵗ on six points that satisfies the Mendris–Zlatoš axioms (B0)–(B4), has every one of its five-point restrictions metrizable, and is metrizable by no metric — with four betweenness facts, against the six of the only such structure we have found written down before. Exhaustive computation places 1 675 470 labelled relations, in 2 596 isomorphism classes, between the axioms and metrizability at six points, and shows that four facts is the exact minimum, attained by 270 relations in exactly two classes. That six is the least n at which the axioms fail to characterise metrizability is Mendris–Zlatoš's 1995 assertion, published without proof; we give a machine-checked proof of its existential half and of their own example. Every statement outside the census is formally verified in Lean 4.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
3fbfc3615f0b899af75f5722b0ed01e4f18bd8019d5f98ebc9726a02077e81ef
Claim ledger
Stated results
MB0candidate2026-08-28
The six-point exchange identity, and the exchange law it implies
MB1known2026-08-28
Locality fails at six points: a betweenness relation on six points whose every five-point restriction is metrizable but which is metrizable by no metric
MB2candidate2026-08-28
The exhibited relation Bstar is the betweenness relation of no metric
MB3routine2026-08-28
Every five-point restriction of Bstar is the betweenness relation of a metric
MB4routine2026-08-28
Non-vacuity: some metric satisfies all four hypotheses of the exchange law
MB5routine2026-08-28
All four hypotheses of the exchange law are needed
MB6routine2026-08-28
None of the six restriction metrics of MB3 induces Bstar globally
MB7routine2026-08-28
Two betweenness facts do not force two more
MB8known2026-08-28
Every metric betweenness relation satisfies the axioms (B0)-(B4)
MB9routine2026-08-28
Bstar satisfies the axioms (B0)-(B4)
MB10known2026-08-28
The betweenness axioms (B0)-(B4) do not imply metrizability, and six points is where that first shows
MB11correction2026-08-28
b₆ = 7221418: the corrected OEIS value is right, and arXiv:2607.27222v1 Table 1's b₆ = 7238428 is too large by 17010
This ledger entry is reported in prose and is not bound to a Lean theorem.MB12candidate2026-08-28
bbar₆ = 11610 and cbar₆ = 10287
This ledger entry is reported in prose and is not bound to a Lean theorem.MB13candidate2026-08-28
On six points exactly 1675470 labelled relations (2596 isomorphism classes) satisfy (B0)-(B4) without being metrizable; the least number of betweenness facts in such a relation is four, attained by 270 relations in exactly two isomorphism classes
This ledger entry is reported in prose and is not bound to a Lean theorem.MB14routine2026-08-28
Infrastructure: a pruned base-4 depth-first search computes exactly the sum of a leaf value over all completions passing every check
MB15routine2026-08-28
(A₂, T₂) of Mendris & Zlatos satisfies the betweenness axioms (B0)-(B4)
MB16routine2026-08-28
Every five-point restriction of (A₂, T₂) is metrizable
MB17routine2026-08-28
The twelve-term identity behind (A₂, T₂): its six slacks and the six it forces are the same linear form
MB18known2026-08-28
(A₂, T₂) is metrizable by no metric
MB19known2026-08-28
The Mendris-Zlatos claim, checked for their own example: (A₂, T₂) is a betweenness space, all its five-point restrictions are metrizable, and it is metrizable by no metric
MB20routine2026-08-28
(A₂, T₂) and Bstar are not isomorphic
MB21candidate2026-08-30
The cyclic identity on six points, and the cyclic law it implies
MB22candidate2026-08-30
Bcyc — a second four-fact non-metrizable betweenness space on six points, not isomorphic to Bstar
MB23routine2026-08-30
Every five-point restriction of Bcyc is metrizable, and none of the six restriction metrics induces Bcyc globally
MB24routine2026-08-30
Bcyc is isomorphic neither to Bstar nor to (A₂,T₂)
MB25routine2026-08-30
Controls for the cyclic law: all four hypotheses are satisfiable, all four are needed, and two do not suffice
MB26candidate2026-08-30
Four is the minimum: a betweenness space on six points with at most three betweenness facts is metrizable
MB27candidate2026-08-30
The four-fact non-metrizable betweenness spaces on six points are exactly 270 labelled relations, each isomorphic to Bstar or to Bcyc
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- A metric d on a finite set X induces a ternary relation
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7