(* ::Package:: *)

(* ::Text:: *)
(*n = 7 verification (Lemma 2.7): Z7(\[Alpha],t)=-1*)
(**)


(* ::Input:: *)
(*\[Omega]=Sqrt[(4-11 t+8 t^2)/t];*)


(* ::Input:: *)
(*\[Alpha]\[Alpha]=(-13+81 t^1-169 t^2+64 t^3+260 t^4-416 t^5+256 t^6-72 t^7+8 t^8)/(8 (-1+t)^3 t^2   (-1+5 t^1-6 t^2+t^3))+((-1-7 t^1+65 t^2-164 t^3+180 t^4-88 t^5+16 t^6) \[Omega]\[Omega])/(8 (-1+t)^3 t^2  (-1+5 t^1-6 t^2+t^3));*)


(* ::Input:: *)
(*q=(2t-1)^10;*)
(**)
(*p61=16t^5(-10+27 t+288 t^2-2022 t^3+5825 t^4-9477 t^5+9336 t^6-5494 t^7+1712 t^8-122 t^9-80 t^10+16 t^11);*)
(*p62=(-16 t^6)(-25+206 t-726 t^2+1459 t^3-1927 t^4+1870 t^5-1394 t^6+724 t^7-210 t^8+24 t^9);*)
(*p41=(-4t^3)(50-687 t+4203 t^2-15695 t^3+41282 t^4-82204 t^5+125852 t^6-144150 t^7+117216 t^8-62520 t^9+18496 t^10-1080 t^11-960 t^12+192 t^13);*)
(*p42=4t^3(10-121 t+677 t^2-2521 t^3+7132 t^4-15412 t^5+24800 t^6-29742 t^7+27184 t^8-18840 t^9+9072 t^10-2520 t^11+288 t^12);*)
(*p21=(-2+40 t-360 t^2+2245 t^3-11098 t^4+42924 t^5-126314 t^6+282304 t^7-483968 t^8+638896 t^9-640864 t^10+470400 t^11-234144 t^12+65792 t^13-2784 t^14-3840 t^15+768 t^16);*)
(*p22=-t^3(65-774 t+4344 t^2-15694 t^3+41224 t^4-82096 t^5+124784 t^6-144768 t^7+127840 t^8-83808 t^9+37824 t^10-10080 t^11+1152 t^12);*)
(*p01=(1-t) (1-19 t+161 t^2-924 t^3+4066 t^4-13822 t^5+35840 t^6-70584 t^7+105400 t^8-118168 t^9+96704 t^10-54208 t^11+17760 t^12-1440 t^13-1024 t^14+256 t^15);*)
(*p02=t^3 (25-290 t+1636 t^2-6010 t^3+15992 t^4-32064 t^5+48928 t^6-56632 t^7+49024 t^8-30752 t^9+13120 t^10-3360 t^11+384 t^12);*)
(*p11=8t^3(t-1)(-125+4005 t-60169 t^2+570158 t^3-3862166 t^4+20045945 t^5-83223823 t^6+284217439 t^7-813613881 t^8+1978202656 t^9-4124892528 t^10+7432364016 t^11-11645707296 t^12+15960414880 t^13-19242695952 t^14+20530254512 t^15-19487643408 t^16+16504985216 t^17-12441863808 t^18+8263236224 t^19-4749495424 t^20+2309017088 t^21-926839040 t^22+300215040 t^23-76503296 t^24+14585856 t^25-1794048 t^26+73728 t^27+8192 t^28);*)
(*p12=8t^3(1-t)(-25+765 t-11171 t^2+105634 t^3-736638 t^4+4055851 t^5-18297419 t^6+69029409 t^7-220386161 t^8+599953820 t^9-1399432680 t^10+2804818368 t^11-4835265904 t^12+7165985152 t^13-9113381872 t^14+9916520688 t^15-9197207856 t^16+7238388416 t^17-4811313152 t^18+2688147584 t^19-1256283520 t^20+488377856 t^21-156990208 t^22+41689856 t^23-9309952 t^24+1799168 t^25-280576 t^26+24576 t^27);*)
(*p31=8 t^3(t-1)(-125+4005 t-59369 t^2+553998 t^3-3730470 t^4+19565545 t^5-83537119 t^6+297885767 t^7-901975729 t^8+2350136384 t^9-5333296784 t^10+10652922784 t^11-18880321184 t^12+29852879392 t^13-42255474560 t^14+53630116864 t^15-60971031168 t^16+61759492352 t^17-55128623872 t^18+42657332224 t^19-28037451008 t^20+15314942464 t^21-6803466496 t^22+2405327616 t^23-657957120 t^24+131469312 t^25-16441344 t^26+663552 t^27+73728 t^28);*)
(*p32=8 t^3(1-t)(-25+765 t-11171 t^2+107634 t^3-787518 t^4+4665067 t^5-22973819 t^6+95297577 t^7-336259225 t^8+1016942748 t^9-2647457192 t^10+5940364352 t^11-11479425312 t^12+19070848736 t^13-27171006848 t^14+33097766976 t^15-34341234112 t^16+30212895232 t^17-22415990528 t^18+13930544128 t^19-7190272256 t^20+3053491200 t^21-1060255488 t^22+303176448 t^23-73578240 t^24+15455232 t^25-2525184 t^26+221184 t^27);*)
(*p51=128t^8(t-1)(-1500+28960 t-257939 t^2+1404604 t^3-5211955 t^4+13795890 t^5-25855137 t^6+29614248 t^7+3063112 t^8-113012293 t^9+333031055 t^10-652968101 t^11+993241608 t^12-1221269400 t^13+1224164696 t^14-994694744 t^15+647101024 t^16-331790224 t^17+131533872 t^18-39147024 t^19+8229120 t^20-1046016 t^21+41472 t^22+4608 t^23);*)
(*p52=128 t^8(1-t)(-100+80 t+20039 t^2-260728 t^3+1786957 t^4-8269540 t^5+28531279 t^6-77414974 t^7+170435054 t^8-309998835 t^9+470441223 t^10-598385907 t^11+638090092 t^12-567729488 t^13+417123064 t^14-249429768 t^15+119783328 t^16-46124976 t^17+14587824 t^18-3960432 t^19+919872 t^20-157824 t^21+13824 t^22);*)
(*p71=2048 t^13(t-1)(-25+56 t+2520 t^2-25565 t^3+120032 t^4-330197 t^5+533239 t^6-339915 t^7-575358 t^8+1899107 t^9-2748394 t^10+2566194 t^11-1675233 t^12+781067 t^13-257689 t^14+57232 t^15-7392 t^16+288 t^17+32 t^18);*)
(*p72=2048 t^13(1-t)(-1-50 t+626 t^2-2319 t^3-1948 t^4+47711 t^5-201331 t^6+485563 t^7-779658 t^8+878711 t^9-712736 t^10+425072 t^11-193639 t^12+72003 t^13-23071 t^14+6068 t^15-1096 t^16+96 t^17);*)


