コメントありがとうございます。
返事遅くなりすみません。

ご指摘の点、確かに証明が甘そうですね。
証明を厳密化してみます。

肝というのは、
「隣の入力のペア毎に1つ以上のAND素子が必要」
「NTDに含まれる隣の入力のペアの濃度は、入力長に対して多項式規模に収まらない」
−＞「NTDを計算するNNF回路族の(AND)素子数は多項式規模に収まらない」
の部分です。

上記は、DTMをエミュレートしているからと言って自明ではありません。

この部分が本証明の肝となります。

定理３より、
NNF回路族には（隣の入力のペアの）差分部分のどちらか片方を含む時のみに1になるAND素子が存在。
−＞隣の入力のペア毎に1つ以上のAND素子が必要。（さもなければ間の入力を区別できない）

定理１２（及び定理５、８、９、１１）より、
NTDに含まれる隣の入力のペアの濃度は、入力長に対して多項式規模に収まらない。

よって、NTDを計算するNNF回路族の素子数は多項式規模に収まりません。

そのようなxは存在しますが、多項式時間還元にはなりません。

多項式時間還元でx(NTD) ∈ Pとなるxが存在する
-->（x(NTD) ∈ Pより）入力長の多項式規模のNNF回路族でx(NTD)が計算できる。
-->（xが多項式時間還元となることより）入力長の多項式規模のNNF回路族でNTDが計算できる。
となり、定理１３と矛盾します。

コメントありがとうございます。

> NTD を導入すると P ⊂ NTD ⊆ PH となる，だから P != PH ってことですか？

いいえ。問題のクラスで表すと
PH ∋ NTD ∉ P
--> P != PH
ですね。

定義１(とSipserの証明)より
P ⊂ 入力長の多項式規模のNNF回路族で計算できる問題のクラス

定理１３より
NTD ∉ 入力長の多項式規模のNNF回路族で計算できる問題のクラス

定理１０より
NTD ∈ PH

から、定理１４にて
・定義１、定理１３より
　NTD ∉ P
・定理１０より
　NTD ∈ PH
よって
PH ∋ NTD ∉ P
--> P != PH
を導いています。

以前にスラドに投稿したときに色々と意見をもらえたので、
今回も投稿してみました。

Paperはまとめていますので、今回コメント頂いたらその内容を
反映してECCC辺りに投稿しようかと思います。
＃大きなギャップが無ければですが……

ご指摘ありがとうございます。
ここはちょっと修正＆補足が必要そうです。

まず「NTDの濃度は多項式規模に収まらない」の部分ですが、正確には
「NTDにある隣の入力のペアの濃度は多項式規模に収まらない」
ですね。定理１２もそれに合わせて
定理１２
NTDに含まれる隣の入力のペアの濃度は、入力長に対して多項式規模に収まらない。
に修正した方が良さそうですね……

また、「よって」の部分ですが、
定理３：
NNF回路には、入力が少なくとも（対応する）差分部分のどちらか片方を
含む時のみに1になるAND素子が存在する。
−＞NTDのそれぞれの隣の入力毎に、（受理すべき隣の入力の差分部分全体と
　　拒否すべき間の入力を判別するために）入力がその差分部分全体を含むかどうかを
　　判定する独自のAND素子を持つ必要がある。

を前提とする「よって」になります。
定理３自体はP≠NPを仮定していませんので、この「よって」もP≠NPを
仮定していません。

後で説明の補強を考えることにします。
＃単純に「定理３より」のような説明を追加する感じですかね。

AIとか、機械にやらせるときの課題は計算結果の評価方法をどうするかですね。

最近ですとビッグデータでゴリ押しするケースも多いですが、証明なんかですと
多数のゴミの山の中から欲しい結果を探し出すという苦行が結局残りそうな
気がします。
＃ネットで欲しい文献を探すイメージ……

NP問題も（膨大な時間を使うことができれば）コンピューターで計算することは
可能ですので、自動定理証明のシステムが存在してもP＝NPにはならないですね。

また、量子コンピューターは（NP問題を効率的に計算できる）非決定性チューリング
マシンを比較的効率的にエミュレートすることができますので、NP問題が効率的に
計算できるようになったからといってP=NPになるわけではないです。
＃量子コンピューターでも、NP完全問題は効率的に計算できないみたいですけど

自動定理証明は色々と研究ありますが、一般的には難しいようですね。
特に、記法すら確立していないような新しい手法なんかは全く歯が立たないかと思います。（この証明は違うけど）

まあ、確実な定理検証システムができてしまうと、数学の証明手法が大きく変わりそうですね。
量子コンピューターで（網羅的に）全ての定理を並列に検証して正しい定理を探り当てる、データマイニング的な手法が数学者の仕事になるかも。