Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupA3SquarePart0.Coefficients0To74

Recurrence 5 lookup certificate: A3Square coefficient convolution #

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_14 :
Polynomial.coeff recurrence5A3Square 14 = -(166450582 * 10 ^ 70 + 3605097591348133179468048042033904167907031404191508775846429354786111)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_15 :
Polynomial.coeff recurrence5A3Square 15 = 7543846123 * 10 ^ 70 + 8334319333988075588859692798925588658853238352142717683367152351077242
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_16 :
Polynomial.coeff recurrence5A3Square 16 = 17509441081551 * 10 ^ 70 + 7798199033656443336770392226412570264486761272685110279467072166606713
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_17 :
Polynomial.coeff recurrence5A3Square 17 = -(9942697889984245 * 10 ^ 70 + 158247506024025344476138327578832025203928300939238416424705630823846)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_18 :
Polynomial.coeff recurrence5A3Square 18 = 3287694666803357455 * 10 ^ 70 + 1389358036731827367590588245785640279210513562310543061345006489199318
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_19 :
Polynomial.coeff recurrence5A3Square 19 = -(779167558967609905930 * 10 ^ 70 + 8581808123955102041046151845121004744581015577768528577082629928299216)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_20 :
Polynomial.coeff recurrence5A3Square 20 = 139275052861061560623756 * 10 ^ 70 + 2598758674519134487041777565551619287663394645434607976427860234442031
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_21 :
Polynomial.coeff recurrence5A3Square 21 = -(18654923187388693606948207 * 10 ^ 70 + 8619298648530190537819973614468492423997010452514000862695339164798110)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_22 :
Polynomial.coeff recurrence5A3Square 22 = 1709117534918668108243101790 * 10 ^ 70 + 8335458132460587930592825060056541304266945031664927665113541688557642
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_23 :
Polynomial.coeff recurrence5A3Square 23 = -(57101255709259215339688433644 * 10 ^ 70 + 7566198959727099731173177271541048798511643618601935720409841738287716)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_24 :
Polynomial.coeff recurrence5A3Square 24 = -(13808590663632299237984798978636 * 10 ^ 70 + 2445798406638283214190151920310442524065231677140804712298161383191878)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_25 :
Polynomial.coeff recurrence5A3Square 25 = 3380326577409046574716735872749196 * 10 ^ 70 + 3992019085393602879747599381737664192644569150175531032230535714242276
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_26 :
Polynomial.coeff recurrence5A3Square 26 = -(446699496885062070738758222439535660 * 10 ^ 70 + 2273177577707747746136510322282853062755179124896382416512536796643665)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_27 :
Polynomial.coeff recurrence5A3Square 27 = 41018973064175823597972865941976444230 * 10 ^ 70 + 3347531450206665141811429888178760610401840989761462381809108290756540
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_28 :
Polynomial.coeff recurrence5A3Square 28 = -(2501230562759208612736587526972667108140 * 10 ^ 70 + 3613407374212020976123114088870870915423645191997627364330391701897670)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_29 :
Polynomial.coeff recurrence5A3Square 29 = 44262071216989959558112385784013443931931 * 10 ^ 70 + 1953667550473496597852315272118998422139093206392047747114481056150890
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_30 :
Polynomial.coeff recurrence5A3Square 30 = 12497260086610676206216989454037689320051099 * 10 ^ 70 + 4476081623049180791230493165636542040520167716176603408591260637880605
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_31 :
Polynomial.coeff recurrence5A3Square 31 = -(2128425869964095548987571554219863706182081407 * 10 ^ 70 + 3516828423646438897419352263507750922619768829887576925817675931466710)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_32 :
Polynomial.coeff recurrence5A3Square 32 = 221263121888724507797803419036141927958841292981 * 10 ^ 70 + 7954891285576576481154151203758381082077949016233498784157701000020578
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_33 :
Polynomial.coeff recurrence5A3Square 33 = -(18036717320149191057814514417800093743917091259147 * 10 ^ 70 + 6609359308622226887489731353166208036119458979498389248478757651885376)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_34 :
Polynomial.coeff recurrence5A3Square 34 = 1238385999100145073419378117639036187652909722200522 * 10 ^ 70 + 8521212333289694765776407500076242202377262146570670476441532995562071
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_35 :
Polynomial.coeff recurrence5A3Square 35 = -(73933644769880433328301630099587671281748214976114755 * 10 ^ 70 + 1372101125291796773959024914567702155541062654009757924618341637935390)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_36 :
Polynomial.coeff recurrence5A3Square 36 = 3905842687640756919354348591712370907259390021427481098 * 10 ^ 70 + 7665529904269693197960567378622965330943546029790507051590579142509330
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_37 :
Polynomial.coeff recurrence5A3Square 37 = -(184568031786403166012672323386376333264792728395315873257 * 10 ^ 70 + 1614351513665394785410985170090633518661836965648230512287262159872792)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_38 :
Polynomial.coeff recurrence5A3Square 38 = 7856332142681586192696515327030624476909959076426972072051 * 10 ^ 70 + 2708563103381287189069304297051755937626221347859776236176655253057449
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_39 :
Polynomial.coeff recurrence5A3Square 39 = -(302615200448093469831279070611371901656787135313951859111092 * 10 ^ 70 + 3662458259861731643262194264220018209322955414468654178940884232187774)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_40 :
Polynomial.coeff recurrence5A3Square 40 = 10576221659974862925436344525502557092409958658009658280236713 * 10 ^ 70 + 9633114156025153593556855907315708485123655846999869498088093264379306
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_41 :
Polynomial.coeff recurrence5A3Square 41 = -(335684229826703897965298438093960749490740920398015090996715245 * 10 ^ 70 + 8865704440262144005006595211165310808328969713792891661424481165523058)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_42 :
Polynomial.coeff recurrence5A3Square 42 = 9665084347623854735151218080855346053302129456878855483078663627 * 10 ^ 70 + 9581757976099154946391088000202170401678522910750491096397494386521362
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_43 :
Polynomial.coeff recurrence5A3Square 43 = -(251452402721286714908653431758715380198674056945260859978069851027 * 10 ^ 70 + 8177228327620953550891714378083325678741294057140577718072473421853374)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_44 :
Polynomial.coeff recurrence5A3Square 44 = 5861253797936143103574475236119688592975382481890859338803625071091 * 10 ^ 70 + 1662375150163152103767321160842383302585237077056314718064356601162018
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_45 :
Polynomial.coeff recurrence5A3Square 45 = -(120292001687801859253761316006275253541304633577098676006926495760671 * 10 ^ 70 + 6349338342697719095524390754496056339849356739086840614488370724642044)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_46 :
Polynomial.coeff recurrence5A3Square 46 = 2090826524490340013960495445296378015746008038519115952284315580905569 * 10 ^ 70 + 9228158794227619971850004686335431016368681698674038697170592641952849
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_47 :
Polynomial.coeff recurrence5A3Square 47 = -((2 * 10 ^ 70 + 7572449620992398805741267980062120956041005553218725095518557862311559) * 10 ^ 70 + 7792463268582591114986893866568148425818277698858617875683642233469954)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_48 :
Polynomial.coeff recurrence5A3Square 48 = (14 * 10 ^ 70 + 3784771811508592298098254933128141113978125070243964107176213431383061) * 10 ^ 70 + 4479061669138887364092372650501874937609763792343826977856687940235486
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_49 :
Polynomial.coeff recurrence5A3Square 49 = (622 * 10 ^ 70 + 3874760536547307444797058436322702309425705216895687675645978213219997) * 10 ^ 70 + 7913727701046530720320232991571792756664052302149926688713596783251562
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_50 :
Polynomial.coeff recurrence5A3Square 50 = -((28782 * 10 ^ 70 + 9003437708774289525780717417196259433628461878097893682367201375772841) * 10 ^ 70 + 6259378180893912922254460132347081996166184550550779475900315123574149)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_51 :
Polynomial.coeff recurrence5A3Square 51 = (798438 * 10 ^ 70 + 5119441862903790126577137999366606793447134134294724349026246780695537) * 10 ^ 70 + 2425252691740575175311241441333642128568747616801022385798271158344088
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_52 :
Polynomial.coeff recurrence5A3Square 52 = -((17588091 * 10 ^ 70 + 6494441672122902186365614542897059593199446906692466583503729467744936) * 10 ^ 70 + 6916607759758144522258385038215127163147978589033570972110502010030872)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_53 :
Polynomial.coeff recurrence5A3Square 53 = (327479859 * 10 ^ 70 + 5677264132291219703368003864501900810704960337885542762439646045235021) * 10 ^ 70 + 8719978582217816763813896545534603104016105540061891775341395890829712
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_54 :
Polynomial.coeff recurrence5A3Square 54 = -((5200936968 * 10 ^ 70 + 1128014051954333922456073992412716448166983603627035419068196651639400) * 10 ^ 70 + 2051469038037532879920882449278843523983597995012989555717046131829122)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_55 :
Polynomial.coeff recurrence5A3Square 55 = (68224921058 * 10 ^ 70 + 1818782384152844731303679930818342319029890268730740517192537555437383) * 10 ^ 70 + 185830980835822694775882941840727929902808623079765694499886202968908
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_56 :
Polynomial.coeff recurrence5A3Square 56 = -((644167376017 * 10 ^ 70 + 5193824744617356420271174273377115407556300701709785617564816807740698) * 10 ^ 70 + 515707852177017748980989527803729231042541013547449201192963769652560)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_57 :
Polynomial.coeff recurrence5A3Square 57 = (975816666110 * 10 ^ 70 + 5392929564111298419707984164677209237089720344080374302340736656311773) * 10 ^ 70 + 4855440976339857083581322024348148652239104247785058884755759530355836
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_58 :
Polynomial.coeff recurrence5A3Square 58 = (142440259449104 * 10 ^ 70 + 7868288399649617924938472747669511166447641412751210915722282117907506) * 10 ^ 70 + 2102685856980623284317757332908912529898925985236376125524661704288581
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_59 :
Polynomial.coeff recurrence5A3Square 59 = -((4524778189895068 * 10 ^ 70 + 333767163898401978004488902282283119827617271981974631782066076497414) * 10 ^ 70 + 9472606956248383889841745353592112741809668485137043614713776690235674)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_60 :
Polynomial.coeff recurrence5A3Square 60 = (98600111483128853 * 10 ^ 70 + 1471125153983176277784629494728241361543463954030924830166480108047587) * 10 ^ 70 + 2295810853996328070259717360496631467757075557990857383582493523278047
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_61 :
Polynomial.coeff recurrence5A3Square 61 = -((1799615918029250337 * 10 ^ 70 + 6637762707509171157687998503809297250723164931989972821898033640891751) * 10 ^ 70 + 9419088755357423047466648863294920145349477298744721685627254905123856)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_62 :
Polynomial.coeff recurrence5A3Square 62 = (29226786096785135326 * 10 ^ 70 + 6598632219677595146567094347276813802496664848861998746165974502262480) * 10 ^ 70 + 7155440812012365503582868906566137186869715447395982182593363595593867
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_63 :
Polynomial.coeff recurrence5A3Square 63 = -((433993071746667821340 * 10 ^ 70 + 6695904949060623122947028358519714978469873706877080493183747333818445) * 10 ^ 70 + 6593067018365465370464759684783831366090306418658387005585468350789754)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_64 :
Polynomial.coeff recurrence5A3Square 64 = (5980818577766308123737 * 10 ^ 70 + 9292775839717814710526336710310899861589751773418497267629399512036540) * 10 ^ 70 + 9922388126752812057836898270054061007630494074687274738386757446346193
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_65 :
Polynomial.coeff recurrence5A3Square 65 = -((77204914074522710761846 * 10 ^ 70 + 7566740003071471723646733489261655480757138842502592417182156540750971) * 10 ^ 70 + 6690713369638020217595157690193867805948627167061695218774461223450660)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_66 :
Polynomial.coeff recurrence5A3Square 66 = (939451914720523164546713 * 10 ^ 70 + 4834515287507003873280227691574213174438227228110034260047962656489791) * 10 ^ 70 + 5450198905685975831587661067920259493411539411779210721675866784792269
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_67 :
Polynomial.coeff recurrence5A3Square 67 = -((10825190616939704997447355 * 10 ^ 70 + 8211179006893203856342581955328764598527985091313486445381554470094062) * 10 ^ 70 + 6214993600708324796821844815826433071961133232933447659344114910505604)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_68 :
Polynomial.coeff recurrence5A3Square 68 = (118533709488669808349652447 * 10 ^ 70 + 499472392943932522872702693471261423005140852865127914981644343275112) * 10 ^ 70 + 7711635852661516090290240932307215259562371212857638431476076237491697
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_69 :
Polynomial.coeff recurrence5A3Square 69 = -((1236783883198566475426153712 * 10 ^ 70 + 3060258314537551798177648041400944758988323387561644132363132794051120) * 10 ^ 70 + 7226908589573750745776275185606369335713116178542094673802444002754702)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_70 :
Polynomial.coeff recurrence5A3Square 70 = (12324616775014453059658391841 * 10 ^ 70 + 109640590312846582141519131056648830260188232206081568284356824419590) * 10 ^ 70 + 9752187882985703294528994392473248359366958159916182289603603216548308
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_71 :
Polynomial.coeff recurrence5A3Square 71 = -((117518149462740668527966334030 * 10 ^ 70 + 8644798158954764064494547903605507601028460245966919156001841665854382) * 10 ^ 70 + 9720635214980388580826371572159082903313818990705146047568318795941016)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_72 :
Polynomial.coeff recurrence5A3Square 72 = (1073976470745713767517014733895 * 10 ^ 70 + 6537396547155318159202252965631537977745619801461019078847409034135444) * 10 ^ 70 + 1627976035860434396553520614418769741861482368792901547448579916282963
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_73 :
Polynomial.coeff recurrence5A3Square 73 = -((9420170553458137521542643077315 * 10 ^ 70 + 1159578646732249376791986830386620796270297390581005142219475782244716) * 10 ^ 70 + 7734824376684834673531029047846591697181927125929205502037463975674160)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_74 :
Polynomial.coeff recurrence5A3Square 74 = (79403855380629573690349110019263 * 10 ^ 70 + 3685607299199232507765489880107204463422803450753683556909660670886263) * 10 ^ 70 + 6137978215745583985631597541060069518948951404259125783984462164218564