平均と分散から順位と島を調べる · X01 統合版1.2 / Moments, gaps and islands

目次を開く · 全 11 節Contents · 11 sections

数学探索 X01 ／証明・解説・監査の統合版 1.2 ／ 2026 09 09

1. 何を調べ、どこまで確認したか

各値が0以上1以下で、全体として0か1に近い有限データを主な対象とする。平均と分散が同じでも、元データの形は一つには決まらない。しかし、二値性の欠損が十分小さく、総和が所定の整数に近いという条件の下では、上位の値と残りの値の間に必ず隔たりができる。その隔たりの鋭い下限、平均の誤差を許した場合の限界、同じ統計量を持つデータの集合が分かれている仕組みを調べた。広い範囲の一般的な統計データに正の間隔を保証するものではない。

本稿には一般の有限列についての数学的証明、限界を達成する配置、図解、先行研究との照合、Leanの証明ソースと検証記録を収録した。従来の14宣言には2026 09 08の成功記録がある。この14件には補助補題と、X01の主結果には含めない4変数の例2件も含む。その後に追加した33宣言の証明コードは実行未確認であり、形式検証済みには数えない。数学的証明、Leanによる検証、学術的新規性は別の主張である。新規性は確定していない。

これまでのレビュー対応。 横田さんから提供されたFable5.1のレビューを、本文と形式証明に照合した。適用域・帰属・分割形の陳述を改め、行列版の系とその位相上の限界を追加した。レビューの数値観察を出発点として、 $1/2<\eta<1$ の全次元における道連結成分数をT9として証明した。新しいT9はLean未形式化で、新規性も未確定である。

v1.2・公開前の統合版（2026 09 09）。 追加監査に基づき、2008年の最大成分の境界とGorbanの既知の成分数増加の例への帰属を補った。追加Leanコード33宣言、固定版Mathlibソースの照合、Lean実行環境が未復元であるという検証状況も同じページへ統合した。本文・図・証明ソースはこのHTMLだけで読める。次の独立レビューのための確認依頼を末尾に用意した。この統合版に対するFableの新しいレビュー結果はまだ含まない。

整数 $n\ge2$ 、実数 $x_i\in[0,1]$ とし、

S=\sum_{i=1}^{n}x_i,\qquad Q=\sum_{i=1}^{n}x_i^2,\qquad D=S-Q=\sum_{i=1}^{n}x_i(1-x_i)

と置く。値を降順に並べたものを $x_{(1)}\ge\cdots\ge x_{(n)}$ と書く。整数 $1\le s<n$ に対し、

e=S-s,\qquad g_s=x_{(s)}-x_{(s+1)}

が総和の整数からのずれと、上位 $s$ 個との境目の間隔である。

平均 $\mu=S/n$ 、分母を $n$ とする分散 $V=n^{-1}\sum_i(x_i-\mu)^2$ なら、

D=n\{\mu(1-\mu)-V\}.

したがって以下の保証は平均・分散・値域から計算できる。ただし、それらの集計値だけで「どの添字が上位か」を特定する主張ではない。順位ラベルは個々の値を観測して決まり、集計値はその境目の余裕を保証する。

正の間隔を保証する条件は、正確には

2D+e^2<1 \quad\Longleftrightarrow\quad 0\le\mu(1-\mu)-V<\frac{1-e^2}{2n}.

従って有効域は $|e|<1$ かつ、分散が端点分布の上界 $\mu(1-\mu)$ に $O(1/n)$ まで近い領域である。総和が非整数の有限列では、この上界自体は達成できない。 $S=m+r$ 、 $0\le r<1$ なら実際の最大分散は $\mu(1-\mu)-r(1-r)/n$ となる（第6節）。この「ほぼ二値」の領域は、固有値が0か1に近い自己共役行列にも自然に現れる。行列版と、そこへ位相の結論を移す際の限界を第2節で明示する。

2. 普遍的な順位不等式と、等号の構造

定理T1（任意の有限分割に対する平方不等式）。 $x\in[0,1]^n$ とし、添字集合の空でない真部分集合 $I$ を取る。 $s=|I|$ 、 $J=I^c$ 、

u=\min_{i\in I}x_i=x_a,\qquad v=\max_{j\in J}x_j=x_b,\qquad g_I=u-v

と置く。ここで $a\in I$ 、 $b\in J$ は極値を達成する添字である。 $g_I$ は符号を持ち、 $I$ が上位集合であるという仮定は不要である。このとき

\boxed{2D+(S-s)^2+g_I^2\ge1} \tag{T1}

が成り立つ。総和の整数への近さも、分割をまたぐ順序 $u\ge v$ も、この平方不等式には不要である。

順位版の系。 $I$ を上位 $s$ 個の添字に取れば $u\ge v$ 、 $g_I=g_s\ge0$ となり、

g_s\ge\sqrt{\max\{1-2D-(S-s)^2,0\}}.

従って $2D+(S-s)^2<1$ なら上位 $s$ 個が残りから正の間隔で分かれる。任意分割の平方不等式だけから、符号付き $g_I$ の正値を結論してはいけない。平方根型では $u\ge v$ という追加仮定が必要である。

図 1

順位の境目に残る間隔

配置を切り替えると、総和のずれ・欠損・順位間隔の関係を確認できます。

配置

数値は表示桁で丸めています。図は個別の配置の確認であり、一般証明は本文の非負項分解です。

証明。 上の任意分割と極値を達成する添字を使い、 $g=g_I=u-v$ と略記する。また

\begin{aligned} \sigma&=\sum_{i\in I}(1-x_i),& \rho&=\sum_{j\in J}x_j,\\ A&=\sigma-(1-u)=\sum_{i\in I\setminus\{a\}}(1-x_i),& B&=\rho-v=\sum_{j\in J\setminus\{b\}}x_j. \end{aligned}

空和は0とする。これらは非負で、 $e=\rho-\sigma$ である。さらに

T=\sum_{i\in I}(x_i-u)(1-x_i) +\sum_{j\in J}(v-x_j)x_j

と置く。各側での極値の定義と箱制約から各項が非負なので $T\ge0$ 。ここでも $u\ge v$ は使っていない。定義を展開すると $D=u\sigma+(1-v)\rho+T$ となる。ここへ $\sigma=1-u+A$ 、 $\rho=v+B$ を代入すれば、

\begin{aligned} R&:=2D+e^2+g^2-1\\ &=2T+2(1-v)A+2uB+(B-A)^2. \end{aligned} \tag{1}

右辺の全項が非負であることが定理を証明する。

等号条件。 $g>0$ なら $u>0$ 、 $v<1$ であるから、 $R=0$ は $A=B=0$ を強制する。したがって等号となる列は、並べ替え後に

(\underbrace{1,\ldots,1}_{s-1},\,u,\,v,\, \underbrace{0,\ldots,0}_{n-s-1}) \tag{2}

という形を持つ。逆にこの形では $A=B=T=0$ なので等号となる。つまり正の間隔を持つ等号配置では、境目の二つ以外は端点0または1に固定される。

ほぼ等号の場合。 $u\ge g$ 、 $1-v\ge g$ より、(1)から

R\ge2g(A+B),\qquad A+B\le\frac{R}{2g}\quad(g>0). \tag{3}

従って $R\le\varepsilon$ 、 $g\ge\gamma>0$ なら、境目の二つ以外が端点から離れた距離の合計は $\varepsilon/(2\gamma)$ 以下である。 $g$ が0へ近づく場合まで同じ強さの安定性を主張してはいけない。また、他の座標を0/1に置き換えて $u,v$ を残す近似では、総和は $A-B$ だけ変わり得る。

行列版の系。 $X$ を $n\times n$ の自己共役行列とし、作用素順序で $0\le X\le I_n$ とする。固有値を $\lambda_1\ge\cdots\ge\lambda_n$ と並べ、 $1\le s<n$ とすると、

2\operatorname{Tr}(X-X^2) +(\operatorname{Tr}X-s)^2+(\lambda_s-\lambda_{s+1})^2\ge1,

\lambda_s-\lambda_{s+1}\ge \sqrt{\max\{1-2\operatorname{Tr}(X-X^2) -(\operatorname{Tr}X-s)^2,0\}}.

証明。 スペクトル定理により全固有値は $[0,1]$ に属し、 $\operatorname{Tr}X=\sum_i\lambda_i$ 、 $\operatorname{Tr}(X-X^2)=\sum_i\lambda_i(1-\lambda_i)$ 。従って固有値列にT1と順位版の系を適用すればよい。

行列版を主定理に格上げしない理由。 この移し替えは直接の系であり、第3節・第6節の固有値差の公式にも使える。しかし、第4節以降の $\binom ns$ 個の成分や面複体は、固定された座標のラベルを持つベクトル、すなわち固定基底の対角行列のモデルについての結論である。行列全空間では固有ベクトルを回転できる。例えば

P_\theta=\begin{pmatrix} \cos^2\theta&\cos\theta\sin\theta\\ \cos\theta\sin\theta&\sin^2\theta \end{pmatrix},\qquad 0\le\theta\le\frac\pi2,

は常に $P_\theta^2=P_\theta$ 、 $\operatorname{Tr}P_\theta=1$ 、 $D=0$ を満たしながら、 $\operatorname{diag}(1,0)$ と $\operatorname{diag}(0,1)$ を結ぶ。一般の複素自己共役行列でも、同じ階数の直交射影はユニタリ共役で移り合い、ユニタリ行列の固有位相を連続に動かすことで経路が得られる。従ってベクトルの成分数を行列空間へそのまま移すことはできない。応用先としては有力だが、行列版を中心に据えるなら、順位差の節はほぼそのまま使えても、成分・穴の節は新たな位相問題として立て直す必要がある。

3. 平均に誤差を許したときの、鋭い三段の公式

整数 $1\le s<n$ 、 $0\le\eta\le1/2$ 、 $\delta\ge0$ に対し、

F_{s,\eta,\delta} =\{x\in[0,1]^n:\ |S-s|\le\eta,\ D\le\delta\}

を考える。 $\eta$ は総和の誤差幅であり、平均の誤差幅は $\eta/n$ である。

\delta_0=\eta(1-\eta),\qquad \delta_c=\frac{1-\eta^2}{2}

と置く。

定理T2（鋭い誤差帯保証）。

\boxed{ \min_{x\in F_{s,\eta,\delta}}g_s(x)= \begin{cases} \dfrac{1+\sqrt{1-4\delta}}2, &0\le\delta\le\delta_0,\\[5pt] \sqrt{1-2\delta-\eta^2}, &\delta_0\le\delta\le\delta_c,\\[3pt] 0,&\delta\ge\delta_c. \end{cases}} \tag{T2}

隣り合う枝の端点は一致する。 $\eta=0$ では最初の枝は $\delta=0$ だけになる。各パラメータで可行集合は二値列を含むので非空であり、以下に示す配置が実際に最小値を達成する。

図 2

誤差を許したときの最小間隔

実線が達成可能な鋭い下限。破線は普遍不等式だけから得る簡単な下限です。

総和の誤差幅 η 0.100

欠損の上限 δ 0.200

η は平均の誤差幅ではなく総和の誤差幅です。前提は 0 ≤ η ≤ 1/2。横軸を動かしても対象は D ≤ δ の全配置です。

補題（二乗和の最大値）。 $y_i\in[0,1]$ 、 $\sum_i y_i=t$ なら、

\sum_i y_i^2\le\phi(t):=\lfloor t\rfloor+\{t\}^2. \tag{4}

ここで $\{t\}=t-\lfloor t\rfloor$ である。証明するには、端点でない二つの値 $0<a\le b<1$ があれば、 $\epsilon=\min(a,1-b)>0$ として $(a,b)$ を $(a-\epsilon,b+\epsilon)$ に置き換える。総和と箱制約を保存し、二乗和の増分は $2\epsilon(b-a)+2\epsilon^2\ge0$ である。少なくとも一つの値が端点に達するため、端点でない成分数は一回ごとに減る。有限回の操作で小数成分が高々一つとなり、総和からその最終配置は $\lfloor t\rfloor$ 個の1、端数 $\{t\}$ 、残り0と分かる。これが(4)の上限と達成可能性を同時に証明する。整数総和では端数の座標を省けばよい。これは既知の二乗和最大化の部品である。Rosenberg–Jakobsson, Appendix Lemma 3、Ellis, Theorem 1

T2の下界。 $a=|S-s|\le\eta\le1/2$ と置く。(4)より

D\ge a(1-a). \tag{5}

実際、 $S=s+a$ の端数は $a$ 。 $S=s-a$ の端数は $a>0$ なら $1-a$ 、 $a=0$ なら0であり、いずれも端数に対応する欠損が $a(1-a)$ となる。

$\delta\le\delta_0$ のとき $b=(1-\sqrt{1-4\delta})/2$ と置くと、 $t(1-t)$ が $[0,1/2]$ 上で単調増加することから $a\le b\le\eta$ 。T1によって

g_s^2\ge1-2D-a^2 \ge1-2\delta-b^2=(1-b)^2.

これが第一の枝である。 $\delta_0\le\delta\le\delta_c$ では、T1から直接 $g_s^2\ge1-2\delta-\eta^2$ 。最後の枝では $g_s\ge0$ を使う。

各枝の達成配置。 以下の二値を、 $s-1$ 個の1と $n-s-1$ 個の0の間に置く。

範囲	境目の二値	総和・欠損・間隔
第一の枝	$(1-b,0)$	$S=s-b,\ D=b(1-b)=\delta,\ g_s=1-b$
第二の枝	$((1-\eta+h)/2,(1-\eta-h)/2)$ 、 $h=\sqrt{1-2\delta-\eta^2}$	$S=s-\eta,\ D=\delta,\ g_s=h$
第三の枝	$((1-\eta)/2,(1-\eta)/2)$	$S=s-\eta,\ D=\delta_c\le\delta,\ g_s=0$

第二の枝では $0\le h\le1-\eta$ が $\delta_0\le\delta\le\delta_c$ と同値なので、提示した二値は箱内にある。これで全ての枝の鋭さを示した。

例えば $n=6,s=2,\eta=0.1,\delta=0.2$ なら、間隔は必ず $\sqrt{0.59}\simeq0.7681146$ 以上であり、 $(1,0.8340573\ldots,0.0659427\ldots,0,0,0)$ で達成する。

なお $\sqrt{\max(1-2\delta-\eta^2,0)}$ だけでも有効な下界だが、 $\delta<\delta_0$ では鋭くない。第一の枝を省略すると、 $\delta=0$ における間隔1さえ取り逃す。

4. 島の成分数を、具体的な経路で証明する

定理T3（誤差帯の成分）。 T2と同じ条件で、

