http://hadwiger.html.xdomain.jp/
グラフ理論の本を読んでいたら、「Hajós の構成」なるものを見つけました。
https://sites.math.washington.edu/~billey/classes/562.winter.2018/articles/GraphTheory.pdf
「haj」で検索すると出てきます。
Wikipedia にもあります。
https://en.wikipedia.org/wiki/Haj%C3%B3s_construction
染色数が k 以上のグラフをすべて、再帰的に構成するものですが、
hadwiger氏 の論調に近いものがあると思います。
ブール代数の部分（「4. 最小反例の性質」の命題15,16の証明）に関しては、定理証明をおこなった。
残り以下三点をクリアにすれば、氏の証明は正しいと言えそうだ。
- 頂点の集合A,B,C の定義
- 定理証明の前提条件として使った以下九命題が正しいこと
- P15_1 : Kn && R ==> (Σ(k && Pin) ==> g).
- P15_2 : Kn && R ==> (Σ(Qex) ==> g).
- P15_4 : Kn && R ==> (g ==> Σ(k && Kn && R)).
- P15_5 : Kn && R ==> (Σ(k && Kn && R) ==> (Σ(k && Pin) || Σ(Qex))).
- P16_2 : gKnRin ==> g && Pin.
- P16_3 : g && Pin ==> Σ(k && Pin).
- P16_5 : gKnRex ==> Qex.
- In_ex_eq : gKnRin || gKnRex = g && (Kn && R).
- Qex_sigma : Qex ==> Σ(Qex).
- 「5. 証明」の論証
- 「3. Hadwiger予想と同値な命題」まで
Σ(Kn∧R) ⇔ g∧g1∧g2∧…∧ΣR
「もし、g1が存在するとすれば、g1 の論理否定のついた辺を縮約すれば、より小さい n-1色で彩色不能なグラフになる」
がなぜ言えるか分からない => 少し分かってきた - 集合H を使うもの
「具体例での説明」等4色目が必要な点を取り除くその周りの領域H を3色に固定他を縮約（うまい辺を選んで）取り除いた点を元に戻すそうするとやはり 3-彩色不可能
が言いたい事だと思う
- さらに 頂点の集合A,B,C を使うもの
ブール代数による証明
また、「真理値表を使うやり方」と「ブール代数を使うやり方」
という分け方もありそうだ。
これはあくまで仮定の話、としてそう
これは言えそう。
領域H を2色以下で着色しているから
維持しない縮約の全てを、条件Y で潰さないといけない
→着色の全てが、縮約の全てだから？
うーん。言えるのかどうか...
頂点1 を β で着色するパターンも見なくてはいけないのでは、と思った
- 着色の全てが縮約の全て => 彩色不可能性を維持する縮約と、維持しない縮約に分かれる
- 集合H を2色で着色したら、頂点0に3色目を充てられる
=> 条件Y の着色(縮約)は、3彩色不可能性を維持しない - 条件Y が維持しない縮約(着色)ならば、残りの行は彩色不可能性を維持する縮約(着色)である
Hadwiger予想とは、「彩色に n色必要なグラフは、n点の完全グラフに縮約可能である」という予想です。
Hadwiger予想の n = 3 の場合は、閉路（サイクル）を含まないグラフは2色以内で彩色できるということで、自明に成立しています。そこで n ≧ 4 とします。
グラフは n-1色で彩色不能であるとします。
Σ(Kn∧R) をグラフに含まれる辺の論理式として乗法標準形に展開した各項で、ΣR に含まれないものを、g, g1, g2, … とします。
g はグラフの辺すべての（論理否定のつかない）論理和とします。定義より g, g1, g2, … は ΣR に吸収されません。次の論理式は恒真式です。
Σ(Kn∧R) ⇔ g∧g1∧g2∧…∧ΣR
もし、g1が存在するとすれば、g1 の論理否定のついた辺を縮約すれば、より小さい n-1色で彩色不能なグラフになります。
つまり、いくつかの辺を縮約してより小さい n-1色で彩色不能のグラフにする方法がもしあれば、
ブール代数の機械的な計算で乗法的標準形に展開することによって見つけることができます。
膨大な計算となり現実的な方法ではありませんが、グラフの構造を分析することなしに（理論的には）できるのは、大きな長所です。
Σ(Kn) ⇔ g かなあ？
=> 「(¬g) → ΣR は恒真式」との事（命題3）。
定義 最小反例から、頂点0 と頂点0 に接続している辺を取り除いたグラフを G' とします。
定義 グラフG' に対して着色の条件X, Y を定めます。
条件X: すべての頂点を n-1色以内で着色します。
条件Y: すべての頂点を n-1色以内で着色しますが、集合H の頂点は n-2色以内で着色します。（彩色はできない）
条件X の着色に対応する論理式は Kn であり、条件Y の着色に対応する論理式は Kn-1(H)∧Kn∧R です。
定義 Kn-1(H) を k と表記します。k∧Kn∧R は、Kn-1(H)∧Kn∧R の意味です。
定義 グラフG' の辺すべての論理和を g とします（g の各項は論理否定がついていません）。
tautology (Kn∧R) → { Σ(k∧Kn∧R) ⇔ g } わかった❗❗
ーーーーー
これは自明らしい tautology (Kn∧R) → Σ(Kn∧R)
そして
Σ(k∧Kn∧R) ⇔ g∧Σ(Kn∧R) （命題12 の後半、これ厳密にチェックしたい※※）
から
{ Σ(k∧Kn∧R) ⇔ g } ← Σ(Kn∧R)
が言えるらしい a∧b ⇔ c と a → {b ⇔ c}
定義 グラフG' において、頂点v に隣接していない頂点の集合を A とします。
頂点v + 頂点vに隣接している頂点の集合を B とします。
集合A とB の共通部分を C とします。（集合C は、グラフG' において頂点vに隣接している頂点の集合で、n-1個以上の頂点があります。）
C は空集合になるのでは？
定義 Pin を P の 集合C の頂点が n-2色以内で着色された部分とします。Qex を Q の 集合C の頂点が n-1色を使って着色された部分とします。
命題16よりグラフG' で次の論理式が成立しています。
tautology (Kn∧R) → { [Σ(k∧Pin) ∨ Qex] ⇔ g }
仮定により条件X（グラフ全体を n-1 色以内で着色します） でグラフG' は彩色可能です。その着色を x とします。
これまでと同じく、頂点v は集合H に含まれていない頂点です。
頂点v の隣接頂点（集合C の頂点です）は、着色x で n-2色以内で着色されているはずです。Qex は集合C の頂点に n-1色を使った部分なので、着色x は Qex を偽にします。
着色x は (Kn∧R) を真、[Σ(k∧Pin) ∨ Qex] と g を偽にします。
着色x での v の色のみを変更して、グラフG' での v の隣接頂点のどれかと同じ色にします。これを着色x' とします。
着色x' は集合C の頂点は n-2色以内の着色なので、やはり Qex を偽にします。
着色x' は (Kn∧R) を真、[Σ(k∧Pin) ∨ Qex] を偽にしますが、g を真にします（vの色を隣接の一つと同じにしたから、繋ぐ辺が1になる）。
これは矛盾です。反例は存在しません。■
どんなグラフでも、着色x' は [Σ(k∧Pin) ∨ Qex] を偽にするが、g を真にするのだと思う。
最小反例だけ、 [Σ(k∧Pin) ∨ Qex] ⇔ g が成り立つのだと思う。これが証明のキモ
Σ(k∧Pin) は真にはならないのか？ ← Pin は真だけど、 k は偽
以上より、Hadwiger予想より少し詳しい次の定理が成立していることが分かります。
定理 G を彩色するのに n色必要な完全ではないグラフとします。
頂点v とそれに接続している辺を取り去ったグラフでは n-1色で彩色できるものとします。
この場合、v に接続していない辺を縮約する（あるいは頂点、辺を取り除く）ことを繰り返して、v とあわせて
n点の完全グラフをつくることができます。 ※
（これを以下の具体例でやってる？）
これは、頂点0 と 頂点6 を異なる色で着色すれば、辺e0,6 を付け足すことと同じで、頂点0, 1, 2, 6 が4頂点の完全グラフになります。
もし 頂点0 と 頂点6 を同じ色で着色するなら、
頂点0 と 頂点6 を同じ頂点とみなすことと同じで、この頂点と 3, 4, 5 が4点の完全グラフになり、（無い辺の縮約）
→辺64、63を縮約すれば良い※
臨界グラフならば、一つの辺を縮約すれば完全グラフになり、
臨界でなければ、複数の辺を同時に縮約しないと完全グラフにならない？
頂点0 と 頂点0 の辺を取り除いたグラフを、
条件X：全体を 3色以内で着色する。
条件Y：全体を 3色以内で着色するが、集合H の頂点は 2色以内とする。
104, 116 もそうだね
そうすると次の恒真式が成立します。※※
tautology Σ(k∧K4∧R) ⇔ g∧g1∧g2∧g3∧Σ(K4∧R)
完全グラフでないとき、どの辺にも論理否定のつかない g （3彩色できてる）のような最大項があれば、
g1, g2, g3 のようなどれかの辺に論理否定のついた最大項が生じることを証明すれば、
Hadwiger予想を証明したことになります。←これはいいや
ピーターセングラフは 3彩色 できるよ
