QE による検証

Mathematica の QE のデフォルトの議論領域は

Reduce[Exists[x, a*x^2 == 1]]

に対する出力

f:id:ehito:20190320172321p:plain

からも判るように複素数体であり，前回公開した Mathematica での実装の目的の 1 つは，この QE による結果の検証でした．

Mathematica で前回の各関数の定義コードを実行した後，例えば，

(p1=PL[[1]])@x

f:id:ehito:20190320165602p:plain

を

mp[p1];nGG[];cs[];RR[];InputForm@DP

のように処理すると

f:id:ehito:20190320165305p:plain

といった出力が得られます．

このとき，A についての 2 つの条件
(1) A が分解体の primitive element の定義多項式 p2 の零となる
(2) A の多項式で表された根全体 r1 /. pe -> A が入力の多項式 p1 の根全体となる
が等価であるという式

ForAll[A, 
 Equivalent[p2@A == 0, 
  ForAll[x, Times @@ (x - r1 /. pe -> A) == p1@x]]]

すなわち

f:id:ehito:20190320165152p:plain

を複素数体上で

Reduce[%,Complexes]

のように QE すると

f:id:ehito:20190320170301p:plain

と答えてくれます．

また，A についての 2 つの条件
(1) A が分解体の primitive element の定義多項式 p2 の零となる
(3) 出力 DP に属する全ての多項式の共通の零点 (w,e[1]) が存在する
が等価であるという式

ForAll[A, 
 Equivalent[p2@A == 0, 
  Exists[Evaluate@Rest@vs, And @@ (# == 0 & /@ DP)]]]

すなわち

f:id:ehito:20190320170755p:plain

を複素数体上で

Reduce[%,Complexes]

のように QE すると

f:id:ehito:20190320170830p:plain

と答えてくれます．