🔢 mathematics

Exact Zarankiewicz Values On Two Finite Frontier Slices

本論文は、軌道証明書、削除補題、および厳密な算術検証を利用して、Z(12,n,3,3)=6n (18≤n≤22) や Z(13,22,3,3)=137 といった値を確定させる、特定の有限スライスおよびその近傍のフロンティアにおけるザランケヴィッチ数の正確な値を確立する、結合された証明書に基づくコンピュータ支援証明を提示する。

原著者： Koyar Afrasyab

公開日 2026-08-11

📖 1 分で読めます🧠 じっくり読む

CC BY 4.0

原著者： Koyar Afrasyab

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

あなたは、最も効率的な道路網を構築しようとしている都市計画家だと想像してください。あなたには、「ハブ」と呼ばれる一組の地点と、「目的地」と呼ばれるもう一組の地点があります。あなたの目標は、交通の流れを維持するために、それらの間にできるだけ多くの道路（接続）を描くことです。しかし、厳格なゾーニング法が存在します。あなたは、特定の、厄介な交差点パターンを構築することを禁じられています。数学的に言えば、この禁止されたパターンは「完全二部グラフ」、あるいは単に「3x3の交差点」です。つまり、3つのハブがすべて同じ3つの目的地に接続されているような状況を作ると、ルール違反となります。

このパズルは「ザラニエヴィッツ問題」として知られています。これは、組み合わせ論（構成や配置、組織化を専門とする数学の一分野）における古典的な難問です。数学者たちは、巨大で理論的な都市に対してはこの問題を解く方法を見出していますが、今回の課題は「中規模」の町に関するものです。これらの特定のサイズについては、可能なロードマップの数が膨大であるため、手作業ですべてをチェックすることはできませんが、同時に、無限の都市に適用できる単純な公式で解けるほど単純でもありません。これは「ゴールドロック（適度な）ゾーン」の難易度です。紙と鉛筆による証明には大きすぎ、かといって漸近的なショートカットが通用するほど小さくもない、絶妙な難しさなのです。

そこに、特に手強い中規模サイズのパズルを解き明かした研究者、コヤル・アフラシアブが登場します。この問題を、グリッド上で「3x3」の禁止された交通渋滞を作ることなく、描ける道路の絶対的な最大数を求めることだと考えてみてください。アフラシアブは単に推測したのではなく、答えを突き止めるためのデジタル探偵機関を構築しました。この論文は、2つの特定の「スライス」、すなわち、行数が12のグリッドと行数が13のグリッド、および様々な列数の組み合わせに焦点を当てています。

主な発見は、これらのグリッドに対する正確な「速度制限」のリストです。行数が12で、列数が18から22までの範囲にあるグリッドの場合、ルールを破らずに引ける道路（エッジ）の最大数は、正確に $6n$ （ $n$ は列数）となります。例えば、12x18のグリッドには正確に108本の道路を引くことができ、12x22のグリッドには132本の道路を引くことができます。論文では、これらのグリッドにあと一本でも道路を追加しようとすれば、必然的に禁止された交通渋滞が発生することを示すことで、これを証明しています。

この物語の中で最も劇的な部分は、13x22のグリッドに関するものです。以前の予想では、限界値は140本に達する可能性さえありました。アフラシアブのコンピュータを用いた証明は、あらゆる不可能な配置を排除していく「ふるい」のように機能しました。彼らは、誰かがルールを破らずに138本の道路を引けるという仮定からスタートしました。各地点に何本の道路が接続されているかという「プロファイル」をチェックするという巧妙な消去法を用いることで、138本は不可能であることを証明しました。彼らは、真の天井（上限）が見つかるまで絞り込みを行い、最終的に137本が真の限界であることを突き止めました。彼らは、137本の道路が成立する具体的な検証済みマップさえも提示しており、その数に到達できること、そしてそれ以上には行けないことを証明しています。

また、この論文は、13x18、14x17、15x18といった隣接するグリッドのマップも確定させています。一つの非常にトリッキーなケースとして、16x17のグリッドについては、132本の道路を確実に構築できることを証明しつつも、上限は依然として132から133の間の狭い範囲にあることを確認しています。

この研究を特別なものにしているのは、その「手法」です。著者は、単に「解が見つかりませんでした」と表示するだけのブラックボックス型のコンピュータプログラムを実行したわけではありません。代わりに、彼らは「証明書ベース」の証明を作成しました。これは、探偵がパン屑の跡を残していく様子を想像してください。あり得ないシナリオを一つ排除するたびに、誰でも電卓を使ってエラーを確認できる数学的な「領収書（証明書）」を残したのです。論文には、単一のコマンドを実行するだけで、数百万もの領収書を再検証し、ミスがなかったことを確認できるデジタルパッケージが含まれています。これは、単なる「おそらく」という答えを「間違いなく」という事実へと変える、厳格で透明性が高く、完全に再現可能な、数学界への勝利なのです。

技術要約：2つの有限フロンティア・スライスにおける正確なザラニェヴィッチ値

問題設定
本論文は、サイズ $m$ と $n$ の二部グラフにおいて、 $K_{s,t}$ を含まない最大エッジ数 $Z(m, n, s, t)$ を求めるザラニェヴィッチ問題を扱う。著者は、中程度の有限パラメータにおける $s=t=3$ （ $K_{3,3}$ を回避するケース）のケースに焦点を当てている。漸近理論は高度に発達しているが、特定の有限次元における正確な値は、深刻な対称性と証明の認証コストの高さから、依然として困難な課題である。本論文は、未解決または部分的に解決されている既知の領域である「有限フロンティア」を対象としている。これには、ストリップ $Z(12, n, 3, 3)$ （ $18 \le n \le 22$ ）、特定のケース $Z(13, 22, 3, 3)$ 、および $13 \times 18$ と $16 \times 17$ の周辺にある一連の値が含まれる。