(* ::Text:: *)
(**)
(*Two particular checks and a plot*)


(* ::Input:: *)
(*RootReduce[1/q{Sqrt[p71+p72 \[Omega]\[Omega]],p61+p62 \[Omega]\[Omega],-Sqrt[p51+p52 \[Omega]\[Omega]],p41+p42 \[Omega]\[Omega],Sqrt[p31+p32 \[Omega]\[Omega]],p21+p22 \[Omega]\[Omega],-Sqrt[p11+p12 \[Omega]\[Omega]],p01+p02 \[Omega]\[Omega]}.Table[Sqrt[A]^j,{j,7,0,-1}]/.A->\[Alpha]\[Alpha]/.\[Omega]\[Omega]->\[Omega]/.{{t->4/5},{t->1/(11-4Sqrt[6])}}]*)


(* ::Input:: *)
(*Plot[1/q{Sqrt[p71+p72 \[Omega]\[Omega]],p61+p62 \[Omega]\[Omega],-Sqrt[p51+p52 \[Omega]\[Omega]],p41+p42 \[Omega]\[Omega],Sqrt[p31+p32 \[Omega]\[Omega]],p21+p22 \[Omega]\[Omega],-Sqrt[p11+p12 \[Omega]\[Omega]],p01+p02 \[Omega]\[Omega]}.Table[Sqrt[A]^j,{j,7,0,-1}]/.A->\[Alpha]\[Alpha]/.\[Omega]\[Omega]->\[Omega],{t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0],1},PlotRange->{-1.1,-.9},WorkingPrecision->30]*)


