# 検証プログラムは何をしているか

このリポジトリの検証は、難しい最適化ではありません。各 JSON に入っている点集合が、本当に `N`-avoiding かを全三点で総当たり確認しています。

## 生成プログラムと検証プログラムは別

ここは重要です。witness table には二つの段階があります。

```text
生成、探索:
  よさそうな点集合 S を見つける

検証:
  その S が本当に N-avoiding かを厳密に確認する
```

`N=1..27` は、BorisAlexeev が Erdős Problems #352 のコメント欄に投稿した witness を同じ JSON 形式に直して、このリポジトリで再検証したものです。該当コメントは 2025-12-28 03:17 の投稿で、`N`, `f(N)`, witness という形式で `N=27` までのデータを載せています。たとえば `N=5` は、点の順番を並べ替えると普通の `3 x 3` 格子ブロックです。

`N=28..40` は、次のような探索で候補を作りました。

```text
1. radial-prefix disk search
   大きめの候補ボックスを作り、中心を少しずつ変えながら、
   中心に近い格子点から順に追加する。
   初めて禁止三角形が出たところで止める。

2. local add-only repair
   今ある witness の周辺だけを見て、
   追加しても条件を壊さない点を貪欲に足す。

3. fixed-box hitting-set search
   固定した有限ボックス内で、禁止三角形を hyperedge として作り、
   より大きな independent set があるか探索する。
```

公開用 repo に入っている

```bash
python3 scripts/radial_prefix_search.py 5
```

は、このうち一番素朴な radial-prefix 探索です。`N=5` では `3 x 3` の9点を再現します。ただし、これは軽い再現用の構成補助であって、表のすべての最良行を作る完全な optimizer ではありません。

探索プログラムは heuristic でも構いません。なぜなら、下界主張に必要なのは「どう探したか」ではなく、最後に得られた `S` が本当に条件を満たすことだからです。ただし、読者にとっては生成方法も重要なので、検証とは分けて説明する必要があります。

## 検証プログラムが見るもの

点集合を `S` とします。条件は次です。

```text
S の任意の三点 p,q,r について
|area(p,q,r) - N| > diam(p,q,r)
```

ここで「三点」には重複も含めます。つまり `p,p,q` や `p,p,p` も確認対象です。

大事なのは、この verifier が調べるのは「JSON に書かれている一つの集合 `S`」だけだということです。すべての可能な格子点集合を探索しているわけではありません。

たとえば JSON に 20 点が書かれているなら、verifier が見るのは「その 20 点の中から選ぶ三点」だけです。重複ありなので、確認する三点組の数は

```text
20*21*22/6 = 1540
```

です。これは無限個ある「ありうる20点集合」を全部見る、という意味ではありません。

それで十分なのは、witness table が下界の主張だからです。サイズ `m` の集合 `S` が一つでも条件を満たせば、

```text
f(N) >= m
```

が分かります。これは「少なくとも m 点は置ける」という意味です。

逆に、

```text
f(N) = m
```

と言うには、`m+1` 点以上の集合が存在しないことを別に証明する必要があります。その場合は、`(0,0)` を含まない集合、平行移動した集合、形が全然違う集合も全部排除しなければいけません。これは witness verifier ではなく、上界 certificate の仕事です。

なお、下界 witness は `(0,0)` を含む必要はありません。格子上のどこかに条件を満たす集合が一つあればよいです。座標は見やすさのために平行移動されていることがあります。

## 浮動小数を使わない形

面積や距離をそのまま小数で比べると丸め誤差が出ます。そこで verifier は整数だけで判定します。

```text
A2 = 三角形の面積の 2 倍
D2 = 三角形の直径の 2 乗
gap = (A2 - 2N)^2 - 4D2
```

このとき

```text
|area - N| > diameter
```

は、正確に

```text
gap > 0
```

と同じです。だからプログラムは全三点について `gap` を計算し、ひとつでも `gap <= 0` があれば失敗にします。

なぜ同じかを一行ずつ書くと、面積を `A`、直径を `d` として、

```text
|A - N| > d
|2A - 2N| > 2d
|A2 - 2N| > 2d
(A2 - 2N)^2 > 4d^2
(A2 - 2N)^2 > 4D2
gap > 0
```

です。途中で二乗してよいのは、両辺がどちらも 0 以上だからです。

## 出力の読み方

```bash
python3 scripts/verify_witnesses.py
```

出力の `min_gap` は、その witness の全三点の中で一番小さかった `gap` です。

`min_gap` が正なら、その JSON の点集合は検証済みです。たとえば `N=28` の `min_gap=44` は、いちばん危ない三点でもまだ 44 だけ整数判定上の余裕がある、という意味です。

## なぜ N=1..27 も入れるか

はい、公開時には「1〜27 は？」と聞かれやすいです。そこで `data/witnesses/` には BorisAlexeev の既存フォーラム witness も同じ形式で入れています。各 JSON の `source` には、BorisAlexeev のコメント由来であることを明記しています。

このリポジトリで新しく見せたい部分は主に `N=28..40` ですが、検証プログラムは `N=1..40` の全 witness を同じ方法で確認します。