Recurrence 5 lookup certificate: B1A3 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.recurrence5B1A3_coeff_0 : Polynomial.coeff recurrence5B1A3 0 = 0

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_1 : Polynomial.coeff recurrence5B1A3 1 = -(5504 * 10 ^ 70 + 2264712803397541033003458089436964882284165860489944173288987361806592)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_2 : Polynomial.coeff recurrence5B1A3 2 = 42587536 * 10 ^ 70 + 9717172543884304050105072712305572161662063535986125885125197180414464

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_3 : Polynomial.coeff recurrence5B1A3 3 = -(155597302421 * 10 ^ 70 + 9506376789139276916854255998721742107056781414768369641482575007053024)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_4 : Polynomial.coeff recurrence5B1A3 4 = 331520747768196 * 10 ^ 70 + 560435891357521163071968719694820283206375355165058162043805943220860

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_5 : Polynomial.coeff recurrence5B1A3 5 = -(442909232982487068 * 10 ^ 70 + 3276642647535733631244200323290489776628411762208509589335103585221116)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_6 : Polynomial.coeff recurrence5B1A3 6 = 373523606780616448100 * 10 ^ 70 + 1703526790267805245915224613166719023551519244947507191463843200645712

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_7 : Polynomial.coeff recurrence5B1A3 7 = -(186062682881037853348858 * 10 ^ 70 + 9692860735328781931750729747469270378563278558282116000271972216462996)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_8 : Polynomial.coeff recurrence5B1A3 8 = 35568261704251459638146205 * 10 ^ 70 + 3414162109490828180555778516116628790963337922140842852137079405843120

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_9 : Polynomial.coeff recurrence5B1A3 9 = 19720215329700880686020606553 * 10 ^ 70 + 1311900948379669333109150781517399831585317585094175419491050751285712

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_10 : Polynomial.coeff recurrence5B1A3 10 = -(21807665312708647818933873513819 * 10 ^ 70 + 9064980614654282825193078148300609320429911644572565149089558925148244)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_11 : Polynomial.coeff recurrence5B1A3 11 = 13397327238285791792720615431283036 * 10 ^ 70 + 5192060160142074420089915684524403120446657862503532450908032941842552

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_12 : Polynomial.coeff recurrence5B1A3 12 = -(7026890499389508133571852079262215386 * 10 ^ 70 + 6395711957638704698032164130424118297660806345950008801793556473732704)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_13 : Polynomial.coeff recurrence5B1A3 13 = 3051678794810780394670757151781004951260 * 10 ^ 70 + 6177132742472185422124561194643765414023226883343022868844232975733586

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_14 : Polynomial.coeff recurrence5B1A3 14 = -(913629117653031457920892933854537841370928 * 10 ^ 70 + 9799972441780754981553900743966253658812566835255004781658504374135141)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_15 : Polynomial.coeff recurrence5B1A3 15 = 90113132271343575564151581017215151227024393 * 10 ^ 70 + 9974214297326757312354746881180521288253415981736592852841302850992283

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_16 : Polynomial.coeff recurrence5B1A3 16 = 79296442504860765757875098152158354577401501997 * 10 ^ 70 + 9257030632327784597145981142048778049264570401275320690644183353212834

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_17 : Polynomial.coeff recurrence5B1A3 17 = -(57174583600568932917900047365970509436867034780231 * 10 ^ 70 + 7690647831338248048057452812877715491013093911973058665830546760481555)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_18 : Polynomial.coeff recurrence5B1A3 18 = 22745180860381834975334399883176158271412383258501185 * 10 ^ 70 + 9649587252191870223956119734040074822618921055048194768599419555039090

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_19 : Polynomial.coeff recurrence5B1A3 19 = -(6612668281231003742890401923774762585581282688889507184 * 10 ^ 70 + 2132059846336571793170667581476810237183449321411853925762192090896864)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_20 : Polynomial.coeff recurrence5B1A3 20 = 1517101879717945486323687980503866963333602428813848351145 * 10 ^ 70 + 838648397966087717607586506754390582069882402845805118210659640498965

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_21 : Polynomial.coeff recurrence5B1A3 21 = -(283459615979962867235846171323412744722389705896749985422140 * 10 ^ 70 + 4546604156909290961401958063029124092169513119563464717020657635446788)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_22 : Polynomial.coeff recurrence5B1A3 22 = 43656254805453668633209244995725026297268929733243525731289542 * 10 ^ 70 + 9114451196822688016375029487734830615103907185600640318374820718701421

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_23 : Polynomial.coeff recurrence5B1A3 23 = -(5524739770779271337861245860344083419891081750400733533718375423 * 10 ^ 70 + 4618259412901261055607666332805502021940404013574427626895784158079348)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_24 : Polynomial.coeff recurrence5B1A3 24 = 559531488118453934170363029714965625989411413846845198674278909195 * 10 ^ 70 + 5649578498106164167550774065484722032350155107033254956899971133661734

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_25 : Polynomial.coeff recurrence5B1A3 25 = -(41389535787512810699411523601647996590729443727385909042543014864071 * 10 ^ 70 + 2778720411680595580816092620657999099038706656756199591804571846467280)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_26 : Polynomial.coeff recurrence5B1A3 26 = 1338439888377084003734328248014010044538116661384686245700894395095949 * 10 ^ 70 + 8612720909242449532739396681737316879889362616103946113609054722256704

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_27 : Polynomial.coeff recurrence5B1A3 27 = (20 * 10 ^ 70 + 715676449913136827486570793727574528710417768474869641265472349456124) * 10 ^ 70 + 1858545408737909931659557148316583760714815934447543902635080413493703

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_28 : Polynomial.coeff recurrence5B1A3 28 = -((4867 * 10 ^ 70 + 4307296749701995182339763930520029901812319220321442856722551449177669) * 10 ^ 70 + 9819974307582529916199945806679640149076620526432823140775390604832787)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_29 : Polynomial.coeff recurrence5B1A3 29 = (648563 * 10 ^ 70 + 2779339646927126249512755108034915973366883844411848656189238923644831) * 10 ^ 70 + 2821710194140080963786326435625310924223049362962790668534083046496153

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_30 : Polynomial.coeff recurrence5B1A3 30 = -((66747710 * 10 ^ 70 + 6760466004153520045846442454243807735401006413557533036691691634206468) * 10 ^ 70 + 5250282282268531719148728136916834608796255074733551696699721890201009)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_31 : Polynomial.coeff recurrence5B1A3 31 = (5767318273 * 10 ^ 70 + 4018887367803687515720746233034291555829725225091394032783707239996023) * 10 ^ 70 + 792069205146453242041862232875653534396633411249573422884520723296192

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_32 : Polynomial.coeff recurrence5B1A3 32 = -((433283354643 * 10 ^ 70 + 5095865597082619219796197448495672839467716594335609546138806892383248) * 10 ^ 70 + 3811883772834029476451746700960714074404391476045204265446978366954758)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_33 : Polynomial.coeff recurrence5B1A3 33 = (28839709055210 * 10 ^ 70 + 6747836875581697921306593509587042861654491548279374058863069915513559) * 10 ^ 70 + 2016153275711473972933689599358698155947488439177352527000645014863990

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_34 : Polynomial.coeff recurrence5B1A3 34 = -((1720687824965896 * 10 ^ 70 + 2285541305156360545258487275373162063869067908339693217429388358962774) * 10 ^ 70 + 4857732806382757320311624034709210647041678326615130343192192441548502)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_35 : Polynomial.coeff recurrence5B1A3 35 = (92763348223776605 * 10 ^ 70 + 7217281807704224946432025752958178612071798419452295353348935878465676) * 10 ^ 70 + 4111873936381900154847648905735376819825612612908009365812867246396161

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_36 : Polynomial.coeff recurrence5B1A3 36 = -((4545140493345419681 * 10 ^ 70 + 3080090266980233282878426531021931184198613603158504985301340699765514) * 10 ^ 70 + 6231145103527094494648077206164745835963621859058716965252109145289811)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_37 : Polynomial.coeff recurrence5B1A3 37 = (203301956987773374884 * 10 ^ 70 + 5554033547741024952688395245576590327649784741423451882819991991784944) * 10 ^ 70 + 7691368500011493390983043166193160919633287407917130584932749588349165

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_38 : Polynomial.coeff recurrence5B1A3 38 = -((8330200867065412166885 * 10 ^ 70 + 9886418932565125788764772111373438534091644847420897381444555540037022) * 10 ^ 70 + 9632577921409223877406432781763743382378789921234030606039412903944803)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_39 : Polynomial.coeff recurrence5B1A3 39 = (313509026112289852303728 * 10 ^ 70 + 9246474025295439551235627795993080523230550836222418226871404002778228) * 10 ^ 70 + 4390085032481745384272054933597305067690820947605076396204897836142682

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_40 : Polynomial.coeff recurrence5B1A3 40 = -((10859186785124759129556887 * 10 ^ 70 + 1154954322192855294009603888777673177027206740628649279087760365611696) * 10 ^ 70 + 8328914477156660804392325392307996427222436635534067030634225360085421)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_41 : Polynomial.coeff recurrence5B1A3 41 = (346649924777258686237655481 * 10 ^ 70 + 5621077902103465810976705719844599610215798516875776752144922195242402) * 10 ^ 70 + 436646287284878260330809666392841668291015203761186754094070458548639

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_42 : Polynomial.coeff recurrence5B1A3 42 = -((10205271417499961464491703591 * 10 ^ 70 + 4507917696680338254158803662074449504976077219249069293332548925488591) * 10 ^ 70 + 6233412826982220757622654255785384383597078526272439355712857646096840)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_43 : Polynomial.coeff recurrence5B1A3 43 = (277029323099026165645163944858 * 10 ^ 70 + 7520707075069548152080873436876611762430283456230612554291232008686202) * 10 ^ 70 + 6767575060194601333432170968912087632461496495100795021304946646507770

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_44 : Polynomial.coeff recurrence5B1A3 44 = -((6925147251046618592909127668802 * 10 ^ 70 + 6155239388076350898663489294778267762060209545338853124507345770661853) * 10 ^ 70 + 2631042512500342128208186802380992078283152249810642678958472964537294)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_45 : Polynomial.coeff recurrence5B1A3 45 = (158938518652354295836553445662152 * 10 ^ 70 + 6811535042296264700507311866587320704000195550258419937282889856305118) * 10 ^ 70 + 9381168914283409761828520751766934614437423778218724537525588003987955

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_46 : Polynomial.coeff recurrence5B1A3 46 = -((3329619461878612067717366420623354 * 10 ^ 70 + 1332816833236972730982207265862267732306532984703730003142664968013095) * 10 ^ 70 + 4623291132435262695049015512237679501109781183080969971713041358630728)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_47 : Polynomial.coeff recurrence5B1A3 47 = (62967483793365217072507207403237399 * 10 ^ 70 + 5746688910301789155088145922050187531068160944215261414584357673067551) * 10 ^ 70 + 8066457052133577866435281457677350685672493504549577610770866072270134

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_48 : Polynomial.coeff recurrence5B1A3 48 = -((1051232663077559498133754774938291193 * 10 ^ 70 + 970552575828536309694099103839602382443233505514494948161877204677143) * 10 ^ 70 + 1024774818218297108056557845900580169458551353258164235219810296929222)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_49 : Polynomial.coeff recurrence5B1A3 49 = (14704487461541183949551623518601285951 * 10 ^ 70 + 8815415777506161048639521285334843441572862070325678044982655245658951) * 10 ^ 70 + 297895245746974421523802550576938244352366739238056121461671689353071

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_50 : Polynomial.coeff recurrence5B1A3 50 = -((145266485616576043451501025797823912955 * 10 ^ 70 + 1772226278008159257578642124947739616866819627875259900499860720899410) * 10 ^ 70 + 2562628597377393344446781392866899225736240398680542596760633107209141)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_51 : Polynomial.coeff recurrence5B1A3 51 = -((25590276165410337253251703737672495807 * 10 ^ 70 + 5605328535841468341954152400837571737138281451757328948622514690325876) * 10 ^ 70 + 4654742376076052325962489650214653378001307144597938024931911747951869)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_52 : Polynomial.coeff recurrence5B1A3 52 = (49412119761019514011879658509972026347547 * 10 ^ 70 + 1667084387722067227916105573022584795962088968507691511030444451091090) * 10 ^ 70 + 6677924651048948028595996347370601207743587482319121089365286392644215

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_53 : Polynomial.coeff recurrence5B1A3 53 = -((1658586425651782179407004336694245168880389 * 10 ^ 70 + 1376572797712700710062410606049939367779320260180511454283006116487893) * 10 ^ 70 + 596408658639716923211094875986477829557144175026382234983102834984472)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_54 : Polynomial.coeff recurrence5B1A3 54 = (39758350760236533502883235319342055300264303 * 10 ^ 70 + 5354783606521914966933662614003984427827410338504218683561019853907716) * 10 ^ 70 + 5394535893584328825892942779830235371846826934708527966538060554004630

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_55 : Polynomial.coeff recurrence5B1A3 55 = -((805686006775677924082307149486258197986047357 * 10 ^ 70 + 2633052201546974903231203665351577185752468145736640909758540977108689) * 10 ^ 70 + 8468521109350030262463400048647319746110997484724831845177546552750305)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_56 : Polynomial.coeff recurrence5B1A3 56 = (14565617092253083013610840595092968272624372833 * 10 ^ 70 + 8024587304081405810800798776469601975165838253428692700736925910220380) * 10 ^ 70 + 7720113332768925292668598935715226744817907535162948522279389985975482

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_57 : Polynomial.coeff recurrence5B1A3 57 = -((240761761715156970261920647565496384643482856923 * 10 ^ 70 + 2607179411432535002343210912599305897568118157898626320724231471256432) * 10 ^ 70 + 9092921227760398525790377355490317712336304396327020856960216776704552)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_58 : Polynomial.coeff recurrence5B1A3 58 = (3688307813884143041768442485738630135008182165557 * 10 ^ 70 + 7896534737161346481110444924649325681775572380214372923446096123032438) * 10 ^ 70 + 9324902346976159289707424624715291329511300639165159482258336601717840

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_59 : Polynomial.coeff recurrence5B1A3 59 = -((52810091297871420103671092563739478889532702885378 * 10 ^ 70 + 5454940816879070789428693210390574521049125004095606606183512630707312) * 10 ^ 70 + 4282013869953384209660764932964894123928445213091297690255475108607908)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_60 : Polynomial.coeff recurrence5B1A3 60 = (710809083884556308360878487505551514402233917603331 * 10 ^ 70 + 7213940896999207791869687373290126962345619020376237637943025503790016) * 10 ^ 70 + 8998290275369659619733272884841499141139005507560205228299975079375477

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_61 : Polynomial.coeff recurrence5B1A3 61 = -((9031281747180055170180106681055861468120216962903283 * 10 ^ 70 + 2524820924319982273703085483118562244983956717895055048233222179051401) * 10 ^ 70 + 819286183903906226617399644809322891580250585303878160327675929171809)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_62 : Polynomial.coeff recurrence5B1A3 62 = (108666160713993419158882846920784180129779093457735368 * 10 ^ 70 + 7129366970283256920042046982908573565492642111853734786494750008133050) * 10 ^ 70 + 4351279161658454513550385780889324415336857576056349039680071288766619

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_63 : Polynomial.coeff recurrence5B1A3 63 = -((1241350824397694838179757329953134003047187050782137709 * 10 ^ 70 + 8171863039222089314865716574864001060911836245752151449554018302652873) * 10 ^ 70 + 2969043951004919904107543791119115913927288647006390703944745276057912)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_64 : Polynomial.coeff recurrence5B1A3 64 = (13491560636999264275441625101549264543517644517169169040 * 10 ^ 70 + 6677133122515131235912228691750148429967941888830073853422379555368464) * 10 ^ 70 + 4861565430706643875082916657529040927066614201659560202431883160916903

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_65 : Polynomial.coeff recurrence5B1A3 65 = -((139755699880462831542041368303631136783901093081214162806 * 10 ^ 70 + 5179854749810517141010783742823949768348023983711463026086922310515740) * 10 ^ 70 + 5761937467409030816165713523645421060523539352621848737135712578650838)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_66 : Polynomial.coeff recurrence5B1A3 66 = (1381926149922224789880303092613648330982299102729178428534 * 10 ^ 70 + 9173043507261081160616368364748589122514475206059647181348001285979868) * 10 ^ 70 + 9603388279212225199650171814014555419535494908296355818700499168547906

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_67 : Polynomial.coeff recurrence5B1A3 67 = -((13061614346368689944522003835169021456512824192822951334087 * 10 ^ 70 + 1476421537189174396860449461065767256711326407960109483193757456459796) * 10 ^ 70 + 3503959553764357397744206443474965215430455173871911935805721797009247)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_68 : Polynomial.coeff recurrence5B1A3 68 = (118149514184016967559662129526559916943727332219987332670365 * 10 ^ 70 + 5172456971223463621882478643466486777165312650432860158412122089537010) * 10 ^ 70 + 1779600556746566019476933317027127606981039188588749079460444377343995

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_69 : Polynomial.coeff recurrence5B1A3 69 = -((1023920726036051761081083196226781423310747300817562261775897 * 10 ^ 70 + 2619653827911420025708902752319842163541038953984559831638330665705809) * 10 ^ 70 + 6704573555566107964823244004090433175529124631968904732946652056567081)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_70 : Polynomial.coeff recurrence5B1A3 70 = (8510111299988950968996846790225208628703073360965327996587064 * 10 ^ 70 + 6324337587570214737233695183365741956687020535483234365905967775349268) * 10 ^ 70 + 6959583362382884356274916365072130870220846450210733415526150855242194

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_71 : Polynomial.coeff recurrence5B1A3 71 = -((67895282988001361662598924853344159317338747224704737867907018 * 10 ^ 70 + 4039470515455417071705656785473014809614099535992318640981833299498705) * 10 ^ 70 + 291838208354688582107270324121273518020151346568714217391622775777648)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_72 : Polynomial.coeff recurrence5B1A3 72 = (520416784247082673079246353090252076972789055644058130822742951 * 10 ^ 70 + 651769350653670897516670693566757796580430205958404471244541194948292) * 10 ^ 70 + 7464242427386623289452495591611684123878075851033166591081378433328271

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_73 : Polynomial.coeff recurrence5B1A3 73 = -((3835457215825383973500190627253167853282474702202057458110983059 * 10 ^ 70 + 8311735216199081796105933653824348935845255949390175657933306335230297) * 10 ^ 70 + 1716626777314794765110558909504896720840994663099270181625441975914763)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_74 : Polynomial.coeff recurrence5B1A3 74 = (27199573794884910455943445629575598028547126483942916103248213689 * 10 ^ 70 + 2996730556185195036402146217902340148075759434011795943288771197429774) * 10 ^ 70 + 7547142535658784641627069508272063337586621527079806453916896496731248

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_75 : Polynomial.coeff recurrence5B1A3 75 = -((185734155797373117251154624504166070014986209511354648704693579503 * 10 ^ 70 + 7559105655789285836346565675349426920003995007313370043099072871688229) * 10 ^ 70 + 7457028213123846567154198932011119251740983822566801649156152850704594)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_76 : Polynomial.coeff recurrence5B1A3 76 = (1222065535932334196587677370288369101289988600754108878941306985709 * 10 ^ 70 + 8932729895336690466251717003063987906778910243752931352018523116553757) * 10 ^ 70 + 9247547234558539975119017269698150656768027780739356775249751488159669

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_77 : Polynomial.coeff recurrence5B1A3 77 = -((7752521327391588269116738652845569235582885296132586334109983867860 * 10 ^ 70 + 9439308248652537355670386341405818371247848886372376412630212626991296) * 10 ^ 70 + 2260470482732104832943146598233185195283088590609154970528682527387999)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_78 : Polynomial.coeff recurrence5B1A3 78 = (47445571520795835526052831836557061612949690069159703130352907344117 * 10 ^ 70 + 81042553540686964064820082754049728624422585550287559994045634663398) * 10 ^ 70 + 6291143867482499213307296323404557469081484307289402776630875412407884

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_79 : Polynomial.coeff recurrence5B1A3 79 = -((280283841917197880072020681889261902666978070498150830887185506238848 * 10 ^ 70 + 8258822935789505910514366451079472949139352162593596705784958837344937) * 10 ^ 70 + 1444858768707278201719598081746704391882162128722845191147155551401724)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_80 : Polynomial.coeff recurrence5B1A3 80 = (1599128851971047963663856421959878776384936057227016342084774291815304 * 10 ^ 70 + 3935063545903602004082439318406609666680141366936191400164453151000876) * 10 ^ 70 + 9363868594525664168529314684322370225526383425478195444015420329501897

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_81 : Polynomial.coeff recurrence5B1A3 81 = -((8816048898462384899440668719012178641337641222814598566474647630282285 * 10 ^ 70 + 9906812967162217235982787850186809313945379618196219740587652179779275) * 10 ^ 70 + 8935335798963430115707807378017406950917182491977747688535111951175236)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_82 : Polynomial.coeff recurrence5B1A3 82 = ((4 * 10 ^ 70 + 6987383694659164011425179702072539063408888821054696407640293140550444) * 10 ^ 70 + 6984814021048228036860531506552744256602016857486791288427901719944118) * 10 ^ 70 + 3857002775086997620630039629400228790669403417322916945712683112449469

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_83 : Polynomial.coeff recurrence5B1A3 83 = -(((24 * 10 ^ 70 + 2218333843011086850365449861829619722990424827734014502831540525455288) * 10 ^ 70 + 3277891014610787448152531531854690307455883797090824609895708516166079) * 10 ^ 70 + 9299761333833983667865403277683827031823731987638173028815504776635830)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_84 : Polynomial.coeff recurrence5B1A3 84 = ((120 * 10 ^ 70 + 8213414169395862555966203834141756764600402110577373938236812234666845) * 10 ^ 70 + 3773321401150747489763381726582583202031153507147285137130450693215459) * 10 ^ 70 + 989329893697123609439088766007307496380249462780959447698980106108934