(* ::Text:: *)
(**)
(*Note that we will need 4 lemmas:*)
(**)
(*\[Alpha]*b1=u1/q, \[Alpha]^3*b3=u3/q, \[Alpha]^5*b5=u5/q,\[Alpha]^7*b7=u7/q *)
(**)
(*u1,u3,u5,u7 has the form (P1+P2)\[Omega]/Q ,where P1,P2,Q are suitable polynomials of t.*)


(* ::Input:: *)
(*u1=(-10+198 t-1742 t^2+9029 t^3-30986 t^4+74600 t^5-128398 t^6+153928 t^7-113584 t^8+22480 t^9+49912 t^10-57728 t^11+28480 t^12-7808 t^13+2656 t^14-1280 t^15+256 t^16)- \[Omega]\[Omega] t(10-174 t+1409 t^2-7126 t^3+25020 t^4-63866 t^5+121016 t^6-171312 t^7+180480 t^8-140328 t^9+80640 t^10-35392 t^11+12352 t^12-3104 t^13+384 t^14);*)
(*u3=1/(4 (-1+t)^3 t^3) (85 t-1530 t^2+11801 t^3-45890 t^4+41000 t^5+573384 t^6-3922012 t^7+14743612 t^8-38993060 t^9+77564192 t^10-118920088 t^11+141854664 t^12-132268192 t^13+97062688 t^14-56854208 t^15+27058816 t^16-10397056 t^17+2955904 t^18-459904 t^19-25728 t^20+24576 t^21-3072 t^22+t (5+26 t-1583 t^2+18062 t^3-114412 t^4+486044 t^5-1488148 t^6+3355172 t^7-5454140 t^8+5774672 t^9-2173480 t^10-4792760 t^11+11086592 t^12-12846496 t^13+10198080 t^14-6137984 t^15+2960896 t^16-1140864 t^17+322944 t^18-57216 t^19+4608 t^20) \[Omega]\[Omega]);*)
(*u5=1/(4 (-1+t)^6 t^3) (-250 t+2987 t^2+4045 t^3-313967 t^4+2996100 t^5-16116136 t^6+58167348 t^7-149013636 t^8+272559440 t^9-335591112 t^10+197736736 t^11+199225392 t^12-723484336 t^13+1121333232 t^14-1215613648 t^15+1022423712 t^16-691412576 t^17+377059456 t^18-161992864 t^19+52100096 t^20-11373440 t^21+1286912 t^22+47232 t^23-33792 t^24+3072 t^25-t (10+391 t-9797 t^2+89447 t^3-426220 t^4+970280 t^5+778040 t^6-14382620 t^7+57858672 t^8-144875368 t^9+260147248 t^10-352440432 t^11+368727984 t^12-300424464 t^13+188428624 t^14-84962240 t^15+18995168 t^16+8535104 t^17-11947808 t^18+6943232 t^19-2508672 t^20+576000 t^21-77184 t^22+4608 t^23) \[Omega]\[Omega]);*)
(*u7=1/(4 (-1+t)^6 t^3) (-33 t-16 t^2+9292 t^3-122404 t^4+793766 t^5-2977444 t^6+5622684 t^7+4021212 t^8-63726144 t^9+227073744 t^10-503694112 t^11+787840912 t^12-888389920 t^13+694326576 t^14-308427104 t^15-34342848 t^16+181724576 t^17-160749120 t^18+84638784 t^19-29409792 t^20+6561152 t^21-788736 t^22+4736 t^23+11264 t^24-1024 t^25+t (-1-90 t+1532 t^2-7096 t^3-28190 t^4+520588 t^5-3157956 t^6+11559500 t^7-28309248 t^8+46157648 t^9-42374448 t^10-6235696 t^11+91494176 t^12-165214832 t^13+179249632 t^14-132624128 t^15+66918944 t^16-20646976 t^17+1733440 t^18+1652608 t^19-877696 t^20+214528 t^21-27776 t^22+1536 t^23) \[Omega]\[Omega]);*)


