ARC138 D - Differ by K bits の解法の正当性を示す

なんの記事？

$N$ ビットグレイコードの、ハミング距離 $K$ のバージョンは存在しますか？存在するならばそのひとつを構築してください、という問題がARC138 Dにて出題されました。

$K=1$ のときはグレイコードそのものなので、必ず構築できます。以下では、 $K\geq2$ のときを考えることにします。所望の順列が存在するための自明な必要条件として、次の条件が考えられます。

$K$ が奇数であり、かつ $K\lt N$

逆にこの条件を満たすならばいつでも構築可能なのですが、公式解説ではそれを示す過程で、

$N$ bit の XOR の基底であって，popcount が
$K$ になる値のみからなるものを取ることができます

という事実を使っています。これは（たぶん）非自明だと思うので証明を考えてみました、というのが本記事の内容です。

示したいこと

以下では単に「行列」と言ったら、体 $\mathbb{F}_2=\{0,1\}$ 上の行列を考えるものとします。示すべきことは、「正整数 $N$ と、 $K\lt N$ なる奇数 $K$ とを任意にとったとき、各行に $1$ がちょうど $K$ 個あるような $N\times N$ 行列 $M$ が存在して、 $M$ に対して行基本変形を施すことにより単位行列にできる」ということです。行基本変形は可逆なので、変形していく方向を逆にした、以下の命題が証明できればよいです。

命題

正整数 $N$ と、 $K\lt N$ なる奇数 $K$ とを任意にとる。このとき、 $N\times N$ 単位行列に行基本変形を施すことにより、各行に $1$ がちょうど $K$ 個あるような行列にできる。

証明

行基本変形の手順を以下のように与えます。

$N\times N$ 単位行列からスタートする。 $K=1$ ならば既に目標の行列になっている。
$3,\dots,K+1$ 行目を $1$ 行目と $2$ 行目に足す。
$1$ 行目と $2$ 行目を $3,\dots,N$ 行目に足す。
ここで、右下の $(N-2)\times(N-2)$ の領域に注目すると、 $(N',K')=(N-2,K-2)$ の部分問題が現れている（ $N',K'$ の条件は保たれる）。よって、再帰的に目標の行列を構成できる。

言葉だとわかりにくいので、 $(N,K)=(7,5)$ のときを例にとって、変形されていく様子を図解します。

matrix1

matrix2

matrix3

matrix4

matrix5

matrix6

matrix7

最後は、部分問題が $(N,K)=(3,1)$ となって変形が終了しました。図で灰色になっている部分は、その時点で既に確定した部分です。既に確定したはずの部分が、後の変形で壊れたりすることがあるのではないかと思うかもしれませんが、 $K$ が奇数であることなどより、そのようなことは起こりえません（例を追ってみるとわかると思います）。だから安心して部分問題に帰着できるわけです。

おわりに

というわけで、証明できました。証明さえできれば、今回は $N$ が小さいので、基底の構成は愚直に $O(N2^N)$ で十分です。今回の証明での構成方法であれば、（基底の構成パートは） $O(N^2)$ でできそうです。
もっと簡単な証明があったり、もっと綺麗な基底があったりしたら教えてください。