定理 (20060819) の証明の核心部分．

証明そのものは 論文をご覧下さい． ここは手持ちの証明の強引さの笑い話のページです．

領域 D を帯状領域に変換する対応 y=x²z を考え， (X,Y)=grad W に対して G(x,z) = X(x,x²z)/x および F(x,z) = z X²(x,x²z)/Y(x,x²z) とおく． D における grad W の固定点と D'={(x,z) = x>0, 0≦z≦1} における F(x,z)=G(x,z)=1 の解が1:1に対応することはすぐ分かる．

(x,z)→(G(x,z),F(x,z))のヤコビアンを J_GF= G_x F_z - F_x G_z とおく． 陰関数定理から J_GF が 0 にならない（定符号である）ことが， 少なくとも局所的には (x,z)→(G(x,z),F(x,z)) が1:1であること （したがって，特に，固定点の唯一性）を保証する． 定理に設定したいくつかの条件のおかげで， さらにそのとき大局的にも x が 0 近くの定性的振る舞いが伝搬するので， 大局的な固定点の唯一性に至る．

問題の核心は D'における J_GF>0 の証明である． 実際には，D'全体で証明できなくても， たとえば F=1の近傍に限って証明すれば十分なので，それを目指す．

Rem₀=e(x,z) =(1-z)x² Y²/X²(x,x²z) (J_GF-F(1-F)/(z(1-z)) G_x)(x,z) とおく（ Rem₀はMathematicaで計算するとき付けた名前， e(x,z)は論文に書いたとき付けた名前．ソフトによって見やすさが違うので…） と，これがx,z,1-zの正係数多項式になることが言えれば F≦1 かつ D' 上で J_GF>0 となり，証明が終わる（0 にならないことは 項を具体的に見ると言えるのでここでは省略）． つまり，３変数正係数多項式 f(x,z,s) をうまく見つけて， Rem₀=e(x,z)=f(x,z,1-z) としたい．

試行錯誤で見いだした e_c(x,z,s) = ct[x,z,s]（右辺はMathematicaで使った名前） と e_r(x,z,s) = res = Σ_n=9³⁰ resC[n,z,s] xⁿ（同上） を用いて f(x,z,s)=e_c(x,z,s)+e_r(x,z,s) とおくと， e(x,z)=f(x,z,1-z)，すなわち，
Rem₀=ct[x,z,1-z] + res /. s→1-z
がMathematicaによって確かめられた，というのが下の図である．

ところで，Mathematicaと書くと，下の長い式のことを， 機械が勝手に計算したもの，と 思うかもしれないので念のために書いておくと， 「counter term」ct[x,z,s] は，私が全ての項を手で打ち込んだもの． これらは，W に問題2 (19990204)の仮定を満たす項を順次追加しながら 証明を見つけつつ，その証明が成り立つように探し当てた．

F(1-F)/(z(1-z)) G_x(x,z) という意味のよくわからない（が， とりあえず有用な）関数もそのようにして私が見つけたもので， Mathematicaが教えてくれたのではない． Mathematicaにやらせたのは，これらの項を引いた残り e_r の算出で， それはxとzの多項式として得られるので負の符号があちこちに残る． それをzと1-zの正係数多項式に書くのも手で行う必要がある． つまり res の長い式のうちsを含む項はやはり私が手で打ち込んだもの．

このように，手持ちの証明は腕力と感と長い試行錯誤で解いたもので， 数学的描像や物理的描像の知られていない，自動化もできない， 不満足なものです．最大の不満は，もちろん，このままでは高次元（多変数）化 が自動的でないことです．良い証明（および良い定理）が待ち望まれます．

証明の完成図

「Counter term」 e_c(x,z,s) = ct[x,z,s] に負号がないようにできた！

「残差」 e_r(x,z,s) = res = Σ_n=9³⁰ resC[n,z,s] xⁿ に負号がないようにできた！