The exact asymptotic constant in the metric dimension of Jaccard space
Bjørn Kjos-Hanssen
cs.DM
Sep 8, 2026 · v1
TL;DR
The paper's results were verified in Lean 4 using Harmonic's Aristotle, with a public repository; the Lindström/Cantor–Mills coin-weighing theorem is assumed as a black box.
Abstract
Let $X$ be a finite set with $|X|=n$ and let $\mathrm{Jac}(a,b)=|a\,\triangle\, b|/|a\cup b|$ be the Jaccard distance on the power set $2^X$. Lladser and Paradise recently proved that the metric dimension of $(2^X,\mathrm{Jac})$ is $Θ(n/\ln n)$, with the constant left open; their bounds are $(\ln 2)\,n/\ln n\lesssim β(2^X,\mathrm{Jac})\lesssim 2\ln(2e)\,n/\ln n$. We determine the constant: \[ β(2^X,\mathrm{Jac})=\frac{2n}{\log_2 n}\,(1+o(1))=(2\ln 2)\,\frac{n}{\ln n}\,(1+o(1)). \] The proof identifies the problem, on each “slice” of subsets of fixed cardinality, with the Erdős–Rényi coin-weighing problem for a spring scale (the problem of detecting matrices). The lower bound is the Erdős–Rényi entropy argument applied to the middle slice; the upper bound follows from the explicit detecting families of Lindström and of Cantor and Mills, augmented by a single extra landmark that reveals cardinality.
Problem
Lladser and Paradise showed that the metric dimension of the power set of an n-element set under the Jaccard distance is Θ(n/ln n). The exact asymptotic constant was left open, with lower and upper bounds differing by a factor of about 4.9.
Approach
On each slice of fixed-cardinality subsets, resolving under the Jaccard distance is shown to be equivalent to the Erdős–Rényi coin-weighing problem (detecting families). The lower bound applies the Erdős–Rényi entropy argument to the middle slice, using a hypergeometric variance bound. The upper bound takes the explicit detecting families of Lindström and of Cantor–Mills and adds the single landmark X, which reveals cardinality. The results were machine-checked in Lean 4 with Aristotle, taking the coin-weighing asymptotics (Theorem 2.3) as an assumption.
Results
The metric dimension is (2n/log₂ n)(1+o(1)), i.e. (2 ln 2) n/ln n, with an explicit lower bound valid for all n ≥ 2 and an upper bound of M(n)+1. Exhaustive search for n ≤ 5 shows the metric dimension can be strictly smaller than M(n).
| n | 1 | 2 | 3 | 4 | 5 |
|---|
| β(2^X, Jac) | 1 | 2 | 2 | 3 | 3 |
| M(n) | 1 | 2 | 3 | 3 | 4 |
Metric dimension of Jaccard space vs. coin-weighing number for n ≤ 5 (exhaustive search)