手法
証明はコンピュータ支援によるものであるが、厳密に**証明書ベース（certificate-based）**であり、単に「実行不能」を返す混合整数線形計画法（MILP）ソルバーや、明示的な証拠（witness）なしに動作するSATソルバーに依存する手法とは区別される。検証は、正確な整数および有理数演算（Pythonの Fraction および標準ライブラリを使用）に依拠しており、浮動小数点最適化は初期の証明書発見のためにのみ使用されている。

手法は多層的な削減戦略を採用している：

グローバル緩和と次数プロファイル： $13 \times 22$ のケースでは、138エッジを持つ仮定の行列を想定する。列次数に関連するペナルティ関数 $p(d) = \binom{d}{3} - 15d + 70$ を分析することで、探索空間をすべての可能な行列から、わずか83個の異なる次数プロファイル（列次数のヒストグラム）へと削減する。
ファルカスの証明書（Farkas Certificates）： これら83個のプロファイルのうち77個について、著者は正確な有理数ファルカスの証明書を構築する。これらの証明書は、 $K_{3,3}$ フリーの条件（具体的には、すべての行の3つ組が最大2つの列に現れること）によって課される線形制約を、そのプロファイルに対して非負整数解が存在しないことを示すことで、実行不能性を証明する。
標識行（Marked-Row）とリーヴ（Leave）の列挙： 残りの6つのプロファイルは、より粒度の高い手法によって除外される。著者は「標識行」を固定してそれを削除し、残りの12点上の「リーヴ多重グラフ」を分析する。これには以下が含まれる：
- 合同式による議論： 行の不足分に関するモジュロ演算を用いて、特定の構成を排除する（例：プロファイル 6187391）。
- グラム行列の制約： 残差ブロックのインシデンス行列のランクおよび行列式条件をチェックする。
- 正確な列挙： 残差ブロック設計を網羅的に列挙し、残りの因子分解システムに対して整数スケールのファルカス証明書を適用する。
削除補題と証拠（Witnesses）： $12 \times n$ ストリップおよびフロンティアの閉鎖については、「削除補題」（ $Z(m, n)$ と $Z(m, n-1)$ の関係）を、明示的な構成的証拠（下界を達成する行列）と組み合わせて使用し、正確な等式を確立する。

主な貢献と結果
本論文は、以下の正確な値および境界に対する、結合された証明書ベースの証明を提供する：

$12 \times n$ ストリップ： $Z(12, n, 3, 3) = 6n$ （ $18 \le n \le 22$ ）を証明する。これは、 $Z(12, 18, 3, 3) = 108$ に対する正確な証明書と、それに続く $n=19, 20, 21, 22$ に対する明示的な証拠に支えられた削除議論によって確立される。
$13 \times 22$ のケース： $Z(13, 22, 3, 3) = 137$ を証明する。138のエッジによる上界は、上述の網羅的なプロファイル分析によって排除される。137の下界は、明示的な構成（137個の1を含む $13 \times 22$ 二進行列であり、 $K_{3,3}$ を含まない）によって確認される。
フロンティアの閉鎖： 隣接する4つのセルに対して正確な値を確立する：
- $Z(13, 18, 3, 3) = 116$
- $Z(14, 17, 3, 3) = 118$
- $Z(14, 18, 3, 3) = 124$
- $Z(15, 17, 3, 3) = 126$
- $Z(15, 18, 3, 3) = 132$
$16 \times 17$ 区間： 区間 $132 \le Z(16, 17, 3, 3) \le 133$ を報告する。下界は新しい132エッジの証拠によって支持され、上界の133は先行文献（Collinsら）から引用されている。本論文では、この特定のセルに対する正確な値は本研究内では決定されていないことを明記している。

意義と主張
著者は、本研究がこれらの特定のザラニェヴィッチ値に対して、完全で再現可能、かつ証明書ベースの証明を提供するものであると主張している。その意義は、発見（ここで浮動小数点ヒューリスティックが使用される可能性がある）と検証（正確な演算のみを使用する）の厳格な分離にある。

再現性： 本論文には、すべての570万件の正確な非負チェック（次数プロファイルの再生成、ファルカス証明書の再生、および残差ブロック設計の網羅的列挙を含む）を再生する「ワンコマンド検証ゲート」が含まれている。
謙虚さ： 著者は、これらの結果が「独立した再現と査読を待つ、新しいコンピュータ支援による証明」とみなされるべきであると明示している。本論文は、一般的なザラニェヴィッチ問題を解決したり、普遍的なアルゴリズムを提供したりすることを目的としたものではなく、有限の極値問題における役割分担（粗いグローバル緩和を用いてほとんどのケースを排除し、計算負荷の高い正確な列挙を少数の「困難な」残余プロファイルのために予約する）を示すものである。
先行研究： 著者は、 $13 \times 22$ における137エッジの構成は以前に報告されているものの、正確な上界は新しい貢献であることを述べている。同様に、 $12 \times n$ ストリップの特定の値（ $n=18$ から $21$）およびフロンティア閉鎖の値は、論文作成日（2026年8月）時点の既存の索引付き文献には見られない新しい正確な結果として報告されている。

本論文は、未検証のDRATクレーム、SATタイムアウト、または浮動小数点ソルバーのステータスが定理の前提として使用されていないことを強調して締めくくられており、数学的主張がすべて明示的な有限データと正確な演算に基づいていることを保証している。

関連論文