Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0MainPart3.Coefficients431To455

Recurrence 4 lookup certificate: Scalar0Main coefficient convolution #

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_431 :
Polynomial.coeff recurrence4Scalar0Main 431 = -(((120985756400612448898241918966269388023544177 * 10 ^ 70 + 4662278581494059993048973678439568493269499639466528147889461577211097) * 10 ^ 70 + 4229312824541449729708523051820385061801318059619653446903259786725271) * 10 ^ 70 + 2385317228459318097564969620294235831593550969613292237495654812763547)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_432 :
Polynomial.coeff recurrence4Scalar0Main 432 = ((30557767028647409212167410996067924926612237 * 10 ^ 70 + 2636623189408979983942455345348701065312929423368558280544541864705999) * 10 ^ 70 + 9545555211440358986670112521923079610946870096138969513845296303903952) * 10 ^ 70 + 2915280950073435333001267110279966639970891240091569452149829914866391
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_433 :
Polynomial.coeff recurrence4Scalar0Main 433 = -(((7176865714575833252379059221873567614167815 * 10 ^ 70 + 2468995885791404546294761517606435515771105207251800198280150025964870) * 10 ^ 70 + 3387764538895543893981417871127745914348689279424620782694634418428481) * 10 ^ 70 + 1982168037633905721687699990189618302311766633572779873368434535315909)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_434 :
Polynomial.coeff recurrence4Scalar0Main 434 = ((1530211956596711997321520713571003015278419 * 10 ^ 70 + 6777681860631142281974699676006673508856118855073838228309968188109486) * 10 ^ 70 + 9086915975578192722393383328140020605826418829812814227026126504574148) * 10 ^ 70 + 7185875256959842875798673996913368204430424103976113463723147591404416
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_435 :
Polynomial.coeff recurrence4Scalar0Main 435 = -(((280678434555424754598227455076597137867806 * 10 ^ 70 + 6239446640979640448042394947636046330431506368137464135631800022221516) * 10 ^ 70 + 8307972817091074843344451149291166239116719032536698929201732196395631) * 10 ^ 70 + 5062454641597746986676816795923721257522527944782313787624768635790169)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_436 :
Polynomial.coeff recurrence4Scalar0Main 436 = ((37302050373589897392556640996360113722004 * 10 ^ 70 + 2396779546724074622337333288061684492346963857644328442086431431633049) * 10 ^ 70 + 5723691000343855467067679379937596538146029964986113406890186362742438) * 10 ^ 70 + 8544143416637285652771848931452455572920796742587547797109868463343292
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_437 :
Polynomial.coeff recurrence4Scalar0Main 437 = ((56013523658463775727202315192786225514 * 10 ^ 70 + 7237237937013311989109297840296052243364456964473264303100959763276981) * 10 ^ 70 + 1738839919800801400543885458626288033736696369141927783351659308836674) * 10 ^ 70 + 1379961316780581552845856414580116650746443731912769745084778537713355
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_438 :
Polynomial.coeff recurrence4Scalar0Main 438 = -(((2426905246451285571545307530393778298529 * 10 ^ 70 + 7835636671415713981733254761979378898391831653427352335150561699549334) * 10 ^ 70 + 481619279675433548430823817981893414631956641922334909781909937187113) * 10 ^ 70 + 6533861772151123092839957485851363516671500799166819912291744174458530)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_439 :
Polynomial.coeff recurrence4Scalar0Main 439 = ((1166062663133568486576435041544701714003 * 10 ^ 70 + 3593619599716695526780525789233447300965874427646051002839607765381833) * 10 ^ 70 + 5334707293497503890741322599213459642240680016535069061044837620360114) * 10 ^ 70 + 3475444541519668829821615357514277636273962766692220261639080729170809
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_440 :
Polynomial.coeff recurrence4Scalar0Main 440 = -(((406402383150994509105440543736521247432 * 10 ^ 70 + 4670899650771093143084617273161037459378594377201484656258451083070666) * 10 ^ 70 + 7083251340799553499442309258909023313668223844646318235375737892356149) * 10 ^ 70 + 6964990110079226734865863446092480561676232152643796231260493915010753)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_441 :
Polynomial.coeff recurrence4Scalar0Main 441 = ((121469624748985213751719335468800954609 * 10 ^ 70 + 3383181517082165205759499168189408347716804558231062592817811637248054) * 10 ^ 70 + 5822440491356025933310380907313690278010587133142377929576232290427719) * 10 ^ 70 + 5655412764941814691605151360981983899067827100508333882114645851125942
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_442 :
Polynomial.coeff recurrence4Scalar0Main 442 = -(((32789762321880366882245737768896169735 * 10 ^ 70 + 5659575833058413227934390812502968981669866034635492453973167126740907) * 10 ^ 70 + 6882662638040831727359304365228912714609063909104761536063207030173421) * 10 ^ 70 + 1499063311114556492617634630086015032309109058119469525729638201070927)