Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupLeadingSquarePart0.Coefficients190To216

Recurrence 4 lookup certificate: LeadingSquare 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.recurrence4LeadingSquare_coeff_190 :
Polynomial.coeff recurrence4LeadingSquare 190 = (178554888260308744798605351965166093713191465780846669387654255 * 10 ^ 70 + 1932855898491804881767894909025224494921709035648160131941557785913763) * 10 ^ 70 + 3081809341175198990974473162624653973840552685051314099683159627887249
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_191 :
Polynomial.coeff recurrence4LeadingSquare 191 = -((54550356320818597438313412533021651033068850470973022003055685 * 10 ^ 70 + 6851165584780857508574054735426056336397454108972425173765766917419896) * 10 ^ 70 + 2592832681028403285712879691308962779731925453896005595910323154106704)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_192 :
Polynomial.coeff recurrence4LeadingSquare 192 = (79947986079124818781411508187643733264007354146059326235826 * 10 ^ 70 + 8788641382508637812167172088113913542853935351261498657428237994829208) * 10 ^ 70 + 8383355844330055557577817296688410381994863836563461300715694302074870
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_193 :
Polynomial.coeff recurrence4LeadingSquare 193 = (19033585229871521603635727455854202438437269180620431995229184 * 10 ^ 70 + 6887226835084185243990397228568769895764039907375549617772294725447126) * 10 ^ 70 + 7733711428957881454155092267570076416130860253939500444169016806327422
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_194 :
Polynomial.coeff recurrence4LeadingSquare 194 = -((21908149269648278913052561826394292426415896710593631842298270 * 10 ^ 70 + 7565396811212562719419877134326117000322586212972673598492327025181976) * 10 ^ 70 + 9220873766674773731400734255703854588622606299268753445166094278595146)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_195 :
Polynomial.coeff recurrence4LeadingSquare 195 = (18525154999457191607976867945439538629780998034019553937159367 * 10 ^ 70 + 3399246308375386732823591470794107201397977864713150157160542741290606) * 10 ^ 70 + 541550666544015390877695442926669895765494946888180752712087473334776
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_196 :
Polynomial.coeff recurrence4LeadingSquare 196 = -((13642155493564864168801327951141252711060597176702372943301745 * 10 ^ 70 + 1372836877418335030369345481056357285541438473873664775315050696012610) * 10 ^ 70 + 8428952499319725181187355720474458726530280358329790169220372948614205)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_197 :
Polynomial.coeff recurrence4LeadingSquare 197 = (9222556739430457217591477642043334320190993912415588673929429 * 10 ^ 70 + 8761117695608078945469975531605396282759945780590815082813037157635986) * 10 ^ 70 + 8110621472275898222800497071759086378856074107190639038055011012874822
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_198 :
Polynomial.coeff recurrence4LeadingSquare 198 = -((5854962965970539960692350176768358415929564648006178317720213 * 10 ^ 70 + 2151694220550362963030388092244548740823084130472979477337000291908761) * 10 ^ 70 + 5336156219102710445194773345608836187031711829284945181457539884581333)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_199 :
Polynomial.coeff recurrence4LeadingSquare 199 = (3529650839839117481991085417492177795523181220181161657000982 * 10 ^ 70 + 3549561976029487334648673230148105351152485047431662457157357290520295) * 10 ^ 70 + 8400904228185774956077976613627476572191493761961954980054012501116194
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_200 :
Polynomial.coeff recurrence4LeadingSquare 200 = -((2031425359192790476137600652948868417244070351281947479769261 * 10 ^ 70 + 3496580799191041603442544040164916236768682212680808682257678932317979) * 10 ^ 70 + 7519199766932589848777544837018274491704959293867659652336132368579047)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_201 :
Polynomial.coeff recurrence4LeadingSquare 201 = (1118101446674178105072408813795805097084767864609131291870959 * 10 ^ 70 + 2718483571752904253766009209419277003658275579916106770685716697832346) * 10 ^ 70 + 8101380399521506760754572810318784663493725641029629761994161692993156
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_202 :
Polynomial.coeff recurrence4LeadingSquare 202 = -((587776085034489181742722704362152415022671325208888741659143 * 10 ^ 70 + 7407647591709426007324830850478747383931326856565915243108546491158947) * 10 ^ 70 + 5770382269619844225999035064787523851079132422340502912342917328363400)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_203 :
Polynomial.coeff recurrence4LeadingSquare 203 = (293724495020284414742646707318533091051348636003840799794347 * 10 ^ 70 + 848957046153631202925748598011923816653635632768907748713825389404190) * 10 ^ 70 + 9587573184102620602297883228382699756718449048510737060829855276623504
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_204 :
Polynomial.coeff recurrence4LeadingSquare 204 = -((138146235916756014185233960276830315276604659227619718950042 * 10 ^ 70 + 5621815214009538176359639016930255616691817302773722261190002112407061) * 10 ^ 70 + 3301498636217317506355315237792281465266561878775536786081262567223106)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_205 :
Polynomial.coeff recurrence4LeadingSquare 205 = (59931615319374241767326672524370710038306975290437454049528 * 10 ^ 70 + 7440097757870403308896179313275423597982904468841654785735738144888850) * 10 ^ 70 + 7760579398933309833241004641828713496709220593672530267603798516292862
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_206 :
Polynomial.coeff recurrence4LeadingSquare 206 = -((22914586769981557950246554087972311189008050161231720830279 * 10 ^ 70 + 7926597319396733789269471782790881428292590685695793556198707163180052) * 10 ^ 70 + 319661169039109044608324629669152682338070708565897518853734000876014)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_207 :
Polynomial.coeff recurrence4LeadingSquare 207 = (6731369246930313602685835123634922289792745043722707048388 * 10 ^ 70 + 732706282695275527434783660026488741324047999644938363481640863482616) * 10 ^ 70 + 9749892902928182452770237320994581283328814298508179892579379576435278
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_208 :
Polynomial.coeff recurrence4LeadingSquare 208 = -((467110432716333619273927970094717356228540193505189280638 * 10 ^ 70 + 73280821615806920862195282976508134186585692154920159147302227396376) * 10 ^ 70 + 127659044095977391138687251443728738735081071148392406371533227781138)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_209 :
Polynomial.coeff recurrence4LeadingSquare 209 = -((1429763217149544081871020217819506377314314363194472312655 * 10 ^ 70 + 2704442104185773581299873302702121986794469920239816070555035238922577) * 10 ^ 70 + 3161167998444256910652466351806593018932792193090182120058384057647620)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_210 :
Polynomial.coeff recurrence4LeadingSquare 210 = (1617307332044024782745970452879310057193144124250651412839 * 10 ^ 70 + 4444739749277732709266995631056153579859771368344941770327622469415568) * 10 ^ 70 + 6441966623150463089491583774186506059060430442014504040101632580208630
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_211 :
Polynomial.coeff recurrence4LeadingSquare 211 = -((1273576612115461003392454228112259966788798432688880640597 * 10 ^ 70 + 6936558912361851468075072141823349206288764675865241186365954613516729) * 10 ^ 70 + 2714362406862929629431234780658842875655134603132655628125589694632496)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_212 :
Polynomial.coeff recurrence4LeadingSquare 212 = (864229645484271579707317395321720879462866700144347582286 * 10 ^ 70 + 5833979170191483996272174138365220131189731496669862554024512242952481) * 10 ^ 70 + 3831928111162587755099597829505962832883481591195493878552608970892129
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_213 :
Polynomial.coeff recurrence4LeadingSquare 213 = -((537291077426076647307224153769029499729321498364986281415 * 10 ^ 70 + 1308785514056070383626003157641489046357813296420328598683772479834389) * 10 ^ 70 + 7985421111113724447875094722186302111529392023559604933013360383889956)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_214 :
Polynomial.coeff recurrence4LeadingSquare 214 = (314118366479036277206287405150093316606508846496231224643 * 10 ^ 70 + 3499099353601243422945060497297648483885625698913192331188199818615048) * 10 ^ 70 + 2359436178444118264332469906364503507120249635808556086920529378139176
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_215 :
Polynomial.coeff recurrence4LeadingSquare 215 = -((175012018588993423799011552077475955944490310495376031350 * 10 ^ 70 + 6273256964686908273041603041432356335896946979170196605165649000144141) * 10 ^ 70 + 2299682090664432159306488312650284856947184979346659261620976485988898)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_216 :
Polynomial.coeff recurrence4LeadingSquare 216 = (93624237253306707627581667445594295377018896745704616653 * 10 ^ 70 + 7153373162677362050465416334983490579363535999500776248494433248403253) * 10 ^ 70 + 8216001819229903372954493649727480499353752440603151321264818795449888