\boxed{ \#\pi_0(F_{s,\eta,\delta})= \begin{cases} \binom ns,&0\le\delta<\delta_c,\\ 1,&\delta\ge\delta_c. \end{cases}} \tag{T3}

ここで $\pi_0$ は道連結成分を表す。元のラベル付きデータ空間で数えており、座標を置換した列を同一視しない。閾値未満の成分は、上位 $s$ 個の添字集合に正確に対応する。

二値代表への二線分経路。 降順の $x$ と、それに対応する二値代表 $z=(1,\ldots,1,0,\ldots,0)$ 、1の数 $s$ 、を取る。誤差帯 $P=\{y\in[0,1]^n:\ |\sum_i y_i-s|\le\eta\}$ の中の補助頂点 $v$ を次の順で選ぶ。

$x_s\le1/2$ なら $v=(1^{s-1},1-\eta,0,\ldots,0)$ 。
それ以外で $x_{s+1}\ge1/2$ なら $v=(1^s,\eta,0,\ldots,0)$ 。
それ以外なら $v=z$ 。

$1^k$ は1を $k$ 個並べる記法である。境界で複数の選択が最適になる場合も、この順で一つを選べばよい。

重み $w_i=2x_i-1$ 、方向の係数 $c=\sum_i w_i(v_i-x_i)$ と置く。重要なのは $c\ge0$ であり、これは次の符号分解で確認できる。

第一の場合は $\alpha=w_s\le0$ として

c=\sum_i(w_i-\alpha)(v_i-x_i) +\alpha(s-\eta-S). \tag{6}

$i<s$ では最初の積の両因子が非負、 $i>s$ では両因子が非正、 $i=s$ では重みの差が0である。最後の積も、 $\alpha\le0$ と $s-\eta-S\le0$ により非負。第二の場合は $\alpha=w_{s+1}\ge0$ と置き、最後の項を $\alpha(s+\eta-S)$ に替えれば同じ証明となる。第三の場合は、上位側で $w_i\ge0,v_i-x_i\ge0$ 、残り側で両者が非正であり、各積が非負である。

従って $0\le t\le1$ で

\begin{aligned} D(x+t(v-x)) &=D(x)-tc-t^2\|v-x\|_2^2\\ &\le D(x). \end{aligned} \tag{7}

帯 $P$ は凸なのでこの線分は帯内にあり、式から $D$ は非増加である。さらに $v$ から $z$ へは、小数座標を $\eta\to0$ または $1-\eta\to1$ と動かすだけでよい。 $\eta\le1/2$ のためこの線分でも $D$ は非増加となる。これで任意の点から、その二値代表へ高々二本の線分で到達できた。これは各点に対する経路の構成であり、点 $x$ に応じた候補の選び方の連続性は示していない。従ってこの構成だけから、全体の変形収縮を結論しない。

成分の分類。 $\delta<\delta_c$ ではT2より境目の間隔が正である。連続経路の途中で上位 $s$ 個の添字集合を変えるには、その境目で同値が生じる必要があるから、上位集合は経路上で変わらない。一方、同じ上位集合を持つ点は上の経路で同じ代表へ結べる。全ての $s$ 元集合に二値代表が存在するので、成分数は $\binom ns$ である。

$\delta\ge\delta_c$ では、1と0を交換する二座標だけを

(1,0)\longrightarrow(1-\eta,0) \longrightarrow(0,1-\eta) \longrightarrow(0,1) \tag{8}

と動かす。他の $s-1$ 個の1は固定する。総和のずれは $\eta$ 以内であり、最初と最後の線分上の最大欠損は $\delta_0$ 、中央の最大欠損は $\delta_c$ 。一つずつ添字を交換すれば任意の二値代表を結べる。任意の点は代表に結ばれているため、集合全体が道連結となる。閾値ちょうどもこの側に含まれる。

この構成は既知の凸幾何の背景を持つ。Gorban, Lemma 2.1・Proposition 2.4（PDF版）は凸集合を避けた頂点への線分接続と、成分数の辺グラフへの還元を扱う。ここでは箱の誤差帯について頂点を明示し、非増加性を直接証明した。新しい一般原理とは主張しない。

4.1 許容幅が半分を超えるとき：新しい島の誕生と合流

前節の制限 $\eta\le1/2$ は本質的である。しかし $1/2<\eta<1$ の範囲も、帯多面体の頂点と辺を調べることで全次元の成分数を決定できる。集合を

F_\delta=\left\{x\in[0,1]^n:\left|\sum_i x_i-s\right|\le\eta, \quad D(x)=\sum_i x_i(1-x_i)\le\delta\right\}

とする。以下では $n\ge2$ 、 $1\le s<n$ は整数、 $1/2<\eta<1$ 、 $\delta\ge0$ を仮定する。

定理 T9（広い帯における完全成分数公式）。

a=1-\eta,\quad k=\eta(1-\eta),\quad c=\frac{1-\eta^2}{2},\quad h=\frac14,\quad b=\binom ns

とおく。 $F_\delta$ の道連結成分数は

N_{n,s}(\eta,\delta)= \begin{cases} b,&0\le\delta<k,\\ (n+1)b,&k\le\delta<\min(c,h),\\ b+\binom n{s-1}+\binom n{s+1},&c\le\delta<h\quad(c<h),\\ b,&h\le\delta<c\quad(h<c),\\ 1,&\delta\ge\max(c,h). \end{cases} \tag{T9}

空の区間の行は除く。 $c=h$ は $\eta=1/\sqrt2$ と同値であり、この場合は中間の二段階がなくなる。表示した各閾値での等号を含む公式である。

図 3

広い総和帯で、成分が生まれてから合流する

n = 2、s = 1 に固定します。|x₁ + x₂ − 1| ≤ η、x₁(1 − x₁) + x₂(1 − x₂) ≤ δ を満たす集合の道連結成分数です。帯内の数値は成分数を示します。

総和の許容幅 η0.9

欠損の上限 δ0.1

k = η(1 − η) は4成分が新たに現れる閾値、c = (1 − η²)/2 と h = 1/4 は合流の閾値です。閾値ボタンは丸め前の値を選び、等号は変化後の成分数に含めます。η = 1/√2 では c = h で合流が同時に起きます。非常に短い区間の帯内数値は省略されます。

証明の道具：凸障害物と辺グラフ。 コンパクト凸多面体 $P$ と連続凹関数 $f$ に対し、 $X=\{f\le\delta\}$ の成分数は、許容頂点 $f(v)\le\delta$ と、全体が許容される辺 $\max_e f\le\delta$ のグラフの成分数に等しい。

この事実を確認する。 $U=\{f>\delta\}$ は相対的に開いた凸集合である。 $U$ と交わる面を次元の大きい順に処理し、その面の相対内部に $c\in U$ を選ぶ。面内の $x\notin U$ を、 $c$ から $x$ に向かう半直線上で面の境界まで動かす。凸性により、 $x$ を過ぎてから $U$ に再び入ることはない。これは境界を固定する連続な変形であり、他の面上の恒等写像と貼り合わせられる。有限回の処理により、 $X$ は $U$ と交わらない閉じた面の複体 $K$ に強変形収縮する。 $U$ と交わる面の相対内点が選べることは $U$ の相対的開性から従う。各面の辺グラフは連結なので、 $K$ とその 1 次元骨格の成分数は等しい。この骨格が上記の許容グラフである。

頂点の全列挙。 帯だけを課した多面体を $P$ とする。その頂点は次の三種類で尽くされる。

型	座標の構成	個数	$D$
$B$	$s$ 個の 1、残り 0	$b$	0
$L$	$s-1$ 個の 1、1 個の $a$ 、残り 0	$sb$	$k$
$U$	$s$ 個の 1、1 個の $\eta$ 、残り 0	$(n-s)b$	$k$

帯境界が活性でない頂点は箱の頂点であり、許容される整数和は $s$ だけである。帯境界が活性なら少なくとも $n-1$ 座標が 0 または 1 に固定され、残りの座標は和の条件で $a$ または $\eta$ に決まる。これで完全性と個数が従う。

辺の全列挙と閾値。 箱の辺に沿うものは、 $L\leftrightarrow B$ の $a\leftrightarrow1$ と、 $B\leftrightarrow U$ の $0\leftrightarrow\eta$ だけである。いずれも変化する座標が $1/2$ を通るため、辺上の最大欠損は $h=1/4$ 。各 $L,U$ 頂点は、この種類の辺でただ一つの $B$ 頂点につながる。

帯面内の辺は、二座標を動かす次の四種類である。他の座標は 0 または 1 に固定する。

帯面	二座標の端点	辺上の最大 $D$
下側・短い辺	$(a,0)\leftrightarrow(0,a)$	$c$
下側・長い辺	$(1,a)\leftrightarrow(a,1)$	$d=(1-a^2)/2$
上側・短い辺	$(1,\eta)\leftrightarrow(\eta,1)$	$c$
上側・長い辺	$(\eta,0)\leftrightarrow(0,\eta)$	$d$

必要な座標数が確保できない型は現れない。辺の内点で帯境界が活性なら、 $n-2$ 座標が固定されるので、この表で尽くされる。二座標の和を $t$ とすると

y(1-y)+(t-y)(1-t+y) =t-\frac{t^2}{2}-2(y-t/2)^2

であり、中点が各辺内にあるため表の最大値を得る。また

c-k=\frac{(1-\eta)^2}{2}>0,\quad h-k=(\eta-\tfrac12)^2>0,\quad d>\max(c,h).

成分を数える。 $\delta<k$ では $B$ 頂点のみ、 $k\le\delta<\min(c,h)$ では全頂点が存在し、いずれもまだ辺がない。

$c<h$ で $c\le\delta<h$ なら短い帯面辺が先に入る。下側では 1 の位置集合（大きさ $s-1$ ）を固定した群ごとに連結となり、群の数は $\binom n{s-1}$ 。上側では正の位置集合（大きさ $s+1$ ）を固定した群ごとに連結となり、群の数は $\binom n{s+1}$ 。 $B$ の $b$ 個を合わせて T9 の第三行となる。

$h<c$ で $h\le\delta<c$ なら箱に沿う辺が先に入り、各 $B$ を中心に $L,U$ を葉とする、互いに素な $b$ 個の星形ができる。

$\delta\ge\max(c,h)$ になると全 $B$ 頂点が連結となる。実際、二つの $s$ 要素集合が一要素の交換で移り合うとき、共通する $s-1$ 個の 1 を固定して「箱の辺 → 下側の短い辺 → 箱の辺」の三辺で結べる。任意の二つの $s$ 要素集合はこの交換の繰返しで結ばれる。すべての $L,U$ は箱の辺で $B$ につくので全体が連結である。長い辺が入る前にすでに連結となり、それ以後は新しい頂点が生まれない。グラフ補題から T9 が従う。□

レビューの具体例。 $n=2,s=1,\eta=0.9$ では

k=0.09,\qquad c=0.095,\qquad h=0.25,

従って成分数は

2\ \xrightarrow{\ \delta=0.09\ }\ 6\ \xrightarrow{\ \delta=0.095\ }\ 4\ \xrightarrow{\ \delta=0.25\ }\ 1.

各矢印の閾値で右側の個数になる。レビューの $\delta=0.09,0.10,0.20,0.26$ における $6,4,4,1$ という観察は正しい。集合が増大しても、新しい頂点で島が生まれるため、成分数は単調減少とは限らない。

追加系：二次元の穴も分類できる。 $n=2,s=1$ で $p=x_1+x_2-1,\ q=x_1-x_2$ とおくと、帯多面体は六角形

|p|+|q|\le1,\quad |p|\le\eta, \qquad D=(1-p^2-q^2)/2

になる。 $\delta<1/2$ では原点を含まないので、原点から外向きに六角形の境界へ伸ばす放射変形が、 $F_\delta$ を許容境界へ強変形収縮する。この変形はノルムを減らさず、 $D\le\delta$ を保つ。境界は斜辺四本（閾値 $h$ ）と垂直辺二本（閾値 $c$ ）からなる。従って $\delta<\max(c,h)$ では各成分が可縮、 $\max(c,h)\le\delta<1/2$ では $F_\delta\simeq S^1$ 、 $\delta\ge1/2$ では六角形全体となり可縮である。

位置づけ。 T9 は Gorban の一般的な多面体・凸障害物の理論から得られる明示的な系として扱う。同論文§4.2・Fig.4.5（PDF版）には、集合の増大途中で新しい孤立頂点が現れ、成分数が増える例もある。したがって非単調性という現象自体を新規とはしない。同一の箱帯における閾値と二項係数の成分数公式の先行記述は今回未同定であり、優先権は未確定である。本節は通常の数学的証明であり、Lean未形式化である。

5. 0.5での丸めは、順位の交換より先に壊れる

定理T4（最近0/1丸めの閾値）。

\delta_R=\frac12-\eta^2

とする。T2の条件の下で $D<\delta_R$ なら、各値を近い0/1に丸める方法は一意であり、1の数は $s$ 個となる。この厳密な保証の閾値は鋭い。

証明。 ある一座標が $1/2$ なら、残りの総和は $s-1/2+e$ である。 $-1/2\le e\le1/2$ と(4)から、

\begin{aligned} D&\ge\frac14+ \left(\frac12+e\right)\left(\frac12-e\right)\\ &=\frac12-e^2\ge\delta_R. \end{aligned} \tag{9}

端点 $e=\pm1/2$ では残りの総和が整数となり、積の部分は0で、同じ式が成立する。

$D<\delta_R$ の点からT3の二線分経路で二値代表へ戻ると、経路全体でも $D<\delta_R$ 。従ってどの座標も $1/2$ を通れない。丸め結果は経路上で一定であり、終点の二値代表と一致する。

閾値の等号は $(1^{s-1},1/2,1/2-\eta,0,\ldots,0)$ で達成する。 $\eta>0$ なら、小さい $\epsilon>0$ に対して境目の二値を $(1/2-\epsilon,1/2-\eta+\epsilon)$ とすると、どちらも $1/2$ 未満なのに総和は $s-\eta$ である。欠損は $\delta_R+2\eta\epsilon-2\epsilon^2$ となり、 $\delta_R$ のすぐ上で丸めの1の数が $s-1$ 個になる。

\delta_c-\delta_R=\frac{\eta^2}{2}.

従って $\eta>0$ では、最近丸めの保証が失われても、上位 $s$ 個はなお分離している範囲がある。例えば $n=2,s=1,\eta=0.1,x=(0.49,0.41)$ では $D=0.4918<\delta_c=0.495$ だが、0.5で丸めると両方0になる。

成分は二値代表を中心とする星形とは限らない。 $n=2,s=1,\eta=1/2$ 、 $x=(3/8,1/8)$ 、 $\delta=11/32<\delta_c$ とする。 $z=(1,0)$ から $x$ への直線上では $D(t)=3t/4-13t^2/32$ で、 $t=12/13$ の値 $9/26$ が $\delta$ を超える。T3の補助頂点を経由する必要がある。

$\eta\le1/2$ を外してはいけない。 $n=2,s=1,\eta=0.9,\delta=0.1$ では $(0.1,0)$ と $(1,0)$ が可行だが、両者を結ぶ経路は第1座標が $1/2$ になる点を通り、そこで $D\ge1/4>\delta$ となる。 $\delta>\delta_c=0.095$ でも連結ではない。T1はこの範囲でも正しいが、T2–T4の同じ公式を拡張したことにはならない。

6. 総和が整数でない切片では、合流が二段になる

ここでは誤差帯を考えず、総和を正確に固定する。整数 $n\ge1$ 、 $0\le m\le n-1$ 、 $0<r<1$ に対し、

\begin{aligned} S&=m+r,\qquad M=m+r^2,\\ H_S&=\{x\in[0,1]^n:\ \sum_i x_i=S\},\\ X_E&=\{x\in H_S:\ \sum_i x_i^2=M-E\},\\ E_{\max}&=M-S^2/n. \end{aligned}

以前の欠損 $D$ と今回の $E$ は異なり、 $D=r(1-r)+E$ である。(4)と $\sum_i(x_i-S/n)^2\ge0$ から、実現可能な範囲は $0\le E\le E_{\max}$ 。最大配置と一様点 $c=(S/n,\ldots,S/n)$ を結ぶ線分上で全ての値を実現できる。

定理T5（非整数切片の鋭い順位差）。 存在する添字について、

\min_{x\in X_E}(x_{(m)}-x_{(m+1)}) =\sqrt{\max\{(1-r)^2-2E,0\}} \quad(m\ge1), \tag{T5a}

\min_{x\in X_E}(x_{(m+1)}-x_{(m+2)}) =\sqrt{\max\{r^2-2E,0\}} \quad(m+1<n). \tag{T5b}

全範囲の鋭さの証明。 T1に $s=m$ 、 $s=m+1$ を代入し、 $D=r(1-r)+E$ を使えば、それぞれの下界を得る。正の枝では次の配置を使う。

\begin{aligned} y_U(h)&=(1^{m-1},(1+r+h)/2,(1+r-h)/2,0,\ldots,0),\\ h&=\sqrt{(1-r)^2-2E};\\ y_L(h)&=(1^m,(r+h)/2,(r-h)/2,0,\ldots,0),\\ h&=\sqrt{r^2-2E}. \end{aligned} \tag{10}

前者は $0\le E\le b=(1-r)^2/2$ 、後者は $0\le E\le a=r^2/2$ の範囲で、降順・箱制約・指定の総和と二乗和を全て満たし、該当する順位差が $h$ となる。

各閾値を $t\in\{a,b\}$ 、その同率配置を $y=y_L(0)$ または $y_U(0)$ とする。閾値以降は

x(\lambda)=c+\lambda(y-c),\qquad0\le\lambda\le1

を使う。並び順と境目の同率を保ち、

E(x(\lambda)) =E_{\max}-\lambda^2(E_{\max}-t). \tag{11}

$t<E_{\max}$ なら $\lambda=\sqrt{(E_{\max}-E)/(E_{\max}-t)}$ を選び、閾値から上端までの全 $E$ で順位差0を達成できる。 $t=E_{\max}$ なら、その枝は一様点だけで処理する。存在する各種類の中点自体が可行なので、その閾値は必ず $E_{\max}$ 以下である。

図 4

二つの順位差が、別々の閾値で消える

n = 6、m = 2 を固定し、端数 r と欠損 E を動かします。成分数はラベル付きの配列全体で数えています。

総和の端数 r 0.300

最大二乗和からの欠損 E 0.100

a = r²/2、b = (1−r)²/2。閾値の等号では合流済みです。E = Emax は一様配置 1 点。図の曲線は各順位差の最小値です。

定理T6（非整数切片の成分数）。 内部の場合 $1\le m\le n-2$ では $a=r^2/2$ 、 $b=(1-r)^2/2$ 、 $N=\binom nm(n-m)$ として、次の表が正確な道連結成分数を与える。

条件	成分数	成分を識別するラベル
$E<a$ かつ $E<b$	$N$	上位 $m$ 個の集合と、その次の一添字
$a\le E<b$	$\binom nm$	上位 $m$ 個の集合
$b\le E<a$	$\binom n{m+1}$	上位 $m+1$ 個の集合
$a\le E$ かつ $b\le E$	1	全体

表は実現可能域と交差させて読む。 $r<1/2$ なら $N\to\binom nm\to1$ 、 $r>1/2$ なら $N\to\binom n{m+1}\to1$ 、 $r=1/2$ なら $E=1/8$ で直接 $N\to1$ と合流する。各閾値の等号は合流済みの側に含む。

頂点と辺。 $H_S$ の点に二つ以上の内部座標があれば、その二つを和を保って正負に少し動かせるため頂点ではない。従って頂点は $m$ 個の1、一つの $r$ 、残り0であり、個数は $N$ 。1の添字集合 $A$ 、 $r$ の添字 $j\notin A$ を用いて頂点を $(A,j)$ と表す。

辺の相対内部では自由座標が二つである。実際、自由座標が $p$ 個なら、和の一制約を課した局所的な面の次元は $p-1$ である。辺では $p=2$ だから、残る座標は0/1で、自由な二つの和は $r$ または $1+r$ となる。従って辺は $(r,0)\leftrightarrow(0,r)$ と $(1,r)\leftrightarrow(r,1)$ の二種類だけである。辺上の二乗和は中点で最小となり、そこでの欠損 $E$ はそれぞれ $a,b$ となる。

等位集合から残存辺へ。 $\Omega_E=\{x\in H_S:\ Q(x)\ge M-E\}$ とする。 $\Omega_E$ は凸多面体 $H_S$ から相対開凸集合 $U_E=\{Q<M-E\}$ を除いた集合である。 GorbanのProposition 2.4（PDF版）により、その道連結成分は、 $U_E$ の外に残る頂点と、全体が $U_E$ を避ける辺からなるグラフの成分に対応する。全頂点の二乗和は $M$ なので残存し、二種類の辺はそれぞれ $E\ge a$ 、 $E\ge b$ のときに残る。

$E<E_{\max}$ では、この補集合は $X_E$ へ強変形収縮する。 $R_E=\sqrt{M-E-S^2/n}>0$ として

p_E(x)=c+\frac{R_E}{\|x-c\|_2}(x-c) \tag{12}

と置く。 $\|x-c\|_2\ge R_E$ なので、 $x$ と $p_E(x)$ を結ぶ放射方向の線分は、凸な $H_S$ 内にあり、その半径は $R_E$ 以上を保つ。これが $\Omega_E$ 内の連続な変形収縮であり、 $X_E$ を固定する。これは同論文Lemma 3.2（PDF版）の本例での明示式でもある。

グラフの数え上げ。 $a$ の辺だけなら $A$ を固定した $n-m$ 個の頂点が完全グラフを作り、成分数は $\binom nm$ 。 $b$ の辺だけなら $B=A\cup\{j\}$ を固定した $m+1$ 個の頂点が完全グラフを作り、成分数は $\binom n{m+1}$ 。両方が残ると、まず $A$ を固定して $j$ を選び直し、次に $B$ を固定して $A$ の一要素を交換できるため、任意の頂点へ到達できる。両方ないと全頂点が孤立する。これで表が従う。T5の正の間隔が各順位ラベルの不変性を保証し、表のラベル数と一致する。

端と退化例。

$m=0,n\ge2$ では $b$ の辺とT5aの順位が存在しない。 $E<a$ で $n$ 成分、 $a\le E\le E_{\max}$ で1成分となる。
$m=n-1,n\ge2$ では $a$ の辺とT5bの順位が存在しない。合流は $b$ で $n\to1$ となる。
$n=2$ では有効な閾値は $E_{\max}$ と一致し、二点が一様点に合流する。
$n=1$ では $H_S=\{r\}$ 、 $E_{\max}=0$ で常に一点。順位差は定義しない。
$E=0$ は頂点そのもの、 $E=E_{\max}$ は一様点一つである。最後のケースには正の半径を要求する(12)を適用しない。

例として $n=6,S=2.3$ では $a=0.045,b=0.245$ であり、成分数は $60\to15\to1$ となる。

7. 島の内部には、穴も生まれて消える

連結成分数だけでは、統計量を保つ集合の形は分かり切らない。ここでは $n=4,S=5/4$ の小さな例について、ホモトピー型まで求める。「点と同じホモトピー型」は、その集合自体が一点という意味ではなく、連続的に縮めて点と同じ型になることを表す。

定理T7（交わらない面への収縮）。 コンパクト凸多面体 $P$ と、その中で相対開な凸集合 $U$ を取る。 $U$ に交わらない閉面全ての合併を $K$ とすると、 $P\setminus U$ は $K$ へ強変形収縮する。ここで閉面には $P$ 自身も含める。各面 $F$ の境界 $\partial F$ は、そのアフィン包 $\operatorname{aff}F$ 内の相対境界を指す。

証明。 $U=\varnothing$ または $P\setminus U=\varnothing$ は直ちに処理できる。以下では、 $U$ に交わる正次元の閉面 $F$ を高次元から順に処理する。 $U$ が $P$ で相対開なので、 $U\cap F\ne\varnothing$ なら $U\cap\operatorname{relint}F\ne\varnothing$ 。実際、交点の十分小さい相対近傍は $U$ に含まれ、面の相対内部はその面に稠密である。

中心 $c_F\in U\cap\operatorname{relint}F$ を選ぶ。 $x\in F\setminus U$ に対して、 $c_F$ から $x$ を通る半直線と $\partial F$ との交点を $\rho_F(x)$ と置く。中心が相対内部にあるためこの交点は一意であり、放射射影は中心以外で連続、境界上では恒等写像となる。

$[x,\rho_F(x)]$ は $U$ に入らない。もしその先の点 $y$ が $U$ に入れば、 $c_F,y\in U$ と凸性により、その間にある $x$ も $U$ に入ってしまうからである。従って

H_F(x,t)=(1-t)x+t\rho_F(x) \tag{13}

は $F\setminus U$ を $\partial F\setminus U$ へ縮め、境界を固定する。

処理済みの高次元交差面の内部は既に除かれている。また、 $U$ を避ける高次元面が $F$ を含むことは、 $F\cap U\ne\varnothing$ に矛盾する。従って現在の空間の他の面と $F$ との交わりは境界にあり、(13)を他の部分の恒等変形と貼り合わせられる。面は有限個の閉集合なので、貼り合わせは連続である。最後には $U$ を避ける面だけが残り、 $K$ は全過程で固定される。 $U$ に含まれる頂点は最初から補集合にない。これで強変形収縮を得る。

面の出現閾値。 T6の $P=H_S$ 、 $U_E=\{Q<M-E\}$ に適用する。 $j$ 個の固定1、 $p$ 個の自由座標、残り固定0を持つ非退化面 $F$ は、 $0<S-j<p$ 、次元 $p-1$ を満たす。自由座標を全て $(S-j)/p$ にすると

\min_F Q=j+\frac{(S-j)^2}{p}.

従って閉面全体が補集合に入る必要十分条件は

E\ge E_F:=M-j-\frac{(S-j)^2}{p}. \tag{14}

この条件を満たす面の合併 $K_E$ が有限セル複体となる。T7と(12)より、 $E<E_{\max}$ では $K_E$ と $X_E$ は同じホモトピー型を持つ。正確には、共通の空間 $\Omega_E$ がそれぞれへ強変形収縮する。一般に $K_E$ は $X_E$ の部分集合ではないため、「 $X_E$ が直接 $K_E$ へ変形収縮する」とは述べない。 $E=E_{\max}$ では $X_E=\{c\}$ 、 $K_E=H_S$ がどちらも可縮であることを別途用いる。

図 5

穴が開き、埋まり、また開く

n = 4、S = 5/4。等位集合と同じホモトピー型を持つ面複体 K_E を表示します。

面が加わる段階

模型の向き 30°

E	代表型	β₀, β₁, β₂
[0, 1/32)	12 個の点	12, 0, 0
[1/32, 1/24)	4 個の円周	4, 4, 0
[1/24, 9/32)	4 個の点	4, 0, 0
[9/32, 13/24)	円周 3 本の束	1, 3, 0
[13/24, 43/64)	球面 S²	1, 0, 1
{43/64}	1 点	1, 0, 0

面複体の正確な頂点・辺・面を三次元投影しています。K_E は一般に X_E の部分集合ではありません。両者はホモトピー同値で、「点型」は原集合が一点であることを意味しません。

定理T8（切頂四面体の穴の遷移）。 $n=4,S=5/4$ では $M=17/16,E_{\max}=43/64$ であり、次の変化が起きる。

$E$ の範囲	$X_E$ のホモトピー型	$(\beta_0,\beta_1,\beta_2)$
$0\le E<1/32$	12個の点	$(12,0,0)$
$1/32\le E<1/24$	互いに離れた4個の円周	$(4,4,0)$
$1/24\le E<9/32$	4個の点	$(4,0,0)$
$9/32\le E<13/24$	円周3本を一点で束ねた空間	$(1,3,0)$
$13/24\le E<43/64$	球面 $S^2$	$(1,0,1)$
$E=43/64$	一点	$(1,0,0)$

完全な面計数と証明。 $H_S$ は三次元の切頂四面体の面構造を持ち、頂点12、辺18、三角形面4、六角形面4である。座標を1に固定すると残りの和が $1/4$ となる三角形面、0に固定すると残りの和が $5/4$ となる六角形面を得る。後者の頂点は残り三座標への $(1,1/4,0)$ の六通りの配置である。(14)から全ての閾値は次の通り。

面の型	$j$	$p$	個数	出現閾値
頂点	1	1	12	0
$r\leftrightarrow0$ の辺	1	2	12	$1/32$
三角形面	1	3	4	$1/24$
$1\leftrightarrow r$ の辺	0	2	6	$9/32$
六角形面	0	3	4	$13/24$
多面体全体	0	4	1	$43/64$

最初は12頂点だけである。12本の第一種辺が現れると、各「1の位置」を固定した三角形の周ができるので、4個の円周となる。次にその三角形面が入って穴が埋まり、4個の可縮成分となる。

残りの6辺が入ると、四つの三角形の各組の間に一本ずつ橋がかかる。各三角形を中心から三分割し、各小三角形を自由な外辺から潰すと、三つの橋の取付点を固定したY字型の木に縮められる。この四つの木をそれぞれ一点へ縮約すると、完全グラフ $K_4$ になる。連結グラフの全域木を一点へ縮約すれば残る円周の数は辺数から頂点数を引いて1を足した値なので、ここでは $6-4+1=3$ 本となる。

六角形面が全て入ると多面体の境界全体になる。凸三次元多面体の内部点からの放射射影により、その境界は $S^2$ と同相である。最後に $E=E_{\max}$ では $X_E$ 自体が一様点一つとなる。以上が全区間と等号の扱いを証明する。

有限セル複体の境界行列も $\mathbb F_2$ 上で独立に計算し、表のBetti数と境界の合成が0になることを確認した。ただし、mod 2のホモロジー計算だけからホモトピー型は決まらない。上表の型には今述べた直接の収縮と面構造の証明を用いている。この位相部分はLean未形式化であり、新規性の文献照合も未完了である。

8. Leanで確認した範囲と、再現の記録

既存の14宣言には、Lean 4.19.0、Mathlib v4.19.0による2026 09 08の成功記録がある。終了コードは0。追加33宣言は実行未確認である。 実行したMathlibのcommitは c44e0c8ee63ca166450922a373c7409c5d26b00b である。証明ソースは MomentIslands.lean。

ここでいう成功は、2026 09 08に実施して同梱ログに残した検証の記録である。2026 09 09には、公式Mathlibの固定版ソースを取得し、上記commitとの一致と使用APIを照合した。一方、公式Lean本体の取得は再試行を含め「ネットワーク承認が決定前にキャンセルされた」と返されて停止した。以前の実行環境もアクセス可能な保存先からは復元できず、今回のLeanコンパイルは未実施である。Mathlibのソース取得やAPI照合を、証明検査の成功と読み替えない。

件数の意味。 14件はファイル内の定理宣言の総数であり、14個の独立したX01主定理ではない。特に four_variable_gap_bound と four_variable_gap は前段の4変数不可能例を扱う補助的な記録で、X01本文の主結果には対応しない。

Leanの定理名	検証した内容
pair_square_upper、pair_square_upper_complement	二変数の平方和上界2本
four_variable_gap_bound、four_variable_gap	総和2、先頭二値の和 $1/2$ なら二乗和 $\le3/2$ 。二乗和 $9/5$ の不可能性。X01主結果外の補助例2件
balanced_error_defect、invert_defect_bound、balanced_error_sharp_bound	左右の非負誤差和が同じ $\rho$ という明示仮定から、二次欠損評価と平方根による反転
concentration_from_square_deficit	非負列の二乗和欠損からの集中評価
rank_gap_core、rank_gap_sqrt、rank_gap_slack	T1の集約量に関する核、平方根型、余裕の評価
finite_rank_gap	任意の二つの有限集合から、核に必要な有限和の不等式を構成
rank_gap_partition、rank_gap_partition_sqrt	任意有限型の分割と各側の極値からT1の平方不等式。平方根型には境界の順序を追加

最後の有限分割版 rank_gap_partition は、任意の非自明な有限分割 $I,I^c$ 、その各側で最小・最大を取る添字 $a,b$ を入力とし、本文T1と同じ平方不等式を直接証明している。分割が上位集合であることは仮定しない。rank_gap_partition_sqrt ではさらに $x_b\le x_a$ を仮定し、

\sqrt{1-2\sum_i x_i(1-x_i) -\left(\sum_i x_i-|I|\right)^2} \le x_a-x_b

を証明している。Leanの実数平方根は負の引数で0となるため、保証が正になるための条件と、定理自体の成立条件は区別されている。数学上の順位記法は、有限列から上位 $s$ 個を選んだこの分割の特殊化である。形式ファイルの入出力は分割と極値を達成する添字を明示しており、並べ替え手続きの検証を必要としない。T1の平方不等式の主張と、この形式化された分割版の間に、未形式化の並べ替えアルゴリズムを補う必要はない。

2026 09 08の既存14宣言について公理依存を出力し、依存は標準の propext、Classical.choice、Quot.sound のみだった。証明穴の sorry、admit、sorryAx や、独自公理の宣言はない。これは「公理を全く使わない」という意味ではなく、Lean/Mathlibの通常の基礎に未証明の仮定を追加していないという意味である。

追加した証明コード：33宣言、全て実行未確認。 既存モジュールから次の四つへ形式化を拡張するソースを記述した。件数は定理宣言の数であり、独立した新定理の数ではない。

追加モジュール	宣言数	コードが対象とする内容	現在の状態
`Packing.lean`	6	整数からのずれによる有限列の欠損下界、半整数座標の排除、尺度を変えた二乗和評価	NOT COMPILED
`BandSharp.lean`	8	T2の三分岐のスカラー下界と二座標の達成配置	NOT COMPILED
`FiniteBand.lean`	7	有限分割への下界適用、任意次元の達成配置、T4の閾値での半整数座標の配置	NOT COMPILED
`Rounding.lean`	12	最近0/1丸め、1の個数の保存、一意な二値の $L^1$ 最小化、整数総和での鋭い誤差上界	NOT COMPILED

finite_band_attainment は $(\mathrm{Fin}\,p\oplus\mathrm{Unit})\oplus(\mathrm{Unit}\oplus\mathrm{Fin}\,q)$ という有限添字型に、 $p$ 個の1、境目の二値、 $q$ 個の0を置く。任意の $p,q$ に対して箱制約、総和、欠損、境目の順序を記述している。これは特定の配列の並べ替えアルゴリズムを検証する主張ではない。robust_total_rounding の十分条件は $\eta\ge0$ で記述したが、閾値の達成配置が対象とするのは本文T4と同じ $0\le\eta\le1/2$ である。

追加分には数学的導出、静的点検、13個の有理係数多項式恒等式の正規化検査を行った。しかし、Leanの構文・型・タクティク実行・カーネル検査を完了していない。証明穴や独自公理を追加するコードが見当たらないことだけでも、形式証明の完成とは言えない。追加33件を既存14件に足して「47件検証済み」とは扱わない。

形式検証が残る範囲。 T2の全分岐・達成配置、T4の最近丸めの総和保存などは上の候補コードを実行・修正する必要がある。T1の等号分類全体と完全な安定性、T3の経路と成分分類、T5の全水準での達成可能性、T6–T9の位相分類には、本文の数学的証明はあるが完成したLean検証はない。特に従来の「左右の誤差和が等しい」という形式補題だけで、丸め操作がその仮定を満たすことまで確認済みとは数えない。

全ソース、過去の成功ログ、今回の BLOCKED 記録、再実行スクリプトは、証明ソースと再現資料に収録した。Lean本体とコンパイル済みMathlibは同梱していない。

ソースの同一性。 検証した MomentIslands.lean のSHA-256は

3f29d4e1daad5ed467c6ef2a832a067b03546a2ca35293983f3675e76e70c9fa

である。再現資料には版、実行コマンド、最終成功ログ、途中の入力ルート指定エラー、公式配布物のハッシュを残した。

前回（2026 09 08）の環境固有の互換処理。 公式Leanが実行場所を探す際、プロセス番号とprocfsの見え方の不一致が生じた。このため、同じプロセスの実行ファイルを指す readlink の参照先だけを、プロセス番号を含むパスから /proc/self/exe へ置き換えるCの互換処理を使用した。Leanのソース、数学カーネル、証明検査、公式実行ファイルは変更していない。処理のCソースとハッシュも記録している。通常のLinux環境ではこの互換処理は不要である。

標準環境で、従来の核だけを再実行するコマンドは次の通り。

lake update
lake exe cache get
lake env lean MomentIslands.lean

追加モジュールも含めた検証は、ソース一式を展開したプロジェクト内で lake update、lake exe cache get、python3 verify.py と進める。スクリプトは版・commitを照合し、ビルドと定理ごとの公理依存を記録する。今回の保存記録は実行環境不足を表す BLOCKED である。再実行スクリプト自体も、正常なLean環境で一連の成功をまだ確認していない。

独立した有限計算。

対象	検査した範囲	結果
普遍順位式と非負分解	24,300降順格子列、150,723順位分割	全PASS
誤差帯の鋭さと経路	75,623帯保証と同数の二線分経路、9,240等号配置	全PASS
最近丸め	閾値内の1,880配置	全PASS
誤差帯の辺グラフ	75多面体、8,087辺、583閾値検査	全PASS
非整数切片の順位差	317,353格子列、633,302平方不等式、9,900達成配置	全PASS
非整数切片の成分数	1,695水準の重み付きグラフ	全PASS
広い誤差帯（T9）の辺グラフ	60有理多面体、660臨界値・中点条件	全PASS（v1.1で追加）
穴の遷移	6段階のセル複体と $\mathbb F_2$ 境界行列	全PASS

これらは整数・有理数による厳密な有限検査である。同じ列に複数の検査を行っているため、件数の合計を独立標本数とはしない。連続空間の全ての点への一般性は、本文の証明と、該当する範囲のLean証明が担う。

9. 新規性の照合：何が既知の系なのか

2026 09 09の追加調査で、最上位・最下位の順位版T1と整数総和の場合が、既知境界の系または短い初等的帰結であることをさらに明確にした。内部順位・非整数総和の一般式や、T2・T9の同じ明示公式は今回未同定である。「未同定」は検索の現状であり、新規性の証拠ではない。 順位統計量、二乗和、trace、近射影性、HOMO/LUMO境界、SPREAD制約、hypersimplexなどの別表現を確認した限定的な照合であり、包括的な優先権調査ではない。

最大成分の鋭い境界には2008年の明示的先行例がある。 Rosenberg–Jakobsson (2008), Theorem 1(ii), p.2028 は、確率ベクトル $P=(p_i)$ の二乗和 $1/2<I(P)=\sum_i p_i^2<1$ に対し、

\max_i p_i\ge\frac{1+\sqrt{2I(P)-1}}2 \tag{15}

という鋭い下限を明示している。 $I(P)=1$ は一点集中なので同じ式が成立する。前稿はこの論文のAppendix Lemma 3を二乗和最大化の出典としていたが、主定理にも直接の先行結果があった。Rastegin (2023), Theorem 1、式(30)–(31) も同じ高純度枝を明示している。2008年が初出だとまでは断定しない。

整数総和の丸め上限は初等的に直接証明できる。 左右それぞれで「非負数の二乗和は和の二乗以下」を使う。まず引用に依存しない証明を示し、その後で(15)への集約による対応を記す。

$x_i\in[0,1]$ 、 $S=s\in\mathbb Z$ 、 $D<1/2$ とする。最近0/1丸め $z$ を一つ取り、 $d_i=\min(x_i,1-x_i)$ と置く。 $d_i\le2x_i(1-x_i)$ なので $\sum_i d_i<1$ 。従って

\left|s-\sum_i z_i\right| \le\sum_i d_i<1.

左辺は整数だから0であり、丸めは総和を保存する。もしある座標が $1/2$ なら、そこで異なる二つの丸めがともに同じ総和 $s$ を持つことになり矛盾するため、丸めは一意である。

\rho=\sum_{z_i=0}x_i =\sum_{z_i=1}(1-x_i)<\frac12

と置く。両側の各誤差は非負なので、それぞれの二乗和は $\rho^2$ 以下である。従って

\begin{aligned} D&=2\rho-\sum_{z_i=0}x_i^2 -\sum_{z_i=1}(1-x_i)^2\\ &\ge2\rho(1-\rho). \end{aligned}

すなわち $(1-2\rho)^2\ge1-2D$ 。 $\rho<1/2$ から非負の平方根を取ることができ、

1-2\rho\ge\sqrt{1-2D}.

よって

\|x-z\|_1=2\rho\le1-\sqrt{1-2D}. \tag{16}

任意の部分集合に対する和の誤差は、正部分と負部分の質量がともに $\rho$ であることから $\rho$ 以下。また、1へ丸めた側の最小値は $1-\rho$ 以上、0へ丸めた側の最大値は $\rho$ 以下なので、

g_s\ge1-2\rho\ge\sqrt{1-2D}. \tag{17}

これで(16)(17)の直接証明が完了する。既存Leanの balanced_error_defect と balanced_error_sharp_bound は、等しい誤差質量を仮定した二乗和評価と反転を検証済みである。丸めからこの仮定への接続は追加した Rounding.lean の対象で、実行未確認である。 $s=0,n$ は二値列一つの自明な場合として分けられる。順位版T1で $S\in\mathbb Z$ かつ $S\ne s$ なら $(S-s)^2\ge1$ 、また $S=s,D\ge1/2$ なら $2D\ge1$ なので、残りは自明である。従って整数総和の場合の順位版T1は全てこの初等的帰結に含まれる。

先行記述への集約による対応。 確率ベクトル $P=(1-\rho,(x_i)_{z_i=0})$ を作る。その最大成分は $1-\rho$ であり、

I(P)=(1-\rho)^2+\sum_{z_i=0}x_i^2, \qquad I(P)-(1-D)=\rho^2-\sum_{z_i=1}(1-x_i)^2\ge0.

従って $I(P)\ge1-D>1/2$ なので(15)からも

1-\rho\ge\frac{1+\sqrt{2I(P)-1}}2 \ge\frac{1+\sqrt{1-2D}}2

が得られる。この還元は丸め評価の証明に必要な前提ではなく、明示的な先行不等式との関係を示すものである。原論文が同じ丸め表現やこの集約を述べたとは主張しない。総和 $S=s$ の一般の $s$ について、初等的な直接証明と、この集約による説明の双方を持つ。これらを独立した新しい不等式とは数えない。

最上位・最下位の順位版T1は、総和が非整数でも既知の系となる。 $s=1$ のT1を整理すると

g_1^2\ge 2Q-S^2.

$S=0$ または $2Q\le S^2$ なら自明である。残りの場合は $p_i=x_i/S$ 、 $H=Q/S^2>1/2$ と正規化する。(15)と $p_{(2)}\le1-p_{(1)}$ より

g_1=S(p_{(1)}-p_{(2)}) \ge S(2p_{(1)}-1) \ge\sqrt{2Q-S^2}.

$H=1$ も一点集中として成立する。この最上位の系には、非負性があれば上限 $x_i\le1$ すら不要である。最下位 $s=n-1$ は $y_i=1-x_i$ を降順に並べる。 $D_y=D$ 、 $S_y=n-S$ 、 $g_1(y)=g_{n-1}(x)$ 、 $(S_y-1)^2=(S-(n-1))^2$ なので最上位の系に帰着する。

以上から、順位版T1の非自明な一般式について先行性をなお調べる範囲は、実質的に

n\ge4,\qquad2\le s\le n-2,\qquad S\notin\mathbb Z, \qquad2D+(S-s)^2<1

へ絞れる。これは残る場合の新規性、または既知理論から短く導けないことを証明するものではない。任意分割の符号付き平方形や余裕の恒等式の先行性も、この順位版の特殊例の還元だけでは決まらない。

非整数切片の端も直接の系である。 $m=0$ 、 $S=r$ では $p_i=x_i/r$ を確率ベクトルとして、 $E<r^2/2$ の範囲で(15)を使う。 $p_{(2)}\le1-p_{(1)}$ なので

x_{(1)}-x_{(2)} \ge r\sqrt{2Q/r^2-1} =\sqrt{r^2-2E}.

それ以降の下界0は自明である。 $m=n-1$ は補数 $1-x_i$ を同様に正規化すればよい。内部の一般 $m$ の全公式まで同じ還元で帰属したことにはならない。

対象	文献との対応と現在の扱い
箱内での二乗和最大	同一結果が既知。Rosenberg–JakobssonのAppendix Lemma 3、EllisのTheorem 1に対応
順位版T1の最上位・最下位、整数総和	既知の最大成分境界の系、または短い初等的帰結
順位版T1の内部順位・非整数総和	同じ一般式は今回未同定。新規性未確定
T1の任意分割の平方形、等号配置、余裕の恒等式	個別の先行性は未確定。特殊例の還元だけで全部の帰属を決めない
T2の三分岐、T4の丸め閾値、T5の非整数総和の順位差	T1や既知部品の明示的な帰結。同一の陳述の先行性は未確定
T3・T6・T9の成分分類	Gorbanの一般理論を具体化した系。同じ閉形式は今回未同定
領域の増大途中で島が増える現象	Gorbanの§4.2・Fig.4.5に先行例。現象自体を新規には数えない
T7–T8の面収縮と穴	個別の高次位相の先行性は未確定。成分数のグラフ定理だけで高次位相を帰属させない
行列版	スペクトル定理による標準的な系。固定座標の成分数を行列空間へ転用しない

T2が既知の部品から導けることと、三分岐の同じ陳述が既に出版されていることも区別する。具体的な公式・達成配置の有用性と、独立した新原理としての新規性は同じ評価ではない。

決定論的な順位差をモーメントから評価する問題には先行蓄積がある。 Goroncy–Rychlik (2006) は固定された外部の箱 $[0,1]$ を課さない問題を扱うため、その一般的な表題だけで今回の正の間隔を同一の既知結果と認定してはいけない。

第2節の行列版のように、近似射影行列の残差 $\operatorname{Tr}(X-X^2)$ やそのノルムから固有値情報を得る研究は、density-matrix purification の分野に先行例がある。 Rubensson–Niklasson (2013), §5.1 はtraceとFrobeniusノルムを使った評価を具体的に与える。2026 09 09の再照合では、 $A=X-X^2$ に対する $\|A\|_F^2/\operatorname{Tr}A\le\|A\|_2$ （分母非零の場合）と、残差ノルムに基づく中央の開区間の固有値排除を確認した。今回の指定順位 $s$ とtraceの整数ずれ $e$ を含む鋭式、および頑健な三分岐最小値と同じ記述は、読めた範囲では確認していない。優先権は未確定であり、用途の発想を新規には数えない。

Rubensson–Rudberg–Sałek (2008), Density matrix purification with rigorous error control は概要まで照合した。固有値と占有不変部分空間の誤差制御を扱う関連研究だが、今回全文を取得できず、個々の定理との比較が残る。書誌の実在や概要だけから、今回の式の先行性を認定してはいけない。

Wolkowicz–Styan (1980) のTheorem 2.4は順位差の上界、Theorem 2.5は固有値の全幅の上下界を扱う。Sharma–Pal (2022) のTheorem 5は上位 $k$ 個と下位 $k$ 個の和の差を評価する。これらを今回の指定した内部順位の隣接差の下界と同一視しない。SPREADについてはEkら (2022) の§3・Lemmas 3–5とAlgorithm 1まで確認した。分散下限を使って分散上限制約を伝播する設定であり、本稿の高分散側からの順位差保証とは向きが異なる。

未確認文献としては、上記の2008年近似射影論文に加え、Fahmy–Proschan (1981) の原論文本文、Schaus–Régin (2014)、Kvålseth (2015)、Kobayashi–Tanaka (2025) の個々の式が残る。MathSciNet・zbMATHを用いる包括的調査、全引用連鎖、書籍・非英語文献・索引化されていない資料の網羅は行っていない。未読部分に同じ結果がないとは判定しない。Leanによる証明検証が成功しても、これらの文献上の未確認事項が解消するわけではない。

10. 参照した一次資料

Noah A. Rosenberg and Mattias Jakobsson, The Relationship Between Homozygosity and the Frequency of the Most Frequent Allele, 2008。Theorem 1(ii), p.2028：最大成分と二乗和の鋭い境界。Appendix Lemma 3, p.2032と関連証明：二乗和最大化。
J. L. Ellis, The maximum variance of a finite dataset, given its mean, minimum, and maximum, 2025 preprint v2。全7頁、特にTheorem 1, pp.4–5、Example 2, p.6。有限データの最大分散・最大二乗和。照合した版はarXiv版である。
Alexander N. Gorban, Thermodynamic Tree: The Space of Admissible Paths, 2013。PDF版のLemma 2.1, p.11、Proposition 2.4, p.13、Lemma 3.2, pp.18–19、§4.2・Fig.4.5, pp.26–27。頂点への接続、辺による成分分類、等位集合との対応、成分数が増加する例。旧稿が参照したHTML版のLemma 4、Proposition 7、Lemma 14は、それぞれ上記PDFのLemma 2.1、Proposition 2.4、Lemma 3.2に対応する。
Alexey E. Rastegin, Uncertainty relations in terms of generalized entropies derived from information diagrams, 2023。Theorem 1、式(30)–(31)。最大成分境界の高純度枝を明示する先行記述の一つ。2008年より後の記述であり、初出として扱わない。
Agnieszka Goroncy and Tomasz Rychlik, How deviant can you be? The complete solution, 2006。§2の設定, p.637、§3 Example 2, pp.642–643。固定された外部の箱を課さない決定論的順位境界。
Henry Wolkowicz and George P. H. Styan, Bounds for eigenvalues using traces, 1980。§2、特にTheorem 2.4, 式(2.40), p.482、Theorem 2.5, pp.483–484。順位差の上界や固有値全幅の上下界を照合。
Sharma and Pal, Note on bounds for eigenvalues using traces, 2022。Theorem 5, 式(3.3), p.767。上位・下位それぞれ $k$ 個の和の差を評価する。
Emanuel H. Rubensson and Anders M. N. Niklasson, arXiv:1302.7292, 2013 preprint。§5.1、式(13)–(16)を照合。近似射影残差のtrace・ノルムと固有値境界。本文の版によって題名・式番号が異なるため、ここでは照合したPDFの識別子と箇所を示す。
Alexander Ek, Andreas Schutt, Peter J. Stuckey and Guido Tack, Explaining Propagation for Gini and Spread with Variable Mean, CP 2022。§3、Lemmas 3–5、Algorithm 1, pp.21:4–21:7。前稿の概要確認から進み、分散下限を使う制約伝播の本文を照合した。
Parameterless stopping criteria for recursive density matrix expansions。導入、Theorem 1、§6を確認。近接する反復停止判定の研究であり、今回の式と同一だと認定した資料ではない。
Lean 4.19.0公式リリース、Mathlib v4.19.0。形式検証の固定版。今回取得したMathlibソースと、過去に使用した版のcommitは一致する。

本文の式の直接比較が残る重要な資料は次の通り。

資料	今回確認できた範囲・残る照合
Rubensson–Rudberg–Sałek, Density matrix purification with rigorous error control (2008)	書誌・概要まで。trace誤差と固有値境界の個々の定理の比較が残る
Fahmy–Proschan, Bounds on Differences of Order Statistics (1981)	原論文本文は未読。後続論文からの言及と原論文の直接照合を区別する
Schaus–Régin, Bound-consistent spread constraint (2014)	概要・書誌まで。制約下の分散境界の本文照合が残る
Kvålseth, Bounds on Sample Variation Measures Based on Majorization (2015)	概要・参考文献まで。majorizationによる既知境界への還元が残る
Kobayashi–Tanaka, Unified relationship between mean, variance, and an arbitrary number of quantiles (2025)	概要まで。有限列と外部箱の条件を含むかの本文照合が残る

近接する位相文献として、The Wonderful Geometry of the Vandermonde map の§2.1・Lemma 2.12など、およびHarper, Morse Matchings on a Hypersimplex の面構造・Morse matchingも確認した。順序室内の連結性や整数和のhypersimplexを、今回のラベル付き非整数切片の具体的な遷移列と同一視しない。これらは関連箇所の照合であり、全証明や全参考文献を精読したものではない。

参照した箇所の範囲を超えて、論文全体を今回の式と同一だと扱わない。本文の帰属、直接の証明、検証ログを併せて判断できる形にした。追加監査の原文も統合資料に収録している。

11. 次に確認すること

T9により $1/2<\eta<1$ の成分数は一般の $n,s$ まで分類できた。残る数学的課題は、この領域の高次ホモトピー型、および $\eta\ge1$ でさらに多くの整数総和の頂点が入る場合である。

形式証明では、まず追加33宣言のLean実行と必要な修正、本文の仮定・結論との照合を完了する。T2の達成配置・全分岐とT4の丸め総和保存の候補コードは既にある。T3の二線分経路、T6–T9の連結性と面収縮はその後の形式化対象である。T1の任意分割による平方不等式は、本文と既存の形式ファイルで同じ仮定・結論に揃えた。

文献調査では、箱制約付きの内部順位・非整数総和における順位差、近射影行列の固有値境界、制約伝播、凸集合を除いた多面体の面複体を重点的に照合する。特にT1とT2の別表記を持つ既存定理を探し、見つかった場合は帰属を更新する。

Fableへの次の確認では、T1の任意分割と符号の扱い、T2・T4の端点、T9の辺の全列挙と同時閾値、T7–T8の収縮とホモトピー型、追加Leanコードと本文の一致を優先する。レビュー依頼に、再検査すべき箇所と証拠の読み方をまとめた。

応用を検討する際は、平均・分散の誤差をどう $S$ と $D$ の厳密な許容条件へ変換するかを、実際の観測モデルごとに確かめる。本稿が扱うのは確定的な制約であり、誤差幅を置いただけで確率的な信頼度が得られるわけではない。

既存の公開成果E01・E02の台帳は変更していない。本稿はX01の追加探索を記録するものであり、T1–T9は本文内の命題を参照するための番号であって、学術的新規性を認定した公開成果番号ではない。

Research note · Version 1.2 · 2026 09 09 · Exploration candidate X01 · Consolidated review edition

The principal finite-sample inequality has a preserved successful Lean run from 2026 09 08, covering 14 theorem declarations in the original module. The 33 additional proof scripts are NOT COMPILED: the pinned Mathlib source was obtained, but the Lean executable is absent and its download stopped at a cancelled network approval. The mathematical proofs, finite computational checks, historical Lean result, and uncompiled extension are distinguished throughout this document. No claim of established academic novelty is made.

1. What the two moments can reveal

Version 1.2: consolidated material for further review (2026 09 09). This single document combines T1–T9, their proofs and figures, the additional novelty audit, and the formalization supplement with its sources and execution records. The earlier Fable5.1 review led to the clarified partition statement and T9. The new audit identifies older explicit bounds in Rosenberg–Jakobsson (2008) and an existing example of nonmonotone component counts in Gorban (2013). These attributions narrow the possible novelty claims. A further Fable review is planned, not recorded as completed; see the review request.

Let $n\ge2$ , let $x=(x_1,\ldots,x_n)\in[0,1]^n$ , and write its entries in decreasing order as $x_{(1)}\ge\cdots\ge x_{(n)}$ . Define

S=\sum_i x_i,\qquad Q=\sum_i x_i^2,\qquad D=S-Q=\sum_i x_i(1-x_i).

The nonnegative quantity $D$ is zero exactly at binary vectors. With mean $\mu=S/n$ and variance $V=n^{-1}\sum_i(x_i-\mu)^2$ , it satisfies

D=n\bigl[\mu(1-\mu)-V\bigr].

Thus $D$ measures the deficit from the endpoint variance bound $\mu(1-\mu)$ , multiplied by $n$ . For a fixed noninteger sum, that endpoint bound need not be attainable by a finite vector; Section 6 accounts for the resulting positive minimum of $D$ . The question is how much this aggregate information forces the individual entries to separate.

The useful regime is nearly binary data, with small total defect and a sum close to a specified integer $1\le s<n$ . Write $e=S-s$ . This is not a positive-gap guarantee for broadly distributed statistical data. More precisely, the positive certificate below satisfies

2D+e^2<1\quad\Longleftrightarrow\quad 0\le\mu(1-\mu)-V<\frac{1-e^2}{2n}.

Thus $|e|<1$ is necessary, and the variance must lie within $O(1/n)$ of the endpoint bound. For a fixed finite noninteger sum $S=m+r$ , $0\le r<1$ , the actual maximum variance is $\mu(1-\mu)-r(1-r)/n$ , as shown in Section 6. Nearly idempotent self-adjoint matrices are a natural application through their eigenvalues; Section 2 states that corollary and explains why the vector topology does not transfer to the full matrix space.

For an integer $1\le s<n$ , put $e=S-s$ and $g_s=x_{(s)}-x_{(s+1)}$ . We prove

\boxed{2D+e^2+g_s^2\ge1.}\tag{1}

If $2D+e^2<1$ , the largest $s$ entries are separated from the others by a positive gap. This also prevents the identity of that top group from changing along a continuous deformation that preserves the strict inequality. Aggregate statistics certify separation; they do not identify the labels of the largest entries without observing the vector.

The note develops this observation in three directions: an exact worst-case gap under uncertainty in the sum, a constructive classification of connected components, and a small example where holes appear and disappear. All component counts concern labeled vectors, not vectors modulo permutation and not one-dimensional projections onto a partial sum.

Figure 1

A forced gap between two ranks

Switch configurations to inspect the relation between total error, defect, and the rank gap.

Configuration

Displayed numbers are rounded. These configurations illustrate the result; the nonnegative decomposition in the text proves it universally.

2. A universal rank inequality, its equality cases, and stability

Theorem 1: the square inequality for an arbitrary finite partition

Assume $x\in[0,1]^n$ . Choose any nonempty proper subset $I$ of the index set, put $J=I^c$ and $s=|I|$ , and choose indices attaining the boundary extrema:

u=\min_{i\in I}x_i=x_a,\quad v=\max_{j\in J}x_j=x_b,\quad g_I=u-v.

Here $a\in I$ , $b\in J$ , and $g_I$ is signed. Then

\boxed{2D+(S-s)^2+g_I^2\ge1.}

Neither integrality of $S$ nor cross-ordering $u\ge v$ is assumed for this squared statement. If $I$ is the set of the largest $s$ entries, then $g_I=g_s\ge0$ , and it gives (1) and

g_s\ge\sqrt{\max\{1-2D-(S-s)^2,0\}}.

For an arbitrary partition, the squared inequality does not imply a positive signed gap. The square-root conclusion additionally requires $u\ge v$ .

Proof. Write $g=g_I$ , $e=S-s$ , and define

\sigma=\sum_{i\in I}(1-x_i),\qquad \rho=\sum_{j\in J}x_j,

A=\sigma-(1-u)=\sum_{i\in I\setminus\{a\}}(1-x_i),\qquad B=\rho-v=\sum_{j\in J\setminus\{b\}}x_j.

Empty sums are zero. In particular $A,B\ge0$ , and $e=\rho-\sigma$ . Define

T=\sum_{i\in I}(x_i-u)(1-x_i) +\sum_{j\in J}(v-x_j)x_j.

Every summand is nonnegative by the extremum condition on its own side and the box bounds; cross-ordering is not used. The following exact identity holds:

\boxed{ 2D+e^2+g^2-1 =2T+2(1-v)A+2uB+(B-A)^2. }\tag{2}

For $i\in I$ , write

x_i(1-x_i)=u(1-x_i)+(x_i-u)(1-x_i).

For $i\in J$ , write

x_i(1-x_i)=(1-v)x_i+(v-x_i)x_i.

Summing gives $D=u\sigma+(1-v)\rho+T$ . Substitute $\sigma=1-u+A$ , $\rho=v+B$ , $e=u+v-1+B-A$ , and $g=u-v$ . Expanding and collecting terms gives (2). Since $0\le u\le1$ and $0\le v\le1$ , its right-hand side is nonnegative. This proves the partition statement and, by choosing a top set, (1). This is an identity for arbitrary finite vectors, not an inference from numerical samples. ∎

Equality and quantitative stability

If $g>0$ , then $u\ge g$ and $1-v\ge g$ . Hence, with $R=2D+e^2+g^2-1$ ,

R\ge2g(A+B),\qquad \boxed{A+B\le\frac{R}{2g}.}\tag{3}

Consequently, for $g>0$ , equality in (1) holds precisely for the sorted vectors

(\underbrace{1,\ldots,1}_{s-1},u,v, \underbrace{0,\ldots,0}_{n-s-1}).\tag{4}

Indeed, $R=0$ forces $A=B=0$ ; nonnegative summands then force all the indicated entries to be endpoints. Conversely, (4) makes $A=B=T=0$ , so (2) gives equality.

More generally, $g\ge\gamma>0$ and $R\le\varepsilon$ force the total distance of all entries other than the boundary pair from their indicated endpoints to be at most $\varepsilon/(2\gamma)$ . This estimate degenerates as the gap approaches zero. Replacing those entries by endpoints does not necessarily preserve $S$ : the change in the sum is $A-B$ .

Corollary: a spectral certificate for a Hermitian contraction

Let $X$ be an $n\times n$ self-adjoint matrix with $0\le X\le I_n$ in the operator order, and let $\lambda_1\ge\cdots\ge\lambda_n$ be its eigenvalues. For $1\le s<n$ ,

2\operatorname{Tr}(X-X^2) +(\operatorname{Tr}X-s)^2+(\lambda_s-\lambda_{s+1})^2\ge1,

\lambda_s-\lambda_{s+1}\ge \sqrt{\max\{1-2\operatorname{Tr}(X-X^2) -(\operatorname{Tr}X-s)^2,0\}}.

Proof. By the spectral theorem, $\lambda_i\in[0,1]$ , $\operatorname{Tr}X=\sum_i\lambda_i$ , and $\operatorname{Tr}(X-X^2)=\sum_i\lambda_i(1-\lambda_i)$ . Apply Theorem 1 and its rank corollary to the eigenvalue vector. ∎

This immediate transfer is a useful application, rather than an independent principal theorem. The gap formulas in Sections 3 and 6 transfer in the same way. The component and hole classifications require a different model: they concern labeled coordinates, equivalently diagonal matrices in a fixed basis. Eigenvectors may rotate in the full matrix space. For example,

P_\theta=\begin{pmatrix} \cos^2\theta&\cos\theta\sin\theta\\ \cos\theta\sin\theta&\sin^2\theta \end{pmatrix},\qquad0\le\theta\le\frac\pi2,

is a continuous path from $\operatorname{diag}(1,0)$ to $\operatorname{diag}(0,1)$ , with $P_\theta^2=P_\theta$ , trace $1$ , and defect $D=0$ throughout. More generally, complex orthogonal projections of the same rank are unitarily conjugate, and varying the eigenphases of a unitary matrix continuously supplies a connecting path. Hence the vector count $\binom ns$ cannot be asserted for the full matrix space. Reframing the entire note around matrices would leave the gap formulas largely intact, but would require new topological questions and proofs for the component and hole sections.

3. The exact gap when the sum is uncertain

Fix $1\le s<n$ , $0\le\eta\le1/2$ , and $\delta\ge0$ . Consider

P_{s,\eta}=\{x\in[0,1]^n:|S-s|\le\eta\}, \qquad F_{s,\eta,\delta}=\{x\in P_{s,\eta}:D(x)\le\delta\}.

Here $\eta$ bounds the sum error; the corresponding mean error is $\eta/n$ . This is a joint constraint on $S$ and $D=S-Q$ , not an arbitrary rectangular uncertainty set in the mean and variance.

Set

\delta_0=\eta(1-\eta),\qquad \delta_c=\frac{1-\eta^2}{2}.

Theorem 2: a sharp three-branch formula

\boxed{ \min_{x\in F_{s,\eta,\delta}}g_s(x)= \begin{cases} \dfrac{1+\sqrt{1-4\delta}}2,&0\le\delta\le\delta_0,\\[5pt] \sqrt{1-2\delta-\eta^2},&\delta_0\le\delta\le\delta_c,\\[3pt] 0,&\delta\ge\delta_c. \end{cases}}\tag{5}

The formulas agree at shared endpoints. When $\eta=0$ , the first branch consists only of $\delta=0$ . The set is nonempty because it contains all binary vectors with $s$ ones; compactness and continuity also ensure the minimum exists.

Figure 2

The smallest gap under moment uncertainty

The solid curve is the sharp, attainable bound. The dashed curve uses only the universal inequality.

Total-error allowance η 0.100

Defect budget δ 0.200

η bounds error in the total, not in the mean. Assume 0 ≤ η ≤ 1/2. Each point on the curve optimizes over every vector satisfying D ≤ δ.

Lemma: the maximum squared sum at a fixed total

For $y\in[0,1]^N$ with $\sum_i y_i=t$ ,

\sum_i y_i^2\le\phi(t):=\lfloor t\rfloor+\{t\}^2, \qquad \sum_i y_i(1-y_i)\ge\{t\}(1-\{t\}).\tag{6}

Proof. If two entries satisfy $0<a\le b<1$ , set $h=\min(a,1-b)>0$ and replace $(a,b)$ by $(a-h,b+h)$ . The sum stays fixed, both entries remain in the box, and the squared sum increases by $2h(b-a)+2h^2>0$ . At least one of the two entries becomes an endpoint. Repeating this finite operation leaves at most one nonintegral entry. The resulting vector has $\lfloor t\rfloor$ ones, one entry $\{t\}$ if this is nonzero, and zeros elsewhere. Its squared sum is $\phi(t)$ , which proves both inequalities. ∎

This packed-vector extremum is classical; see Rosenberg–Jakobsson, Appendix Lemma 3, and the finite-data formulation by Ellis [R1–R2]. Its proof is included to make the optimization below self-contained.

Proof of the lower bounds

Let $a=|S-s|\le\eta\le1/2$ . Equation (6) gives $D\ge a(1-a)$ , including either sign of $S-s$ . For $S=s-a$ , the fractional part is $1-a$ when $a>0$ , and zero when $a=0$ ; both give the stated defect bound.

If $0\le\delta\le\delta_0$ , define

b=\frac{1-\sqrt{1-4\delta}}2.

Since $t(1-t)$ is increasing on $[0,1/2]$ , we obtain $a\le b\le\eta$ . Theorem 1 now yields

g_s^2\ge1-2D-e^2\ge1-2\delta-b^2=(1-b)^2.

As $g_s\ge0$ , this proves the first branch. For $\delta_0\le\delta\le\delta_c$ , Theorem 1 directly gives $g_s^2\ge1-2\delta-\eta^2\ge0$ . The bound $g_s\ge0$ proves the third branch's lower bound.

Attainment in every branch

Use $s-1$ initial ones and $n-s-1$ final zeros, leaving exactly two boundary entries.

For the first branch, choose $(1-b,0)$ . Then $S=s-b$ , $D=b(1-b)=\delta$ , and $g_s=1-b$ .

For the second branch, put $h=\sqrt{1-2\delta-\eta^2}$ and choose

\left(\frac{1-\eta+h}{2},\frac{1-\eta-h}{2}\right).\tag{7}

The condition $\delta\ge\delta_0$ is equivalent to $h\le1-\eta$ ; hence both entries lie in $[0,1]$ . Their sum is $1-\eta$ , their difference is $h$ , and their defect is $(1-\eta^2-h^2)/2=\delta$ . Finally, for $\delta\ge\delta_c$ , the same construction at $h=0$ has an exact tie and remains feasible. This proves all three branches and their sharpness. ∎

For example, $n=6,s=2,\eta=0.1,\delta=0.2$ forces a gap of at least $\sqrt{0.59}\approx0.7681146$ . Equality is attained by

(1,0.8340573\ldots,0.0659427\ldots,0,0,0).

There is also stability of the optimizing configurations. If the value in (5) is $q>0$ , the preceding bounds imply $2D+e^2\le1-q^2$ . Therefore

0\le R\le g_s^2-q^2, \qquad A+B\le\frac{g_s^2-q^2}{2g_s}.

A nearly minimal positive gap requires nearly all nonbinary mass to concentrate in the two boundary entries.

4. Components and a constructive path to a binary representative

Theorem 3: the exact merging threshold

For the same parameter range,

\boxed{ \#\pi_0(F_{s,\eta,\delta})= \begin{cases} \binom ns,&0\le\delta<\delta_c,\\ 1,&\delta\ge\delta_c. \end{cases}}\tag{8}

Here $\pi_0$ denotes path components. Below the threshold, a component is specified by the labels of the largest $s$ entries. At equality the components have already merged. The result is an explicit consequence of the general polytope-complement theory of Gorban [R3], but the following proof is independent of that theory.

Step 1: at most two line segments reach a binary vector

Take any $x\in P_{s,\eta}$ , sort its coordinates, and let $z=(1^s,0^{n-s})$ , where $1^k$ means $k$ consecutive ones. Define weights $w_i=2x_i-1$ . Choose an auxiliary point $v$ as follows, with the first applicable case taking priority:

If $x_s\le1/2$ , choose $v=(1^{s-1},1-\eta,0^{n-s})$ .
Otherwise, if $x_{s+1}\ge1/2$ , choose $v=(1^s,\eta,0^{n-s-1})$ .
Otherwise choose $v=z$ .

All three candidates belong to the sum band. We claim

c:=\sum_i w_i(v_i-x_i)\ge0.\tag{9}

In the first case put $\alpha=w_s\le0$ and write

c=\sum_i(w_i-\alpha)(v_i-x_i) +\alpha\bigl[(s-\eta)-S\bigr].

For $i<s$ , both factors of the summand are nonnegative. For $i>s$ , both are nonpositive. For $i=s$ , the first factor is zero. The final product is nonnegative because $S\ge s-\eta$ . This proves (9).

In the second case use $\alpha=w_{s+1}\ge0$ . For $i\le s$ , both factors are nonnegative; for $i>s+1$ , both are nonpositive; and the boundary summand vanishes. The final term is $\alpha[(s+\eta)-S]\ge0$ . In the third case, $w_i$ and $z_i-x_i$ have the same sign in each coordinate, proving (9) directly. These sign arguments also explain the greedy linear optimization behind the construction.

For $0\le t\le1$ , an exact expansion now gives

D(x+t(v-x)) =D(x)-tc-t^2\|v-x\|_2^2\le D(x).\tag{10}

The segment stays in $P_{s,\eta}$ by convexity. Moreover, its defect is nonincreasing in $t$ . If $v\ne z$ , continue along the coordinate segment from $v$ to $z$ . This moves $\eta$ down to $0$ , or $1-\eta$ up to $1$ . Since $\eta\le1/2$ , the function $a(1-a)$ decreases along that segment. The sum stays in the band. Thus every $x\in F_{s,\eta,\delta}$ reaches the binary representative of its chosen top group by at most two line segments, without increasing the defect.

This constructs a path for each starting point. The choice of the auxiliary vertex has not been proved continuous as the starting point varies; the construction therefore does not assert a deformation retraction of an entire component. Gorban's earlier vertex-access Lemma 2.1 in the PDF (Lemma 4 in the HTML version) is a related general result about reaching a polytope vertex by a segment avoiding a convex obstacle [R3]. The greedy choice and the binary endpoint used here are given explicitly by the sign proof above.

Step 2: count the separated components

If $\delta<\delta_c$ , Theorem 2 gives $g_s>0$ everywhere in $F$ . The top- $s$ label set is consequently locally constant: strict separation persists in a sufficiently small coordinate neighborhood. It is therefore constant along a continuous path. Every $s$ -element label set occurs at its binary representative. Conversely, all points with one such label set are connected to that same representative by Step 1. There are exactly $\binom ns$ components.

Step 3: connect all representatives at the threshold

Suppose $\delta\ge\delta_c$ . To exchange one selected label with one unselected label, keep the other $s-1$ ones fixed and move the two relevant coordinates through

(1,0)\longrightarrow(1-\eta,0) \longrightarrow(0,1-\eta)\longrightarrow(0,1).

The first and last segments have defect at most $\delta_0$ . On the middle segment the two entries have sum $1-\eta$ ; their defect is largest when equal and is then $(1-\eta^2)/2=\delta_c$ . The sum error never exceeds $\eta$ . Every two $s$ -element subsets can be joined by a sequence of single-element exchanges, so all binary representatives are connected. Step 1 connects all other points to them. This proves (8), including $\eta=0$ . ∎

Two limits of the statement

The two-segment construction cannot in general be replaced by a direct segment to $z$ . Let $n=2,s=1,\eta=1/2$ , and $x=(3/8,1/8)$ . Here $D(x)=11/32<\delta_c=3/8$ . Along the segment $z+t(x-z)$ , where $z=(1,0)$ ,

D=\frac{3t}{4}-\frac{13t^2}{32}.

At $t=12/13$ this equals $9/26>11/32$ . Thus the asserted components need not be star-shaped about their binary representatives.

The restriction $\eta\le1/2$ is substantive. For $n=2,s=1,\eta=0.9,\delta=0.1$ , both $(0.1,0)$ and $(1,0)$ are feasible. Any continuous path between them makes the first coordinate equal $1/2$ , forcing $D\ge1/4>0.1$ . The set is disconnected even though $0.1>(1-0.9^2)/2=0.095$ . Formula (8) therefore does not extend to this larger error range.

4.1 Beyond a half-unit tolerance: the birth and merger of components

The restriction $\eta\le1/2$ in the preceding result is essential. Nevertheless, for $1/2<\eta<1$ , a complete component count in every dimension follows by examining the vertices and edges of the band polytope. Let

F_\delta=\left\{x\in[0,1]^n:\left|\sum_i x_i-s\right|\le\eta, \quad D(x)=\sum_i x_i(1-x_i)\le\delta\right\}.

Throughout this section, $n\ge2$ , $1\le s<n$ are integers, $1/2<\eta<1$ , and $\delta\ge0$ .

Theorem T9 (complete component count for a wide band). Put

a=1-\eta,\quad k=\eta(1-\eta),\quad c=\frac{1-\eta^2}{2},\quad h=\frac14,\quad b=\binom ns.

The number of path components of $F_\delta$ is

N_{n,s}(\eta,\delta)= \begin{cases} b,&0\le\delta<k,\\ (n+1)b,&k\le\delta<\min(c,h),\\ b+\binom n{s-1}+\binom n{s+1},&c\le\delta<h\quad(c<h),\\ b,&h\le\delta<c\quad(h<c),\\ 1,&\delta\ge\max(c,h). \end{cases} \tag{T9}

Rows with empty intervals are omitted. Equality $c=h$ holds precisely when $\eta=1/\sqrt2$ ; both intermediate rows then disappear. The displayed formula includes every threshold value with the indicated inequalities.

Figure 3

A wider sum band: components appear, then merge

Fix n = 2 and s = 1. The diagram counts path components of the set satisfying |x₁ + x₂ − 1| ≤ η and x₁(1 − x₁) + x₂(1 − x₂) ≤ δ. Numbers inside the band are component counts.

Sum tolerance η0.9

Defect bound δ0.1

At k = η(1 − η), four new components appear; c = (1 − η²)/2 and h = 1/4 are merger thresholds. Threshold buttons select unrounded values, with equality assigned to the state after the transition. At η = 1/√2, c = h and both mergers occur simultaneously. Labels inside very short intervals are omitted.

A graph lemma for convex obstacles. If $P$ is a compact convex polytope and $f$ is continuous and concave, the path components of $X=\{f\le\delta\}$ correspond to the components of the graph retaining vertices with $f(v)\le\delta$ and edges with $\max_e f\le\delta$ .

Here is a proof. The set $U=\{f>\delta\}$ is relatively open and convex. Process the faces meeting $U$ in decreasing dimension. In each such face choose $z\in U$ in its relative interior; relative openness guarantees that this is possible. Move each point outside $U$ outward along the ray from $z$ , until it reaches the face boundary. Convexity ensures that a ray cannot re-enter $U$ after passing a point outside it. This continuous deformation fixes the boundary and therefore glues to the identity on the other remaining faces. After finitely many steps, $X$ strongly deformation retracts onto the complex $K$ of closed faces disjoint from $U$ . Each face has a connected edge graph, so the components of $K$ are precisely those of its one-skeleton. That one-skeleton is the stated graph.

All vertices. Let $P$ impose only the box and band constraints. Its vertices have exactly three types.

Type	Coordinates	Count	$D$
$B$	$s$ ones, all remaining entries zero	$b$	0
$L$	$s-1$ ones, one entry $a$ , all others zero	$sb$	$k$
$U$	$s$ ones, one entry $\eta$ , all others zero	$(n-s)b$	$k$

Indeed, a vertex away from the band boundaries must be a cube vertex, and $s$ is the only allowed integer sum. At a band boundary, at least $n-1$ coordinates must be fixed at zero or one. The sum constraint determines the remaining coordinate as $a$ or $\eta$ . This proves completeness and the counts.

All edges and their thresholds. Edges inherited from the cube are exactly the segments $L\leftrightarrow B$ , with one coordinate ranging from $a$ to 1, and $B\leftrightarrow U$ , with one coordinate ranging from 0 to $\eta$ . Both intervals contain $1/2$ , so their maximum deficit is $h=1/4$ . Each $L$ or $U$ vertex has exactly one edge of this kind, connecting it to a unique $B$ vertex.

Edges within the band boundaries have the following four types. All coordinates other than the displayed pair are fixed at zero or one.

Band boundary	Endpoints of the moving pair	Maximum $D$
Lower, short edge	$(a,0)\leftrightarrow(0,a)$	$c$
Lower, long edge	$(1,a)\leftrightarrow(a,1)$	$d=(1-a^2)/2$
Upper, short edge	$(1,\eta)\leftrightarrow(\eta,1)$	$c$
Upper, long edge	$(\eta,0)\leftrightarrow(0,\eta)$	$d$

A type is absent if its required coordinates do not fit the dimension or sum. At the relative interior of an edge, either no band boundary is active and $n-1$ coordinates are fixed, or one band boundary is active and $n-2$ coordinates are fixed. Thus the list is exhaustive. For a moving pair with fixed sum $t$ ,

y(1-y)+(t-y)(1-t+y) =t-\frac{t^2}{2}-2(y-t/2)^2.

The midpoint belongs to each listed segment, yielding the stated maxima. Moreover,

c-k=\frac{(1-\eta)^2}{2}>0,\quad h-k=(\eta-\tfrac12)^2>0,\quad d>\max(c,h).

Counting the graph components. For $\delta<k$ , only the $B$ vertices are present. For $k\le\delta<\min(c,h)$ , all $(n+1)b$ vertices are present. No edges have yet appeared in either interval.

If $c<h$ and $c\le\delta<h$ , the short band edges appear first. On the lower boundary, they connect each group with a fixed set of $s-1$ one-coordinates; there are $\binom n{s-1}$ such groups. On the upper boundary, they connect each group with a fixed positive support of size $s+1$ ; there are $\binom n{s+1}$ groups. The $b$ binary vertices remain isolated. Adding these counts gives the third row of T9.

If $h<c$ and $h\le\delta<c$ , the cube segments appear first. Each binary vertex is the center of a star whose leaves are its associated $L$ and $U$ vertices. Because every leaf has a unique binary neighbor, these are $b$ disjoint stars.

Once $\delta\ge\max(c,h)$ , all binary vertices are connected. To see this, identify a binary vertex with its set $I$ of $s$ one-coordinates. If $I'$ differs by exchanging one element, keep the common $s-1$ ones fixed and use three edges: a cube segment, a short lower-boundary edge exchanging the position of $a$ , and another cube segment. Any two $s$ -element subsets are related by successive single-element exchanges. Every $L$ and $U$ vertex also attaches to a binary vertex, so the entire graph is connected. This occurs before the long edges appear. No new vertices appear later, and adding edges preserves connectedness. The graph lemma now proves T9. □

The reviewer's numerical example. For $n=2,s=1,\eta=0.9$ ,

k=0.09,\qquad c=0.095,\qquad h=0.25.

The component count therefore evolves as

2\ \xrightarrow{\ \delta=0.09\ }\ 6\ \xrightarrow{\ \delta=0.095\ }\ 4\ \xrightarrow{\ \delta=0.25\ }\ 1.

At each marked threshold the count on its right already applies. Thus the reviewer's observations $6,4,4,1$ at $\delta=0.09,0.10,0.20,0.26$ , respectively, are correct. Although the sets grow with $\delta$ , their component count need not decrease monotonically: new components are born at new feasible vertices.

Additional corollary: holes in dimension two. For $n=2,s=1$ , put $p=x_1+x_2-1$ and $q=x_1-x_2$ . The band polytope becomes the hexagon

|p|+|q|\le1,\quad |p|\le\eta, \qquad D=(1-p^2-q^2)/2.

For $\delta<1/2$ , the origin is excluded. Radially expanding points from the origin to the hexagon boundary gives a strong deformation retraction onto the feasible boundary: the norm never decreases, so the deficit constraint is preserved. The boundary has four sloping edges with threshold $h$ and two vertical edges with threshold $c$ . Therefore each component is contractible for $\delta<\max(c,h)$ ; for $\max(c,h)\le\delta<1/2$ , the entire boundary is feasible and $F_\delta\simeq S^1$ . For $\delta\ge1/2$ , the full hexagon is feasible and contractible. Connectedness and the disappearance of the hole are different events.

Status. T9 applies Gorban’s general theory of polytopes with convex obstacles, notably Proposition 2.4 in the PDF (Proposition 7 in the HTML). His §4.2, Fig.4.5 already gives an example where a growing feasible set acquires new isolated components. That phenomenon is therefore not claimed as a discovery here. The same explicit thresholds and binomial count for this particular band were not identified in the limited search; their priority remains unresolved. T9 has ordinary mathematical proofs and finite checks, but no Lean formalization.

5. Nearest binary rounding has an earlier threshold

Selecting the largest $s$ entries and rounding each entry at $1/2$ are different operations. For coordinatewise nearest rounding, the sharp threshold is

\boxed{\delta_R=\frac12-\eta^2.}\tag{11}

Theorem 4. If $|S-s|\le\eta\le1/2$ and $D<\delta_R$ , every coordinate has a unique nearest value in $\{0,1\}$ , and the rounded vector has exactly $s$ ones.

Proof. Suppose a coordinate equals $1/2$ . The remaining coordinates have sum $s-1/2+e$ , with $|e|\le\eta$ . The packed-square lemma, including the endpoint cases $e=\pm1/2$ , gives

D\ge\frac14+\left(\frac12+e\right) \left(\frac12-e\right) =\frac12-e^2\ge\delta_R.

Thus no coordinate can equal $1/2$ under the strict defect bound. Follow the nonincreasing-defect path from Section 4 to a binary representative with $s$ ones. No coordinate can cross $1/2$ along this path, so its rounding remains unchanged and equals that representative. ∎

The threshold is sharp for the joint guarantee of uniqueness and sum preservation. The vector

(1^{s-1},1/2,1/2-\eta,0^{n-s-1})

has $S=s-\eta$ and $D=\delta_R$ , but at least one rounding tie. When $\eta>0$ , the strict inequality $\delta_R<\delta_c$ leaves a range in which a top group remains separated while nearest rounding may have the wrong number of ones. Replace the boundary pair by

(1/2-\varepsilon,1/2-\eta+\varepsilon).

For sufficiently small $0<\varepsilon<\eta/2$ , both are below $1/2$ , their gap remains positive, and

D=\delta_R+2\eta\varepsilon-2\varepsilon^2 \quad\text{lies between }\delta_R\text{ and }\delta_c.

For example, $s=1,\eta=0.1,x=(0.49,0.41)$ gives $D=0.4918<\delta_c=0.495$ . The first entry is the unique largest entry, but both entries round to zero.

6. An exact noninteger sum produces two merging events

Let $S=m+r$ , where $m\in\{0,\ldots,n-1\}$ and $0<r<1$ . Define

H_S=\{x\in[0,1]^n:\sum_i x_i=S\},\qquad M=m+r^2,

E=M-Q,\qquad E_{\max}=M-\frac{S^2}{n}, \qquad X_E=\{x\in H_S:Q=M-E\}.

The feasible range is exactly $0\le E\le E_{\max}$ . The packed-square lemma gives the maximum $Q=M$ . The identity $Q=S^2/n+\sum_i(x_i-S/n)^2$ gives the minimum $S^2/n$ , uniquely attained at $c=(S/n,\ldots,S/n)$ . Interpolation from $c$ to a packed vertex attains every intermediate value.

The quantities $D$ and $E$ must not be confused:

D=r(1-r)+E.\tag{12}

Theorem 5: both relevant rank gaps are sharp

For every feasible $E$ , and only when the stated rank exists,

\boxed{ \min_{x\in X_E}(x_{(m)}-x_{(m+1)}) =\sqrt{\max\{(1-r)^2-2E,0\}} }\quad(m\ge1),\tag{13}

\boxed{ \min_{x\in X_E}(x_{(m+1)}-x_{(m+2)}) =\sqrt{\max\{r^2-2E,0\}} }\quad(m+1<n).\tag{14}

Proof of the lower bounds. Apply Theorem 1 with $s=m$ , so $e=r$ , and substitute (12). This yields $g_m^2\ge(1-r)^2-2E$ . Apply it with $s=m+1$ , so $e=r-1$ , to get $g_{m+1}^2\ge r^2-2E$ . The gaps are nonnegative, giving the displayed bounds.

Attainment before the thresholds. Put $b=(1-r)^2/2$ . For $0\le E\le b$ , let $d=\sqrt{(1-r)^2-2E}$ and choose

w=(1^{m-1},(1+r+d)/2,(1+r-d)/2,0^{n-m-1}).

Since $0\le d\le1-r$ , this is a sorted box vector with sum $S$ , gap $d$ , and squared sum $M-E$ . Similarly, put $a=r^2/2$ . For $0\le E\le a$ , the vector

w=(1^m,(r+d)/2,(r-d)/2,0^{n-m-2}), \qquad d=\sqrt{r^2-2E},

attains (14). The assumed rank conditions make all multiplicities valid.

Attainment after the thresholds. In either construction, let $y$ be the vector at its threshold $t$ , where $t=b$ or $a$ , so the boundary pair is tied. Interpolate by $x(\lambda)=(1-\lambda)y+\lambda c$ , $0\le\lambda\le1$ . Sorting is preserved and the same pair remains tied. Orthogonality to the constant vector gives

E(x(\lambda))=E_{\max}-(1-\lambda)^2(E_{\max}-t).

Thus every $E\in[t,E_{\max}]$ is attained with gap zero. If $t=E_{\max}$ , only the endpoint needs to be considered. ∎

Figure 4

Two rank gaps vanish at different thresholds

Fix n = 6 and m = 2, then vary r and E. Components refer to the full set of labelled vectors.

Fractional total r 0.300

Squared-norm deficit E 0.100

a = r²/2 and b = (1−r)²/2. Merging has already occurred at equality. E = Emax is the single uniform vector. Curves show the minimum of each rank gap.

Theorem 6: component counts from a weighted edge graph

For the internal case $1\le m\le n-2$ , set

a=r^2/2,\qquad b=(1-r)^2/2,\qquad N=\binom nm(n-m).

The following table gives the number of path components of $X_E$ . Empty intervals are ignored.

Range of $E$	Number of components	Constant label within a component
$E<a$ and $E<b$	$N$	top- $m$ set $A$ , together with the next label $j$
$a\le E<b$	$\binom nm$	top- $m$ set $A$
$b\le E<a$	$\binom n{m+1}$	top- $(m+1)$ set
$E\ge a$ and $E\ge b$	$1$	no separation into components

We use the following known result explicitly. Gorban's Thermodynamic Tree, Proposition 2.4 in the PDF (Proposition 7 in the HTML), identifies the path components of a convex polytope $P$ minus a convex set $U$ with those of the graph formed by vertices outside $U$ and edges entirely outside $U$ . His Lemma 3.2 in the PDF (Lemma 14 in the HTML) identifies the relevant components of a strictly convex level set with those of its superlevel set [R3]. In this quadratic setting the latter step also has the direct deformation retraction below.

Vertices and edges. A point of $H_S$ with two entries strictly between $0$ and $1$ admits a nonzero perturbation of those entries with fixed sum, in both signs. Hence it is not a vertex. All vertices are therefore packed vectors: $m$ ones, one $r$ , and zeros elsewhere. Conversely, fixing those $n-1$ endpoint coordinates fixes the remaining coordinate, so each is a vertex. Label it $(A,j)$ , with $|A|=m$ , $j\notin A$ .

Every edge has exactly two free coordinates in its relative interior. Indeed, fixing its endpoint coordinates leaves a cube slice of dimension one, so the number of free coordinates is two. Their sum must be $r$ or $1+r$ . Thus there are only two edge types:

Type	Moving coordinates	Maximum $E$ on the edge
L	$(r,0)\leftrightarrow(0,r)$	$a=r^2/2$
U	$(1,r)\leftrightarrow(r,1)$	$b=(1-r)^2/2$

Each maximum occurs at the midpoint, by direct expansion of the squared sum. Define

\Omega_E=\{x\in H_S:Q\ge M-E\},\qquad U_E=\{x\in H_S:Q<M-E\}.

The removed set $U_E$ is relatively open and convex. An L edge is wholly in $\Omega_E$ exactly when $E\ge a$ ; a U edge is wholly there exactly when $E\ge b$ . The use of the strict inequality in $U_E$ explains why merging is already complete at the threshold itself.

For $E<E_{\max}$ , put $R_E=\sqrt{M-E-S^2/n}>0$ . Every $x\in\Omega_E$ has $\|x-c\|\ge R_E$ , and

p_E(x)=c+\frac{R_E}{\|x-c\|}(x-c)

belongs to $X_E$ . The homotopy

c+\left[(1-t)+t\frac{R_E}{\|x-c\|}\right](x-c), \qquad0\le t\le1,

stays in $H_S$ by convexity and has radius at least $R_E$ , so it remains in $\Omega_E$ . It fixes $X_E$ . Hence $\Omega_E$ strongly deformation retracts onto $X_E$ . At $E=E_{\max}$ , $X_E=\{c\}$ is handled directly.

Count the surviving graph. With neither edge type present, all $N$ vertices are isolated. With only L edges, $A$ is fixed and the $n-m$ choices of $j$ form a complete graph; this gives $\binom nm$ components. With only U edges, $B=A\cup\{j\}$ is fixed and its $m+1$ choices of $j$ form a complete graph; this gives $\binom n{m+1}$ components. With both types present, the graph is connected. Explicitly, use an L move to designate a desired new element as the fractional coordinate, then a U move to exchange it with an element of $A$ . Repeated single-element exchanges connect all $m$ -subsets, and L moves connect all fractional labels for each subset. Gorban's proposition and the retraction transfer these counts to $X_E$ .

Finally, (13) keeps the top- $m$ label set fixed whenever $E<b$ , and (14) keeps the top- $(m+1)$ set fixed whenever $E<a$ . Each possible label is realized on the segment from its packed vertex toward $c$ . The number of labels equals the component count in each row, proving the stated labeling. ∎

For $r<1/2$ , the counts are $N\to\binom nm\to1$ ; for $r>1/2$ , they are $N\to\binom n{m+1}\to1$ . When $r=1/2$ , both edge types enter at $1/8$ , and the intermediate stage disappears. For example, $n=6,S=2.3$ gives $60\to15\to1$ at $E=0.045$ and $0.245$ .

At the boundaries, $m=0$ has only L edges and only (14): $n$ components merge into one at $E=a$ . The case $m=n-1$ has only U edges and only (13), with merging at $E=b$ . For $n=2$ , the applicable threshold equals $E_{\max}$ , so two points meet at the uniform point. If one allows $n=1$ , the whole slice is already a single point.

7. Beyond connectivity: holes appear and disappear

Take $n=4,S=5/4$ . Then $m=1,r=1/4$ , $M=17/16$ , and $E_{\max}=43/64$ . The component count is $12\to4\to1$ , but this does not describe all changes in shape.

The homotopy sequence to be proved

Range of $E$	Homotopy type of $X_E$	Betti numbers $(\beta_0,\beta_1,\beta_2)$
$0\le E<1/32$	twelve points	$(12,0,0)$
$1/32\le E<1/24$	four disjoint circles	$(4,4,0)$
$1/24\le E<9/32$	four points	$(4,0,0)$
$9/32\le E<13/24$	a wedge of three circles	$(1,3,0)$
$13/24\le E<43/64$	the sphere $S^2$	$(1,0,1)$
$E=43/64$	one point	$(1,0,0)$

Having the homotopy type of a point means being contractible; it does not mean the set literally consists of one point. Likewise, the other rows specify homotopy type rather than an exact embedding or homeomorphism. The Betti numbers displayed here agree over the integers and over $\mathbb F_2$ , as follows from the identified homotopy types.

Figure 5

Holes appear, fill in, and appear again

n = 4, S = 5/4. The diagram shows the face complex K_E with the same homotopy type as the level set.

Cell-filtration stage

Model rotation 30°

E	Type	β₀, β₁, β₂
[0, 1/32)	12 points	12, 0, 0
[1/32, 1/24)	4 circles	4, 4, 0
[1/24, 9/32)	4 points	4, 0, 0
[9/32, 13/24)	Wedge of 3 circles	1, 3, 0
[13/24, 43/64)	Sphere S²	1, 0, 1
{43/64}	One point	1, 0, 0

This is a three-dimensional projection of the exact vertices, edges, and faces of K_E. Generally K_E is not a subset of X_E. They are homotopy equivalent; a point-like type need not mean the original set is a single point.

Theorem 7: retract a convex-set complement to uncut faces

Let $P$ be a compact convex polytope, let $U\subset P$ be relatively open and convex, and let $K$ be the union of all closed faces of $P$ disjoint from $U$ . Include $P$ itself among its faces. Then $P\setminus U$ strongly deformation retracts onto $K$ .

Proof. The assertion is immediate if $U$ is empty. Otherwise process every positive-dimensional face $F$ meeting $U$ , in decreasing dimension. Because $U$ is relatively open in $P$ , a point in $U\cap F$ can be perturbed within $F$ into its relative interior while staying in $U$ . Choose $c_F\in U\cap\operatorname{relint}(F)$ .

For $x\in F\setminus U$ , let $\rho_F(x)$ be the point where the ray from $c_F$ through $x$ meets $\partial F$ , where the boundary is taken within the affine hull of $F$ . The center is in the relative interior and does not belong to $F\setminus U$ , so this radial map is continuous on its domain; it fixes every boundary point. One can see continuity directly by representing $F$ with finitely many affine inequalities: the distance to the boundary along a ray is the minimum of the positive intersection parameters with the supporting hyperplanes.

The entire segment $[x,\rho_F(x)]$ avoids $U$ . Otherwise, for some farther point $y\in U$ on that ray, $x$ would lie on the segment from $c_F\in U$ to $y\in U$ , contradicting convexity of $U$ . Therefore

H_F(x,t)=(1-t)x+t\rho_F(x)

deforms $F\setminus U$ into $\partial F\setminus U$ , staying outside $U$ and fixing the boundary throughout.

At this stage, every higher-dimensional face meeting $U$ has already been collapsed. A higher-dimensional face avoiding $U$ cannot contain $F$ , since $F\cap U\ne\varnothing$ . Thus the currently remaining part of $F\setminus U$ meets the rest of the remaining space only along its boundary. Extend $H_F$ by the identity on that rest. The maps agree on the overlap, and the finite closed-face pasting property gives a continuous homotopy. After finitely many steps, only faces disjoint from $U$ remain. Vertices in $U$ were absent from the complement from the start. Every point of $K$ is fixed during every step, so the resulting deformation retraction is strong. The empty-complement case is interpreted trivially. ∎

This is an explicit finite-dimensional geometric argument; it is not presented as a newly discovered general topological theorem.

Compute the threshold for every face

Apply the lemma with $P=H_S$ and $U=U_E=\{Q<M-E\}$ . A face has $j$ coordinates fixed to $1$ , $p$ free coordinates, and the rest fixed to $0$ , with $0<S-j<p$ . Its dimension is $p-1$ . On this face,

Q=j+\sum_{\text{free }i}x_i^2 \ge j+\frac{(S-j)^2}{p},

because the sum of squared deviations of the free entries from their mean is nonnegative. Equality is attained when all free entries equal $(S-j)/p\in(0,1)$ . The face is entirely outside $U_E$ exactly when

\boxed{E\ge E_F:=M-j-\frac{(S-j)^2}{p}.}\tag{15}

Let $K_E$ contain precisely these faces. Theorem 7 gives $H_S\setminus U_E\simeq K_E$ , and Section 6 gives $H_S\setminus U_E\simeq X_E$ for $E<E_{\max}$ . These are two deformation retractions from the common space $\Omega_E=H_S\setminus U_E$ . We do not claim a direct deformation retraction from $X_E$ to $K_E$ : in general, $K_E$ is not a subset of $X_E$ . At the endpoint, $K_E=H_S$ and $X_E=\{c\}$ are both contractible.

For $n=4,S=5/4$ , this polytope is combinatorially a truncated tetrahedron. Its complete face table is

Face type	$j$	$p$	Count	Entry threshold $E_F$
vertex	1	1	12	$0$
L edge	1	2	12	$1/32$
triangular face	1	3	4	$1/24$
U edge	0	2	6	$9/32$
hexagonal face	0	3	4	$13/24$
full polytope	0	4	1	$43/64$

For completeness, the counts follow by choosing the coordinate positions: vertices choose one fixed $1$ and one fractional coordinate, giving $4\cdot3=12$ ; L edges choose a fixed $1$ and two free positions among the other three, giving $4\binom32=12$ ; triangular faces choose their fixed $1$ , giving four; U edges choose their two free positions, giving $\binom42=6$ ; hexagonal faces choose their fixed $0$ , giving four. No other possibilities satisfy $0<5/4-j<p$ in the relevant dimension.

Theorem 8: the six-stage homotopy classification

For $n=4,S=5/4$ , the six homotopy types and their exact parameter intervals are those stated at the start of this section.

Proof. Read the face complex $K_E$ at each successive threshold.

Initially $K_E$ consists of twelve isolated vertices. At $E=1/32$ , the twelve L edges form four disjoint triangular boundaries, one for each position of the fixed $1$ . At $E=1/24$ , the four triangular faces enter and fill these circles, giving four disjoint disks.

At $E=9/32$ , the six U edges enter. Each pair of triangular disks is joined by one such edge: the edge with free positions $i,j$ connects the disk whose fixed $1$ is at $i$ to the one whose fixed $1$ is at $j$ . In each triangle, choose one of its boundary edges. It is a free edge, because no other two-dimensional cell meets it. Collapse the triangle together with that edge onto the other two edges, keeping all three vertices and all joining edges. Each triangle has become a tree connecting its three attachment points. Contracting these four trees in the resulting graph gives the complete graph $K_4$ ; these elementary collapses and graph-tree contractions preserve homotopy type. Finally, contract a spanning tree of $K_4$ . Its $6-4+1=3$ remaining edges form a wedge of three circles.

At $E=13/24$ , all hexagonal faces enter, so $K_E$ is the entire boundary of the three-dimensional convex polytope. Radial projection from any interior point identifies that boundary homeomorphically with $S^2$ . At $E=43/64$ , the whole polytope enters and is contractible. These arguments prove every row, including the equality conventions. ∎

Independent computation enumerated the faces and formed the cellular boundary matrices over $\mathbb F_2$ , verified that consecutive boundary maps compose to zero, and recovered the displayed Betti numbers. These finite calculations corroborate the result. The homotopy types themselves follow from the direct cell descriptions above, not from mod-2 homology alone.

8. What Lean verified, and what it did not

The recorded run used Lean 4.19.0 and Mathlib v4.19.0, at Mathlib commit c44e0c8ee63ca166450922a373c7409c5d26b00b. It compiled all 14 theorem declarations in MomentIslands.lean, with final exit code 0. These are proofs over the real numbers and arbitrary finite index types, not numerical-grid checks.

That successful compilation was performed on 2026 09 08 and is recorded in the accompanying log. On 2026 09 09, the official tag-to-commit mapping was checked and the pinned Mathlib source was obtained at the stated commit. Fetching the Lean distribution stopped twice because the network approval was cancelled before a decision was returned. A subsequent search did not recover a reusable Lean executable or distribution archive. The Mathlib source enabled API inspection but did not provide a Lean runtime or compiled dependencies. No fresh Lean compilation was performed.

The count of 14 is the number of theorem declarations in the file, not 14 independent principal results of X01. In particular, four_variable_gap_bound and four_variable_gap record an earlier four-variable impossibility example and lie outside the main results of this note.

Formal theorem names	Verified scope
`rank_gap_partition`, `rank_gap_partition_sqrt`	Theorem 1 for an arbitrary finite partition with box bounds and attained extrema; the square-root form adds cross-ordering
`finite_rank_gap`	The bridge from finite sums and boundary hypotheses to the scalar rank certificate
`rank_gap_core`, `rank_gap_sqrt`, `rank_gap_slack`	Scalar algebraic rank inequalities and a quantitative slack bound
`balanced_error_defect`, `invert_defect_bound`, `balanced_error_sharp_bound`	The quadratic defect bound and its inversion for two nonnegative error families explicitly assumed to have the same mass
`pair_square_upper`, `pair_square_upper_complement`	Two elementary two-variable squared-sum bounds
`four_variable_gap_bound`, `four_variable_gap`	Total $2$ and first-pair total $1/2$ force $Q\le3/2$ , and hence exclude $Q=9/5$ ; two auxiliary examples outside X01's main results
`concentration_from_square_deficit`	Concentration derived from a nonnegative vector's squared-sum deficit

The formal theorem rank_gap_partition takes any nontrivial finite partition $I,I^c$ , an index $a\in I$ attaining its minimum, and an index $b\notin I$ attaining the maximum outside $I$ . It proves precisely the squared statement of Theorem 1, without requiring $I$ to be a top set. The separate theorem rank_gap_partition_sqrt adds $x_b\le x_a$ and proves

\sqrt{1-2\sum_i x_i(1-x_i) -(\sum_i x_i-|I|)^2}\le x_a-x_b.

Lean's real square root is zero on negative arguments. Thus the formal statement covers that case as well; a positive radicand is what provides a positive gap. Mathematical order-statistic notation specializes this interface by choosing a top set of size $s$ . The formal input explicitly supplies the partition and indices attaining its extrema. No sorting procedure is needed to state or prove this interface, and no unformalized sorting algorithm is required to fill a gap between the partition statement in this note and the formal theorem.

The historical module does not formally establish the complete three-branch optimization with attaining vectors, the nearest-rounding count-preservation theorem, the full equality classification, the two-segment paths, or any topological classification. In particular, its lemma assuming equal error masses does not prove that a particular rounding procedure produces those masses. The extension below attempts to close the optimization and rounding gaps, but its scripts have not been compiled. The nonnegative identity in Section 2 has a mathematical proof, and its aggregate algebraic identity occurs inside rank_gap_core; exact formal coverage must be read from the declarations.

Each of the 14 historical declarations was audited with #print axioms. Every output listed only propext, Classical.choice, and Quot.sound. There was no sorryAx, proof placeholder, or newly declared axiom. This means no unproved holes were added on top of the usual Lean/Mathlib foundations; it does not mean that the proofs are axiom-free. No successful axiom audit is claimed for the extension.

The checked source has SHA-256

3f29d4e1daad5ed467c6ef2a832a067b03546a2ca35293983f3675e76e70c9fa

During the 2026 09 08 run, the official Lean executable initially failed to locate itself because this host's process-ID namespace did not match its /proc view. A narrowly scoped compatibility shim maps only the current executable's readlink(/proc/<getpid()>/exe) lookup to /proc/self/exe. Lean's source, mathematical kernel, and proof checks were not changed. The reproduction material records the shim source, binary and source hashes, tool versions, failed intermediate attempts, and final successful log. The shim is unnecessary on a standard host.

With the supplied lean-toolchain and lakefile.toml, standard reproduction is

lake update
lake exe cache get
lake env lean MomentIslands.lean

The 33 added declarations: source candidates, NOT COMPILED

Module	Added declarations	Intended coverage	Execution status
`Packing.lean`	6	Integer-offset defect bound by finite induction; absolute offset; exclusion of half-valued coordinates; scaled packing	NOT COMPILED
`BandSharp.lean`	8	The three scalar lower bounds of T2 and their two-coordinate attainment witnesses	NOT COMPILED
`FiniteBand.lean`	7	Actual finite-vector lower bound, binary padding for attainment in arbitrary dimensions, and a half-valued witness at the T4 threshold	NOT COMPILED
`Rounding.lean`	12	Nearest binary rounding, preservation of the number of ones, uniqueness of the binary $L^1$ minimizer, and the sharp integer-total error bound	NOT COMPILED

finite_band_gap explicitly receives a partition, indices attaining its extrema, and the boundary ordering. finite_band_attainment uses the finite index type (Fin p ⊕ Unit) ⊕ (Unit ⊕ Fin q) to provide $p$ ones, two boundary entries, and $q$ zeros, with all box and moment conditions in the statement. Transport through a sorting algorithm on a particular Fin n enumeration is not a separate implemented theorem.

The rounding extension includes the sufficient condition $|S-s|\le\eta$ , $D<1/2-\eta^2$ for count preservation and absence of ties. Its sharp threshold witness assumes $0\le\eta\le1/2$ ; it does not claim an optimal threshold for larger tolerances. T3 and T6–T9, including paths, components, face retractions, and higher homotopy, remain outside Lean coverage.

Mathematical derivation, static source inspection, and rational normalization of 13 polynomial identities were completed for the extension. These do not check Lean elaboration, casts, tactic execution, kernel acceptance, or every inequality inference. The package therefore contains 14 historically checked declarations plus 33 uncompiled candidates, not 47 checked theorems.

The embedded source package includes all five mathematical modules, the import module, version pins, reproduction scripts, historical logs, current blocked-status records, and the algebra check. On a standard machine with the official Lean environment available, the added modules are intended to be checked by:

lake update
lake exe cache get
python3 verify.py

The verifier is designed to record PASS only after a successful build and axiom audit; a missing runtime gives BLOCKED, and a failed build gives FAIL. Its successful end-to-end execution has not yet been demonstrated. Source or runner corrections may still be necessary. This HTML contains the sources and records, not the Lean executable or a complete offline Mathlib installation.

Independent exact-arithmetic checks

Target	Recorded finite coverage	Result
Universal rank bound and nonnegative identity	24,300 sorted grid vectors; 150,723 rank partitions	PASS
Robust formula and paths	75,623 band checks and two-segment paths; 9,240 attaining configurations; 1,880 nearest-rounding checks	PASS
Sum-band edge graphs	75 polytopes; 8,087 independently enumerated edges; 583 threshold checks	PASS
Noninteger rank gaps	317,353 sorted grid vectors; 633,302 squared inequalities; 9,900 attaining configurations	PASS
Noninteger component counts	1,695 weighted-graph levels	PASS
Wide-band edge graphs (T9)	60 rational polytopes; 660 critical-value and midpoint checks	PASS (added in this review)
Hole transitions	Six face-complex stages; boundary matrices over $\mathbb F_2$ , including boundary-squared-zero checks	PASS

The scripts use Python's standard-library integer and rational arithmetic. Different checks reuse some samples; these counts must not be added and reported as independent sample counts. Finite checks do not establish a theorem over a continuous domain. The generality comes from the mathematical proofs and, for the stated formal scope, the Lean proofs.

9. Novelty and attribution

This is a research and exposition note with independently derived formulas, not a certified discovery of new mathematics. Correctness, formal verification, and priority are separate questions. The focused additional audit on 2026 09 09 identified more known special cases and narrowed the remaining search. “Not identified” below means that an identical prior statement was not located in this limited search; it is not positive evidence of novelty.

Two findings materially update the earlier edition. Rosenberg–Jakobsson (2008), Theorem 1(ii), already states the sharp maximum-probability bound used in the rounding comparison [R1]. The earlier edition had principally cited that paper's packing lemma and a later explicit description in Rastegin (2023) [R4]. Also, Gorban (2013), §4.2, Fig.4.5, already exhibits newly born isolated components as the feasible set grows [R3]. Neither the probability bound nor that nonmonotonicity phenomenon is claimed as new here.

Result	Current attribution and remaining scope
Packed maximum squared sum at fixed total	The same extremal formula is known [R1–R2]; not a novelty candidate
Rank form of T1 at the first or last boundary, or with integer total	A short consequence of a known bound or elementary aggregation; reductions are given below
Rank form of T1 at an internal boundary with noninteger total	The same general expression was not identified; priority remains unresolved
Arbitrary-partition square form, nonnegative slack identity, equality classification	Their individual priority is unresolved; identifying some rank special cases does not settle all of these statements
T2, T4, and T5	Explicit consequences of T1 and/or known extremal facts; the same particular formulas were not identified, and no separate general principle is claimed
T3, T6, and T9	Applications of known convex-polytope component theory [R3]; priority of the displayed closed formulas remains unresolved
T7 and T8	An explicit face-retraction argument and a concrete higher-homotopy calculation; a component theorem alone does not establish their full homotopy statements
Matrix corollary	Standard transfer through the spectral theorem; vector component counts do not transfer to the full matrix space
Lean material	Evidence about the specified statements and proof scripts, never evidence of bibliographic priority

A known sharp probability bound

For a probability vector $p$ , put $H=\sum_i p_i^2$ and $M=\max_i p_i$ . Rosenberg–Jakobsson's Theorem 1(ii), p.2028, gives, in particular,

M\ge\frac{1+\sqrt{2H-1}}2,\qquad \frac12<H<1.\tag{17}

At $H=1$ , one coordinate is one and the same expression holds. This is an explicit antecedent from 2008, earlier than the checked 2023 statement; first historical priority is not asserted. The following normalizations and aggregations are our comparison arguments, not claims that the cited paper uses X01's notation or application.

First and last rank boundaries reduce to the known bound

For $s=1$ , T1 simplifies exactly to

g_1^2\ge2Q-S^2.

If $S=0$ , all entries vanish. If $2Q\le S^2$ , the inequality is immediate. Otherwise set $p_i=x_i/S$ , so $H=Q/S^2>1/2$ . Since $p_{(2)}\le1-p_{(1)}$ , (17), with the endpoint handled as above, yields

g_1=S(p_{(1)}-p_{(2)}) \ge S(2p_{(1)}-1) \ge S\sqrt{2H-1}=\sqrt{2Q-S^2}.

This argument needs only nonnegative entries; their upper bound by one is unnecessary in this special case.

For $s=n-1$ , complement and reorder the entries: $y_i=1-x_i$ . Then $D_y=D$ , $S_y=n-S$ , and $g_1(y)=g_{n-1}(x)$ . Moreover,

(S_y-1)^2=(S-(n-1))^2.

The last-rank case therefore reduces to the first-rank case.

Integer totals and the sharp rounding estimate

If $S$ is an integer different from $s$ , then $(S-s)^2\ge1$ and T1 is immediate. If $S=s$ and $D\ge1/2$ , it is also immediate. It remains to consider $S=s$ and $D<1/2$ .

Put $d_i=\min(x_i,1-x_i)$ . For any nearest binary rounding $z$ ,

\sum_i|x_i-z_i|=\sum_i d_i\le2D<1.

Thus the integer $\sum_i z_i-s$ has absolute value less than one and is zero. If a coordinate were $1/2$ , changing its rounding alone would produce another nearest rounding with a different total, contradicting the same conclusion. Rounding is therefore unique, and the coordinates rounded to one are exactly the top $s$ coordinates.

The two error families have equal mass

\rho=\sum_{z_i=0}x_i=\sum_{z_i=1}(1-x_i),\qquad 2\rho<1.

The sum of squares of nonnegative numbers is at most the square of their sum. Applying this separately to both families gives

D=2\rho-\sum_{z_i=0}x_i^2-\sum_{z_i=1}(1-x_i)^2 \ge2\rho(1-\rho).

Since $1-2\rho>0$ , it follows that

1-2\rho\ge\sqrt{1-2D},\qquad \boxed{\|x-z\|_1=2\rho\le1-\sqrt{1-2D}.}\tag{16}

Also, $g_s\ge1-2\rho$ , which proves the integer-total rank inequality. This short calculation does not by itself prove the entire sum-band rounding threshold in T4.

For a further bibliographic correspondence, form $p=(1-\rho,(x_i)_{z_i=0})$ . Its largest coordinate is $1-\rho$ , and

H(p)-(1-D)=\rho^2-\sum_{z_i=1}(1-x_i)^2\ge0.

Hence (17) also yields (16). We do not attribute this aggregation or the same rounding formulation to the 2008 paper. The old Lean module verifies the equal-mass squared-sum argument under an explicit equal-mass hypothesis. The new rounding scripts attempt to establish the rounding procedure's preservation and uniqueness properties, but remain uncompiled.

The remaining rank candidate is narrower

After the reductions above, the nontrivial rank form still requiring priority comparison can be restricted to

\boxed{n\ge4,\quad 2\le s\le n-2,\quad S\notin\mathbb Z, \quad 2D+(S-s)^2<1.}

Outside the last condition the rank inequality gives no positive gap certificate. This narrows the search; it does not prove that the remaining case is new or cannot follow shortly from other known inequalities. The signed arbitrary-partition statement and its slack identity require their own comparison.

T2 follows from T1 and the known packed squared-sum bound. Derivability from these ingredients does not establish that the exact three-branch statement was previously published, but it limits any claim of an independent new principle. For T9, the open novelty question concerns the explicit combination $k=\eta(1-\eta)$ , $c=(1-\eta^2)/2$ , $h=1/4$ , and its binomial component counts, not the general graph reduction or the birth of new components.

What was actually compared, and what remains unread

The audit checked specific results rather than treating similar titles as mathematical equivalence:

Source and inspected part	Comparison with X01
Rosenberg–Jakobsson, Theorem 1(ii), p.2028; Appendix Lemma 3, p.2032 [R1]	Direct antecedents for the probability bound and packing
Ellis, arXiv v2, Theorem 1, pp.4–5; Example 2, p.6 [R2]	Same finite-data maximum-variance and squared-sum formula
Wolkowicz–Styan, Theorems 2.4–2.5, pp.482–484 [R11]	Upper bounds on ranked differences and bounds on the full spectral spread; these are not the specified internal adjacent-gap lower bound
Sharma–Pal, Theorem 5, equation (3.3), p.767 [R12]	Lower bound on top- $k$ sum minus bottom- $k$ sum, a different quantity
Rubensson–Niklasson, §5.1, equations (13)–(16) [R6]	Spectral exclusion from near-idempotency residual norms; no identical integer-offset rank formula identified in that section
Ek–Schutt–Stuckey–Tack, §3, Lemmas 3–5, Algorithm 1 [R7]	Variance lower bounds for propagating an upper variance constraint, with a different direction from X01's high-variance guarantee
Goroncy–Rychlik, §2 and Example 2 [R5]	Deterministic order-statistic inequalities without the same externally fixed box
Gorban, Lemma 2.1, Proposition 2.4, Lemma 3.2; §4.2, Fig.4.5 [R3]	Known vertex/edge and level-set reductions, and a known nonmonotone component-count example

The Gorban numbers in this table follow the PDF; the corresponding older HTML numbers are Lemma 4, Proposition 7, and Lemma 14. His component correspondence alone does not establish the higher-homotopy sequence in T8; its face and cell proofs remain necessary. Matching Betti numbers alone is insufficient for that conclusion.

Selected related portions of The Wonderful Geometry of the Vandermonde map, including Lemma 2.12, and Harper's Morse Matchings on a Hypersimplex were also compared [R13–R14]. Ordered-chamber fibers, labeled vectors, and integer hypersimplices must be distinguished. No full survey of those papers' references is claimed.

Important full-text comparisons remain incomplete: Rubensson–Rudberg–Sałek (2008) [R10], Fahmy–Proschan (1981), Schaus–Régin (2014), Kvålseth (2015), and Kobayashi–Tanaka (2025) [R15]. Their abstracts or references do not establish absence of an equivalent theorem. The search covered English terminology from bounded order statistics, trace bounds, density-matrix purification, SPREAD constraints, and polytope complements. It did not exhaust MathSciNet, zbMATH, books, non-English literature, or every citation chain.

An appropriate publication position is therefore an explicit synthesis, derivation, and verification record with unresolved priority for the remaining formulas. Neither a search miss nor a Lean success certifies novelty.

10. References and source roles

These links identify primary sources. The listed reading scope is deliberately narrower than a claim to have audited every theorem in each paper.

[R1] N. A. Rosenberg and M. Jakobsson, The Relationship Between Homozygosity and the Frequency of the Most Frequent Allele, Genetics 179 (2008), 2027–2036. Theorem 1(ii), p.2028, gives the maximum-probability bound; Appendix Lemma 3, p.2032, gives packing. Both and their relevant proofs were inspected. Author-hosted PDF.
[R2] J. L. Ellis, The maximum variance of a finite dataset, given its mean, minimum, and maximum, arXiv:2508.17525v2 (2025). The seven-page preprint was inspected, particularly Theorem 1, pp.4–5, and Example 2, p.6. This citation refers to the audited arXiv version. arXiv PDF.
[R3] A. N. Gorban, Thermodynamic Tree: The Space of Admissible Paths, SIAM Journal on Applied Dynamical Systems 12 (2013), 246–278. Lemma 2.1, p.11; Proposition 2.4, p.13; Lemma 3.2, pp.18–19; §4.2, Fig.4.5, pp.26–27 of the PDF were compared. Source for vertex access, graph and level-set reductions, and a prior example of nonmonotone component counts. Author's arXiv PDF. The HTML version instead numbers those first three statements Lemma 4, Proposition 7, and Lemma 14.
[R4] A. E. Rastegin, Uncertainty relations in terms of generalized entropies derived from information diagrams (2023), Theorem 1, equations (30)–(31). A later explicit description of the high-collision-probability bound, retained for comparison; [R1] provides an older explicit antecedent. arXiv full text.
[R5] A. Goroncy and T. Rychlik, How deviant can you be? The complete solution, Mathematical Inequalities & Applications 9 (2006), 633–647. §2, p.637; §3, Example 2, pp.642–643 inspected. Its domain differs from the externally fixed-box setting. Publisher PDF.
[R6] E. H. Rubensson and A. M. N. Niklasson, arXiv:1302.7292 (2013 preprint), §5.1, equations (13)–(16). Comparison for near-idempotency residuals and eigenvalue estimation. The inspected bounds include $\|A\|_F^2/\operatorname{Tr}A\le\|A\|_2$ for nonzero denominator and exclusion of a central open interval using the residual norm. arXiv PDF.
[R7] A. Ek, A. Schutt, P. J. Stuckey, and G. Tack, Explaining Propagation for Gini and Spread with Variable Mean, CP 2022, LIPIcs 235, 21:1–21:16. §3, Lemmas 3–5 and Algorithm 1, pp.21:4–21:7 inspected beyond the abstract. Official proceedings PDF.
[R8] Parameterless stopping criteria for recursive density matrix expansions, arXiv:1507.02087v3. Introduction, Theorem 1, and the HOMO/LUMO discussion in §6 were inspected as a related source on convergence of idempotency errors. arXiv full text.
[R9] Lean 4.19.0 and Mathlib v4.19.0. Official version records for the proof environment: Lean release and Mathlib tag. The acquired Mathlib source matches commit c44e0c8ee63ca166450922a373c7409c5d26b00b; this is not evidence of a new Lean compilation.
[R10] E. H. Rubensson, E. Rudberg, and P. Sałek, Density matrix purification with rigorous error control, Journal of Chemical Physics 128, 074106 (2008). Bibliography and abstract only; full-text equation comparison remains outstanding. DOI and publisher record.
[R11] H. Wolkowicz and G. P. H. Styan, Bounds for eigenvalues using traces, Linear Algebra and its Applications 29 (1980), 471–506. §2, especially Theorem 2.4, (2.40), p.482, and Theorem 2.5, pp.483–484, inspected. Author-hosted PDF.
[R12] R. Sharma and M. Pal, Note on bounds for eigenvalues using traces, Operators and Matrices 16 (2022), 759–773. Theorem 5, (3.3), p.767, inspected. Publisher PDF.
[R13] The Wonderful Geometry of the Vandermonde map. Selected portions of §2.1, including Lemma 2.12, inspected for connectedness of ordered-chamber power-sum fibers. Publisher full text.
[R14] J. T. Harper, Morse Matchings on a Hypersimplex, arXiv:1211.6483. The integer-hypersimplex face description and the statement and explanation of Theorem 6.11 were compared; the entire matching proof and associated thesis were not audited. arXiv full text.
[R15] Further full-text comparisons remain incomplete: Fahmy–Proschan (1981), Bounds on Differences of Order Statistics; Schaus–Régin (2014), Bound-consistent spread constraint; Kvålseth (2015), Bounds on Sample Variation Measures Based on Majorization; Kobayashi–Tanaka (2025), Unified relationship between mean, variance, and an arbitrary number of quantiles. Only available abstracts, bibliographic records, or references through other papers were checked; the absence of the present formulas is not established.

11. Remaining proof and literature work

The immediate review task is to check that each theorem's assumptions, threshold endpoints, and stated formal coverage agree. The Fable review request provides focused questions, while the source package makes the proof scripts and records available from this single HTML file. This edition has not yet received that further review.

For formal verification, the next concrete step is to run the existing 33 extension scripts under the pinned Lean and Mathlib versions, correct any elaboration or proof failures, and retain a fresh build and axiom-audit log. Only then can their status change from NOT COMPILED. The two-segment construction and topological results T3 and T6–T9 still require separate formalization.

T9 classifies path components for every admissible $n,s$ when $1/2<\eta<1$ . Mathematical extensions include higher homotopy types in this regime and $\eta\ge1$ , where further integer-sum vertices enter the band. Bibliographic work should concentrate on the remaining internal noninteger-rank case and the unread sources listed above.

This document records exact formulas, ordinary mathematical proofs, known antecedents, historical machine checks, and current uncompiled work. It does not register established academic novelty, alter the previously published E01/E02 ledger, or include the separate triangle-audit candidate X04. Blog publication remains a later decision by Yokota.

順位を守る、平均と分散。What momentskeep apart.