Recurrence 2 lookup certificate: Scalar4Exceptional coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_262 :
Polynomial.coeff recurrence2Scalar4Exceptional 262 = -((575022726094787759337198481519642167828018308406 * 10 ^ 70 + 2632710713045506671719110345375200020118852681015113069629335336426476) * 10 ^ 70 + 4025885879055168300527720898335846026143194151623310374814263034148513)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_263 :
Polynomial.coeff recurrence2Scalar4Exceptional 263 = (167678852090430807723499534195808965197144357084 * 10 ^ 70 + 2024315295733749452002813755788520404205485112878536041609873973774801) * 10 ^ 70 + 4691917028930871549962132175614103248328699005330554960619679402409385
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_264 :
Polynomial.coeff recurrence2Scalar4Exceptional 264 = -((35066649967830343182883750165194028346696709611 * 10 ^ 70 + 5535750441454928343479647274189682576450113942700711937718403516583309) * 10 ^ 70 + 159750705734797593429233072010859281430036538869431437516320689969933)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_265 :
Polynomial.coeff recurrence2Scalar4Exceptional 265 = (41779203627471408041033887357162194563447848 * 10 ^ 70 + 7522918581010936690876960438961123527397614702594315070835566444640516) * 10 ^ 70 + 2210209492836194273844319431835562839844486724574680201950138681076562
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_266 :
Polynomial.coeff recurrence2Scalar4Exceptional 266 = (5663117074125394913949533327198455175267390397 * 10 ^ 70 + 1402482523424696665559764611208967899942348446721060114798215840620025) * 10 ^ 70 + 6304216027090463506124828395248208620222843505538889463853765742647168
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_267 :
Polynomial.coeff recurrence2Scalar4Exceptional 267 = -((4395670956357391282092658382521099031780905567 * 10 ^ 70 + 6717291359145146525735959590750471568822000089100158139253027095477869) * 10 ^ 70 + 2820179033920463460134423420731564368599250004148613601911860143402889)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_268 :
Polynomial.coeff recurrence2Scalar4Exceptional 268 = (2399681086219680201456429550826046278096210481 * 10 ^ 70 + 4116089505566809607731017482204298783884778886879412702295990705496168) * 10 ^ 70 + 6909684737301049026442477216458587178118995841240349580616128402739976
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_269 :
Polynomial.coeff recurrence2Scalar4Exceptional 269 = -((1022672917594052677251941978339286921128064745 * 10 ^ 70 + 3519920645500179704785071776377585838895322793772537883053851383164042) * 10 ^ 70 + 4246043003976822049869457878631992311416469483692741081684392190215879)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_270 :
Polynomial.coeff recurrence2Scalar4Exceptional 270 = (303704807581783561222964197198021825892062320 * 10 ^ 70 + 7928012524653107764093289758711809940990031161091605144255477914443917) * 10 ^ 70 + 8080701977304376650147994765907404038684170282705829253434327959373193
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_271 :
Polynomial.coeff recurrence2Scalar4Exceptional 271 = -((13148772155267050875992660449807724321785686 * 10 ^ 70 + 4002792877627628131308130651664659821404424260509682529123917136284194) * 10 ^ 70 + 9593145445626604128955665288720766901029691537699431608602578627227114)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_272 :
Polynomial.coeff recurrence2Scalar4Exceptional 272 = -((61754002719692596931219113462119234920624746 * 10 ^ 70 + 2893335767253272701038663542811100222478838590328972442709403402908435) * 10 ^ 70 + 8119505713120501314508015629242958399782540022212778324080609293708713)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_273 :
Polynomial.coeff recurrence2Scalar4Exceptional 273 = (55074507417185054895679285996560048419767848 * 10 ^ 70 + 8664870422009210773487479640810807109538155566561829502509995458651737) * 10 ^ 70 + 9048722746369586197206908818447433664116795468676951319131301168562875
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_274 :
Polynomial.coeff recurrence2Scalar4Exceptional 274 = -((31573604516090731364220172237098011461979255 * 10 ^ 70 + 6623187505291376907451558488132547922445184182443284773529378915103264) * 10 ^ 70 + 5978899047712831707218527798941832107922624165572929657901723678456116)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_275 :
Polynomial.coeff recurrence2Scalar4Exceptional 275 = (13627931195738996295079993569478683438969391 * 10 ^ 70 + 6022841872847468794965130373736804510215437608902785949781646011765458) * 10 ^ 70 + 5370403121510412845338669095678317611013099072809285384565818254937565
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_276 :
Polynomial.coeff recurrence2Scalar4Exceptional 276 = -((4257302776231725624333446109857866305980674 * 10 ^ 70 + 5561051417804602335252400810462723839751972629695643637311171675056457) * 10 ^ 70 + 6081089177529457812502872947438843486202598232604476136949298803426794)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_277 :
Polynomial.coeff recurrence2Scalar4Exceptional 277 = (613698195033000718976352412192445921545953 * 10 ^ 70 + 8668276961712893938718973914628427345617913394704385143326757998378075) * 10 ^ 70 + 7164632808516734827233978995927777502426536956776712510039872949880470
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_278 :
Polynomial.coeff recurrence2Scalar4Exceptional 278 = (324150583235314750101557901624873535145168 * 10 ^ 70 + 7528741108175957959104810085110898965576018585128119212464523641718848) * 10 ^ 70 + 9828238928158421331401639464350061107043780158042944356580315083645493
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_279 :
Polynomial.coeff recurrence2Scalar4Exceptional 279 = -((338491146251273752440975973535868758454778 * 10 ^ 70 + 8826684255686406150956524570091405919380306995030979876222565243120932) * 10 ^ 70 + 4556574050681414549569624027106004139757984613554851187493880758120609)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_280 :
Polynomial.coeff recurrence2Scalar4Exceptional 280 = (182001511212667257440203076252246798634427 * 10 ^ 70 + 298483872065719718378877338443467620915600347763690898843900650533392) * 10 ^ 70 + 253929491545054450793286509208126356298537197694306509945805125478790
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_281 :
Polynomial.coeff recurrence2Scalar4Exceptional 281 = -((69906162063173590450311187775360524416380 * 10 ^ 70 + 9924688500643642770037921961884392236553934326827506321637969757413500) * 10 ^ 70 + 1178924432301624378757215626431261491612950607837632758349836957854829)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_282 :
Polynomial.coeff recurrence2Scalar4Exceptional 282 = (18756371758666819886151188738910072989119 * 10 ^ 70 + 117176408851346550368635497520127966472866493351096412960320693792904) * 10 ^ 70 + 637206102315852649644102632150790390804745108650287898207925016583871
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_283 :
Polynomial.coeff recurrence2Scalar4Exceptional 283 = -((2065898800959257635316519378140697158128 * 10 ^ 70 + 621958254531930174692630388569562659688885129342047791087683229742) * 10 ^ 70 + 383009199304060331456304623500777490728685055536107604342661184418263)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_284 :
Polynomial.coeff recurrence2Scalar4Exceptional 284 = -((1228791816696165620291446478299935740081 * 10 ^ 70 + 2263906508210333914845660717768199339101106010067165849214594589276081) * 10 ^ 70 + 1619582745361205323911328763557877523974708499822015795346168010542608)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_285 :
Polynomial.coeff recurrence2Scalar4Exceptional 285 = (989031115554345134990080095419919044429 * 10 ^ 70 + 2260058143089994458159683369264880855864192094104900003802531739257694) * 10 ^ 70 + 5346606266056545437383582205098553351794571978865694149293184158327727
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_286 :
Polynomial.coeff recurrence2Scalar4Exceptional 286 = -((420051979905012158529395774186639470420 * 10 ^ 70 + 9016955834560818686578441483849346698735270367468257491360212542981458) * 10 ^ 70 + 1353003952009040035085198904873910233647930470590622688257687774333159)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_287 :
Polynomial.coeff recurrence2Scalar4Exceptional 287 = (120536130145503844034897237229926842888 * 10 ^ 70 + 376273644667166362819567343119606650073455754386412130308201074091992) * 10 ^ 70 + 8141870056944101369715927369539288282667432385377772484673646754823493
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_288 :
Polynomial.coeff recurrence2Scalar4Exceptional 288 = -((19268200331628781670068967286786574396 * 10 ^ 70 + 4548946063844529107054675538906884582424577625335338353498311327707434) * 10 ^ 70 + 9644221385633460108023223385650865544364723728702340465347055442979994)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_289 :
Polynomial.coeff recurrence2Scalar4Exceptional 289 = -((2399241627878615036183098833660284521 * 10 ^ 70 + 6876103020310320568913844756216699179837028888146196839070584356220132) * 10 ^ 70 + 216091137997701077084366009290518349644792279858275356338185571710221)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_290 :
Polynomial.coeff recurrence2Scalar4Exceptional 290 = (3097983821735091685776910435531178370 * 10 ^ 70 + 3874840347441255710461053249862010888525563930351700133683149150933725) * 10 ^ 70 + 9791475050823348616345642078237454283573709610231278797326914007200893
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_291 :
Polynomial.coeff recurrence2Scalar4Exceptional 291 = -((1287053590092959492894595571832944824 * 10 ^ 70 + 4991342595026275655868130956972529136301761880773344845141942607462772) * 10 ^ 70 + 1571670126488948187300132980228020930482332648684866739415708146890224)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_292 :
Polynomial.coeff recurrence2Scalar4Exceptional 292 = (333063619524255994739629858052331440 * 10 ^ 70 + 3486904581208771865142224886621275507533317270510671290234329250786692) * 10 ^ 70 + 9899686033579492418789444397656298294621922121172391636398661410472309
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_293 :
Polynomial.coeff recurrence2Scalar4Exceptional 293 = -((43964221280592098368831906383469542 * 10 ^ 70 + 3737381531369365613099301426589108056815216509729270476933643594695748) * 10 ^ 70 + 7613280268503084366829623982019173479277115651270186874439875960408879)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_294 :
Polynomial.coeff recurrence2Scalar4Exceptional 294 = -((7043454770392603905586580971329736 * 10 ^ 70 + 9316869830387571866278466652991647549685692264873055934987052600297596) * 10 ^ 70 + 4756855170692682077212331663478410103045761299752764820326334500150784)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_295 :
Polynomial.coeff recurrence2Scalar4Exceptional 295 = (6266765281649131219079280429129283 * 10 ^ 70 + 4038570785481171051737136565898710936532496757621377106789442198255668) * 10 ^ 70 + 2725628190848368375701233119079623780365069530057494600918363595324738