(* ::Input:: *)
(*Together[\[Alpha]\[Alpha]^1 (p11+p12 \[Omega]\[Omega])-u1^2/.\[Omega]\[Omega]->\[Omega]]*)


(* ::Input:: *)
(*Together[\[Alpha]\[Alpha]^3 (p31+p32 \[Omega]\[Omega])-u3^2/.\[Omega]\[Omega]->\[Omega]]*)


(* ::Input:: *)
(*Together[\[Alpha]\[Alpha]^5 (p51+p52 \[Omega]\[Omega])-u5^2/.\[Omega]\[Omega]->\[Omega]]*)


(* ::Input:: *)
(**)
(*Together[\[Alpha]\[Alpha]^7 (p71+p72 \[Omega]\[Omega])-u7^2/.\[Omega]\[Omega]->\[Omega]]*)


(* ::Input:: *)
(*Together[1/q(u7+(p61+p62 \[Omega]\[Omega])\[Alpha]\[Alpha]^3+u5+(p41+p42 \[Omega]\[Omega])\[Alpha]\[Alpha]^2+u3+(p21+p22 \[Omega]\[Omega])\[Alpha]\[Alpha]+u1+p01+p02 \[Omega]\[Omega])/.\[Omega]\[Omega]->\[Omega]]*)


(* ::Input:: *)
(*Resolve[ForAll[t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0]<t<1,\[Alpha]\[Alpha]^1 (p11+p12 \[Omega]\[Omega])==u1^2/.\[Omega]\[Omega]->\[Omega]],Reals]*)


(* ::Input:: *)
(*Resolve[ForAll[t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0]<t<1,\[Alpha]\[Alpha]^3 (p31+p32 \[Omega]\[Omega])==u3^2/.\[Omega]\[Omega]->\[Omega]],Reals]*)


(* ::Input:: *)
(*Resolve[ForAll[t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0]<t<1,\[Alpha]\[Alpha]^5 (p51+p52 \[Omega]\[Omega])==u5^2/.\[Omega]\[Omega]->\[Omega]],Reals]*)


(* ::Input:: *)
(*Resolve[ForAll[t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0]<t<1,\[Alpha]\[Alpha]^7 (p71+p72 \[Omega]\[Omega])==u7^2/.\[Omega]\[Omega]->\[Omega]],Reals]*)


(* ::Text:: *)
(**)
(*Plots*)


(* ::Input:: *)
(*Plot[-Sqrt[\[Alpha]\[Alpha]^1 (p11+p12 \[Omega]\[Omega])]-u1/.\[Omega]\[Omega]->\[Omega],{t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0],1},PlotRange->{-.1,.1},WorkingPrecision->30]*)


(* ::Input:: *)
(*Plot[Sqrt[\[Alpha]\[Alpha]^3 (p31+p32 \[Omega]\[Omega])]-u3/.\[Omega]\[Omega]->\[Omega],{t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0],1},PlotRange->{-.1,.1},WorkingPrecision->30]*)


(* ::Input:: *)
(*Plot[-Sqrt[\[Alpha]\[Alpha]^5 (p51+p52 \[Omega]\[Omega])]-u5/.\[Omega]\[Omega]->\[Omega],{t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0],1},PlotRange->{-.1,.1},WorkingPrecision->30]*)


(* ::Input:: *)
(*Plot[Sqrt[\[Alpha]\[Alpha]^7 (p71+p72 \[Omega]\[Omega])]-u7/.\[Omega]\[Omega]->\[Omega],{t,Root[-1 + 12 # - 20 #^2 + 8 #^3& , 2, 0],1},PlotRange->{-.1,.1},WorkingPrecision->30]*)
