The NANUQ distance, also called the NANUQ metric, is a quartet-based metric on the taxa of a semi-directed phylogenetic network. Its name abbreviates "Network inference Algorithm via NeighbourNet Using Quartet distance" (Allman et al. 2019).
Let 
be such a network on a taxon set 
, with 
. For a four-taxon phylogenetic
tree 
,
define 
to be 0 when 
and 
form a cherry, meaning they are adjacent to the same internal vertex,
and 1 otherwise. For a four-taxon restriction 
of 
, let 
be the unweighted arithmetic
mean of 
over the phylogenetic trees displayed by 
. Then
 |
Here the sum runs over all two-element subsets 
of 
, 
denotes the restriction of 
to the four indicated taxa, and 
(Holtgrefe et al. 2025).
A metric is circularly decomposable if it is a nonnegative weighted sum of the split metrics in a split system that is compatible with a circular
ordering of 
.
Holtgrefe et al. (2025) proved that the NANUQ distance of a binary, semi-directed,
outer-labeled planar, galled level-2 network with one nontrivial blob is circularly
decomposable, with positive split support equal to the union of the splits of its
displayed trees.
A computer-assisted project reported the same circular decomposability and exact-support conclusions for binary, semi-directed least stable ancestor (LSA) networks that are outer-labeled planar and galled, at every finite level and with any number of blobs (VibeMathed 2026). The project used an exact finite certificate, a six-label reduction, and a composition identity. OpenAI Codex developed the proofs, certificates, and partial Lean components under human direction. As of Oct. 1, 2026, the complete theorem had not been formalized in Lean or independently reviewed by a specialist.
