Recurrence 2 lookup certificate: Scalar3Left 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.recurrence2Scalar3Left_coeff_231 :
Polynomial.coeff recurrence2Scalar3Left 231 = -(((52 * 10 ^ 70 + 3307294590224637726469939535905215966024728697646989306878496466786569) * 10 ^ 70 + 6801661045057985624241384651086925953431363533781807628225448770170391) * 10 ^ 70 + 5913953827477468683414166731100760661151388022846088909433955623663283)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_232 :
Polynomial.coeff recurrence2Scalar3Left 232 = ((58 * 10 ^ 70 + 2439685527853146871987570210262038098723468007628135622867983545687469) * 10 ^ 70 + 9731366228616737739863252886594347011700435068294784777051299188628831) * 10 ^ 70 + 8444116782817859650431256433599139294378268263158249245857655324597523
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_233 :
Polynomial.coeff recurrence2Scalar3Left 233 = -(((61 * 10 ^ 70 + 3342503985688099056481349145325310680590436067075362480076772567817475) * 10 ^ 70 + 5328313300334459900030265532278185328598134809169734063807943633260077) * 10 ^ 70 + 2183787771184203674847007580350239640356183483703567333909676549580670)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_234 :
Polynomial.coeff recurrence2Scalar3Left 234 = ((60 * 10 ^ 70 + 9210078598462623644726030842238560581833786978084735579318634120761600) * 10 ^ 70 + 5304481977764210391628460198838294507284346986863533741083438880742013) * 10 ^ 70 + 6417883168829183259122672806323122402924840642873925695099967947880722
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_235 :
Polynomial.coeff recurrence2Scalar3Left 235 = -(((56 * 10 ^ 70 + 7220378302969032929138827322251785243311219979650550591836667890104078) * 10 ^ 70 + 6856897991958921730260467555770905850940158888767399039127600185532989) * 10 ^ 70 + 9109865715439198978351489618071378237542573598880642861220161325129060)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_236 :
Polynomial.coeff recurrence2Scalar3Left 236 = ((48 * 10 ^ 70 + 9341740730935124680372952834478886972480011464200199233274018509922437) * 10 ^ 70 + 3804307456721755186943838267518180994777881800637697153662941722753276) * 10 ^ 70 + 4365486156608062957357971111860729535853902012997788128791989653260912
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_237 :
Polynomial.coeff recurrence2Scalar3Left 237 = -(((38 * 10 ^ 70 + 2278672562203674712231612683394535578538226480104674377998307833291235) * 10 ^ 70 + 3506713276252642670672012611972684077093239648807142243974786614682945) * 10 ^ 70 + 9454636245722957149802997589352970451096451267418822068632909961743606)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_238 :
Polynomial.coeff recurrence2Scalar3Left 238 = ((25 * 10 ^ 70 + 6527339209691939058362984095102081098943356256248201366113169892401074) * 10 ^ 70 + 8401681238434150234593779602769039792026353891288776422232599912504827) * 10 ^ 70 + 8612002397420692479351372438741384805955844002342558940563657968472885
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_239 :
Polynomial.coeff recurrence2Scalar3Left 239 = -(((12 * 10 ^ 70 + 4724501696903166842305281980062933189474940586857558732975209880218952) * 10 ^ 70 + 4222472749892890455497614528524094298572315944210519716552509742501815) * 10 ^ 70 + 3845139091123248725621090683859789626864308359257195692237701164518241)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_240 :
Polynomial.coeff recurrence2Scalar3Left 240 = -((358658854613162523157264471298356650515850480150773849279538949657801 * 10 ^ 70 + 1783821175267136663786435341871992802687732435100437203385301467982292) * 10 ^ 70 + 3004224108768396683717575662673785170515120889383657997074472742430619)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_241 :
Polynomial.coeff recurrence2Scalar3Left 241 = ((10 * 10 ^ 70 + 7751925636671474921431943217015528575488001341785685531503107187723312) * 10 ^ 70 + 350729078836372551958677163258873935084285386873579578116146396555520) * 10 ^ 70 + 5029717250768904405467820597417824186650820542990968468506729821190497
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_242 :
Polynomial.coeff recurrence2Scalar3Left 242 = -(((18 * 10 ^ 70 + 9761902475909299374942994667337010187999092934404244228449285828399007) * 10 ^ 70 + 7099797204695535831042548740897762000231264434938590964681607199649422) * 10 ^ 70 + 83643656443108939203620974240506797416093079477640497597202100424345)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_243 :
Polynomial.coeff recurrence2Scalar3Left 243 = ((24 * 10 ^ 70 + 2732339306811437443942577880664829615763573465710937371345775502302575) * 10 ^ 70 + 5232031634635677701550112052869869228168906945726037394788573835654573) * 10 ^ 70 + 1489900534090276718428793210492992382682698990460093618229869121182918
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_244 :
Polynomial.coeff recurrence2Scalar3Left 244 = -(((26 * 10 ^ 70 + 7017735266444510350008053614977771372367625437082928811735551823328720) * 10 ^ 70 + 6688682453658227573544458270286651858658301382371278696751241359048961) * 10 ^ 70 + 7787952353844628695778490152677343644201222204364055105908283685135224)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_245 :
Polynomial.coeff recurrence2Scalar3Left 245 = ((26 * 10 ^ 70 + 6280942157306404677801914743278109473342509197292425579487288248238291) * 10 ^ 70 + 759799550168363924864997702341999050948359641716577668200814487349965) * 10 ^ 70 + 5474467543811015963478538393552404045831697307428097763605852549739866
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_246 :
Polynomial.coeff recurrence2Scalar3Left 246 = -(((24 * 10 ^ 70 + 6356447144909669967489343596972667537592042794713320734582380310040042) * 10 ^ 70 + 1205966422830279823976248238278889294881771145657142855224767840136623) * 10 ^ 70 + 6495672258128294748009027089280717828621378666042374204482372135267982)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_247 :
Polynomial.coeff recurrence2Scalar3Left 247 = ((21 * 10 ^ 70 + 3973913078574132516728811487484817126468113456708070007317214524310142) * 10 ^ 70 + 5233251793057729031943183082552536708638960959288204944988929224590545) * 10 ^ 70 + 5008467472245951389844258135582224116872543710677589883594291836541475
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_248 :
Polynomial.coeff recurrence2Scalar3Left 248 = -(((17 * 10 ^ 70 + 5610555939844127385313001183256040978791683192085506463572693782105049) * 10 ^ 70 + 1014981829668440268994945486015326450396035482606275044451546143656423) * 10 ^ 70 + 6444927387299453761227723012834267135934616711791726023441653703083930)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_249 :
Polynomial.coeff recurrence2Scalar3Left 249 = ((13 * 10 ^ 70 + 6657405714272086001890840074952452582158899715941822632392484429921069) * 10 ^ 70 + 3644732575531614673659958655723773728940714898811054813172634253954996) * 10 ^ 70 + 2287001407289747816642758229517460905695624054123665268393433247675788
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_250 :
Polynomial.coeff recurrence2Scalar3Left 250 = -(((10 * 10 ^ 70 + 976519610260615881381228770394193062376051378170735115230464629388174) * 10 ^ 70 + 7803147253890100546540248603775250400568628008045451028173280822091271) * 10 ^ 70 + 9675661557438553068816122012031589333930358923741271743642126961606910)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_252 :
Polynomial.coeff recurrence2Scalar3Left 252 = -(((4 * 10 ^ 70 + 7064330030864667840654210880620003199527745255535279556304443790719844) * 10 ^ 70 + 2626239969163920696541612217146235083776018105040815240408552045692100) * 10 ^ 70 + 7117517360069925642712877353580669611626982585129978277155818444408793)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_253 :
Polynomial.coeff recurrence2Scalar3Left 253 = ((2 * 10 ^ 70 + 9504127449065212005863775517408256063686640292466151195607380673435798) * 10 ^ 70 + 6057027915727387407742109136578936967921871339479432078193562934669753) * 10 ^ 70 + 1909710273887443003626184993635322077268509301294704648902717069544531
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_254 :
Polynomial.coeff recurrence2Scalar3Left 254 = -(((1 * 10 ^ 70 + 7316113825936944794834576800170689165339288802633134359791718254171654) * 10 ^ 70 + 7325547678523425435537486504129917054467434893290611294240118157739156) * 10 ^ 70 + 125855243859041536489330906855484404957260849763177859335418313860763)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_255 :
Polynomial.coeff recurrence2Scalar3Left 255 = (9382998580330406048874585980947761618995082404601324956656685803328829 * 10 ^ 70 + 3667058933421616834474654177107103120872556282311671764438912292678990) * 10 ^ 70 + 8755280446716500136307060571545588602155208166534511662014076787918777
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_256 :
Polynomial.coeff recurrence2Scalar3Left 256 = -((4565558877704757640279600222181251371855278981007566658239664145431539 * 10 ^ 70 + 3637871265918681474699513839249420173698344161908301734054798476823327) * 10 ^ 70 + 2240718194669118653633159014067339172598694598024102239870356200048470)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_257 :
Polynomial.coeff recurrence2Scalar3Left 257 = (1865828208219117414086264243074346599251623663106366567118376213886914 * 10 ^ 70 + 2624307704532595015334505523737487421344413741746921720038224871287868) * 10 ^ 70 + 8031067824967304779801326463634149885229280161226920764301986022402856
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_258 :
Polynomial.coeff recurrence2Scalar3Left 258 = -((500338021947770986118957689578082895846876034919429954120098407922560 * 10 ^ 70 + 6938679634664386335651633039281734432671155073115083462464620261216636) * 10 ^ 70 + 1977844725728289046388842761928408579950008667166486561194208442037510)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_259 :
Polynomial.coeff recurrence2Scalar3Left 259 = -((91715127596241827666363803183239480020642448898580386096253238180977 * 10 ^ 70 + 998493419989971729203916020118412346177697426114939607545577354669397) * 10 ^ 70 + 2468745904052643928098376891707734953291051303672083681512060808147689)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_260 :
Polynomial.coeff recurrence2Scalar3Left 260 = (278416012482570794949026521983751479871563526377150622580994078227593 * 10 ^ 70 + 585247824951365055487592189794986116269952641444438257999745208184245) * 10 ^ 70 + 2189461637327888502705076799521254888236628920218880872569564824633207
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_261 :
Polynomial.coeff recurrence2Scalar3Left 261 = -((280705031369114290325144767531382218896969148672509681736104089253880 * 10 ^ 70 + 951943758025959621172136063965599922295418831566975787316143677164281) * 10 ^ 70 + 2946014762474669370806691604160949950745911702340235190844479183785242)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_262 :
Polynomial.coeff recurrence2Scalar3Left 262 = (218323356709107944100979182490561428915069950227854706301183439732884 * 10 ^ 70 + 1823193475140789746767519022114898072340999738704470422055187461592714) * 10 ^ 70 + 6923229051763716919750683914079935386378636605533232176653077831907012
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_263 :
Polynomial.coeff recurrence2Scalar3Left 263 = -((147995871818770195775904225622408278909991502560643062893087933760903 * 10 ^ 70 + 5940232785935319204663401393673560801182418023564578844742137618120928) * 10 ^ 70 + 83874517743116435605301771990951918925522257018388799734813214994194)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_264 :
Polynomial.coeff recurrence2Scalar3Left 264 = (91173615522995442375570957773107962198771487657681000251096506219699 * 10 ^ 70 + 452795759825068009698773375094752349682356171551029864717077894396332) * 10 ^ 70 + 311981054454795084915746896693946399446160837759113910595743058855923
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_265 :
Polynomial.coeff recurrence2Scalar3Left 265 = -((52003487373293001917256631809969605609096949747995515889829497290089 * 10 ^ 70 + 6493468540759676513147190852734845120136424151994488812665504985960100) * 10 ^ 70 + 5309839055874545779996352593357823115501290633449356150032125732046772)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_266 :
Polynomial.coeff recurrence2Scalar3Left 266 = (27710225544067522337353721031357881933980906810797697645776569956533 * 10 ^ 70 + 9757719246967776067068982266340284330090026011904385769053189579612939) * 10 ^ 70 + 9126192653200893473847427200913289826493447092668208430625843830187302
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_267 :
Polynomial.coeff recurrence2Scalar3Left 267 = -((13847897595751534767262578053409213830311911159651985237672587048768 * 10 ^ 70 + 6756165425298759586769172421519182394153282959319069970812734948327543) * 10 ^ 70 + 6335804176696235860197031961355565029184469446751343850406897674781924)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_268 :
Polynomial.coeff recurrence2Scalar3Left 268 = (6493091843359742030351799670058321161313357633153862704748727655331 * 10 ^ 70 + 50762799192706078535979294685399859568352139432109703800231201224495) * 10 ^ 70 + 9777396321974000919350638194861107960296479663914937920184412685870523
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_269 :
Polynomial.coeff recurrence2Scalar3Left 269 = -((2848713551984997400163898842612746549953829687226276413264007528086 * 10 ^ 70 + 5512146365117861663918590700320265928505307533605288280404157175775278) * 10 ^ 70 + 7022132712353367496029329204454738766280998797942756042245486289010065)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_270 :
Polynomial.coeff recurrence2Scalar3Left 270 = (1161556363288517828561868293829292035560134840528808671444610802837 * 10 ^ 70 + 1915817169728147967518496928567549277189433649614202500700964463168038) * 10 ^ 70 + 919697329836270961232297152582247867666460480471226795009251181133351