Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_311 :
Polynomial.coeff recurrence4Scalar2Exceptional 311 = -((((12205614338639305923 * 10 ^ 70 + 9263157984038028496941756540247416068274129585577216362065293014125050) * 10 ^ 70 + 9709804469800441299146459091278011797116305678950511857273814668911036) * 10 ^ 70 + 9248031634220890416496536529718216544397097367871326879355772997595996) * 10 ^ 70 + 4946040685442353754219022803574713418349181806442890409857739020439272)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_312 :
Polynomial.coeff recurrence4Scalar2Exceptional 312 = (((7303887389422915860 * 10 ^ 70 + 5173412016446075695245571295942031813364021014550940376209365809271325) * 10 ^ 70 + 5834322833392490114035381785558742430023390832646964031267612783574054) * 10 ^ 70 + 9549910299957704843476798364325809673886270199213527433897272038555673) * 10 ^ 70 + 1473712649355889292903054746069989148253310186839133316878349933018627
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_313 :
Polynomial.coeff recurrence4Scalar2Exceptional 313 = -((((4297539274229839120 * 10 ^ 70 + 5199163627314774772682563671554108695613779828344784537341942208863419) * 10 ^ 70 + 9750201557406262982507012937607190190825255307424539327576890567003399) * 10 ^ 70 + 2901658011670592436427094098588179042863132546012521695980772248424962) * 10 ^ 70 + 790620359245002081335406865957518120233243768486736960551256349041228)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_314 :
Polynomial.coeff recurrence4Scalar2Exceptional 314 = (((2485855815843781484 * 10 ^ 70 + 7060662728144533427662250580809278992209852462079081842864906279368818) * 10 ^ 70 + 2988705278682707730509487301900337576490584251620828054256015552370922) * 10 ^ 70 + 2090751044911030701359441284014387476585516675175631934160003915040852) * 10 ^ 70 + 7896701255021777152788581489752595077594516063019917602057612304860589
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_315 :
Polynomial.coeff recurrence4Scalar2Exceptional 315 = -((((1413469118864093181 * 10 ^ 70 + 115472179311197701283890225366421132034860117815539574271732514125878) * 10 ^ 70 + 3039750387612619844314829920510707548188853131190507200354342172450340) * 10 ^ 70 + 3962084693983866584950775000186362652279794385789175146743391548666555) * 10 ^ 70 + 7569386712057841691481252870167426501869269265993185215008561756724523)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_316 :
Polynomial.coeff recurrence4Scalar2Exceptional 316 = (((790043296847210541 * 10 ^ 70 + 6770563923017820097422033248822169553036917404700020601385073926265916) * 10 ^ 70 + 8634155243073068756492097027444984833373168317065319695749696906851966) * 10 ^ 70 + 4329014052976926989978030833207617264726846957095532269285903739781215) * 10 ^ 70 + 2571391430369255015076952790688611716092489467580055321508282963041551
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_317 :
Polynomial.coeff recurrence4Scalar2Exceptional 317 = -((((434110537470814736 * 10 ^ 70 + 2229660549466921834402518647865631440992815649876889075393755549169586) * 10 ^ 70 + 2301741857967593902081804601923643580146556576154736180594922516673412) * 10 ^ 70 + 4538121915482283834028468600450590705949779550607174307260022556936506) * 10 ^ 70 + 2700216730616502528310280056247419193254689007243238937773499961546095)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_318 :
Polynomial.coeff recurrence4Scalar2Exceptional 318 = (((234527926569549222 * 10 ^ 70 + 9561461392643876893057032366921949912269672598140420824856585748174411) * 10 ^ 70 + 8792392037272316192899518452797682088547107015999056850213647891146076) * 10 ^ 70 + 9319024562358982802497655009834894589152706853351358068598980661315414) * 10 ^ 70 + 9730482022553324934171253005341557255309817462357336630803624265544692
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_319 :
Polynomial.coeff recurrence4Scalar2Exceptional 319 = -((((124601766178319961 * 10 ^ 70 + 7601366859927073658485880395632899882299890478520894367069929297565438) * 10 ^ 70 + 6574650307385295230273123788239987468559088348724294429700914644764031) * 10 ^ 70 + 1876770765514920485600010176217908457875368816332201555445145906706818) * 10 ^ 70 + 480109290952812443764703517536011682232449762658960676492965589357848)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_320 :
Polynomial.coeff recurrence4Scalar2Exceptional 320 = (((65120033737911959 * 10 ^ 70 + 3435411450474553034978794256693327454787614072836136532106948523851630) * 10 ^ 70 + 3060403467258758064249016989771766115149915527011112300954348039449512) * 10 ^ 70 + 5193682860585428613822155869564488668177333796310964734407549213607425) * 10 ^ 70 + 8125339573619501169527032907544213873645471884586377204150180527793461
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_321 :
Polynomial.coeff recurrence4Scalar2Exceptional 321 = -((((33491350289453721 * 10 ^ 70 + 3290280289521940347646438986262521536624509063644011255695795599313941) * 10 ^ 70 + 3706423426520110541784948912129235433290847342946961132498740829570823) * 10 ^ 70 + 275778358776207530270424708160595091090285903784850824445021679923849) * 10 ^ 70 + 1071594074971948928596830196430134000746040170073340816061837417106352)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_322 :
Polynomial.coeff recurrence4Scalar2Exceptional 322 = (((16958821104105162 * 10 ^ 70 + 6304996538612842044983976117589354751822783589276794632582175346632329) * 10 ^ 70 + 9244728549157779119772159125416176044909676560773854411649565753423069) * 10 ^ 70 + 739133640892474295408337708601510011289109234584447799388497002552678) * 10 ^ 70 + 4688887750931390452098492322858811978668561170039067252388512089219490
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_323 :
Polynomial.coeff recurrence4Scalar2Exceptional 323 = -((((8460238901208915 * 10 ^ 70 + 1928284025766255514136006066306112562332510445972210076014683185303149) * 10 ^ 70 + 2119258102745448278184138183031062820841709241414296176026193111208119) * 10 ^ 70 + 600521139585513445661260884126204669140457722056673611927942617366391) * 10 ^ 70 + 9853256210002822800213983348580553735206753281292639651226943972093340)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_324 :
Polynomial.coeff recurrence4Scalar2Exceptional 324 = (((4161471685827704 * 10 ^ 70 + 3325174223401048844717064117982312653245212620231525671176784232552314) * 10 ^ 70 + 8166190985064499922017730158574888569808248380681356468010747940079946) * 10 ^ 70 + 9616802051157211852887036914605926528380477166085561345506206638129406) * 10 ^ 70 + 8848632508827663453085078393890295060892629243631101567064721580369777
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_325 :
Polynomial.coeff recurrence4Scalar2Exceptional 325 = -((((2020363340272073 * 10 ^ 70 + 1294339587758342754181221935390112364372508984826094923715960693394760) * 10 ^ 70 + 940043331319554918640642035498496123847674215891300641552895397114251) * 10 ^ 70 + 8169987691894823656385989569185568968691925699810485499877122111386415) * 10 ^ 70 + 3381874343040840157847958753104166096738580618543837279387323366454221)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_326 :
Polynomial.coeff recurrence4Scalar2Exceptional 326 = (((969326489131009 * 10 ^ 70 + 4740336851102616760609584837577368049151764148141878497119144552448707) * 10 ^ 70 + 6439457167487519436988100621064654790195084787312986951710715435300318) * 10 ^ 70 + 647649467074110644841913540375190204511807954492231938016430950632927) * 10 ^ 70 + 4327194983984589137274522108861424087322535380401457153783905181766160
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_327 :
Polynomial.coeff recurrence4Scalar2Exceptional 327 = -((((460271684604314 * 10 ^ 70 + 72671548630331388752675667832571174852826992417273710599354578041946) * 10 ^ 70 + 9291111005680622073532011177074862895561853489331714549815973085158308) * 10 ^ 70 + 5551313321725751071400840762005215887692198051585533087706815817685919) * 10 ^ 70 + 1897009602146036825238694215600353898712910740156229226521806431135831)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_328 :
Polynomial.coeff recurrence4Scalar2Exceptional 328 = (((216675891199227 * 10 ^ 70 + 9614893969616222902746759164077731671520306641320317907448132761209982) * 10 ^ 70 + 7009144473595498419773705790935423877736574973150438144420981103333794) * 10 ^ 70 + 1064983348231921231660411147099229197020395507877687083284111053442091) * 10 ^ 70 + 3132530988299821650512678867740701375705779282655697056537273402875594
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_329 :
Polynomial.coeff recurrence4Scalar2Exceptional 329 = -((((101319607958433 * 10 ^ 70 + 1395507907490595673950415029831466445014980834168386486095410299741233) * 10 ^ 70 + 981711033717886263872301232386022174775638356389772605689428740562600) * 10 ^ 70 + 4924406825928033659270470861190860589963315651748946083632112562624410) * 10 ^ 70 + 2196469057731015091440186317227387184281906226908386965122406963502491)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_330 :
Polynomial.coeff recurrence4Scalar2Exceptional 330 = (((47157021799540 * 10 ^ 70 + 4332609304479332601973133006584201956856536234798623101683535603901506) * 10 ^ 70 + 4269925049771093648840826130991620756867768306855834469117996001371709) * 10 ^ 70 + 5007660727142262399831623036063582630761865949148040689997210644051146) * 10 ^ 70 + 713288714567764017579548892269412640506219552630372013208101195507557
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_331 :
Polynomial.coeff recurrence4Scalar2Exceptional 331 = -((((21889842642200 * 10 ^ 70 + 6917089992365900412253093513455399119085667647580631818856223452030786) * 10 ^ 70 + 965484487031311265637810778775892563847909074601097537626030741130120) * 10 ^ 70 + 5486052951362079018613829638156077623846908540669677664427710144992985) * 10 ^ 70 + 5566487833463994311545748418951383258393223360197832478710271570088802)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_332 :
Polynomial.coeff recurrence4Scalar2Exceptional 332 = (((10152383787131 * 10 ^ 70 + 2798242749564345449375895387633360519472655025688475128979630300038147) * 10 ^ 70 + 5854086842007171082982890188992045222635668356913050788559787904726473) * 10 ^ 70 + 8828158297267963851192283666443882528573483886513161891362583452672465) * 10 ^ 70 + 5860598381545449278824939440761256720578746860163417698301211688565475
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_333 :
Polynomial.coeff recurrence4Scalar2Exceptional 333 = -((((4711233362855 * 10 ^ 70 + 3324231092541053964595947213490153024841907390247942729387639471310851) * 10 ^ 70 + 8936387506508129860413895697664472548717785516134436970387397271286604) * 10 ^ 70 + 9172849139983114018946332108640998012272984910431270238460769569175707) * 10 ^ 70 + 8516997571909825147708871475569385545613202152600562417958076480782975)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_334 :
Polynomial.coeff recurrence4Scalar2Exceptional 334 = (((2189295638957 * 10 ^ 70 + 5679738911419826110735333173248338493306993971527838625714470795850355) * 10 ^ 70 + 9262494615021498634365807081687551005597421352850498389479337186098777) * 10 ^ 70 + 7495078424683166786492474321508878101889000771686738626378290468296376) * 10 ^ 70 + 2239967393055252537923686638550524375956879755223866088538242233716877
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_335 :
Polynomial.coeff recurrence4Scalar2Exceptional 335 = -((((1018923951834 * 10 ^ 70 + 5357151514191812963845172710396892235154085283832591985366314109701650) * 10 ^ 70 + 1426883727797335814577080104410609698472401445887180068990762958510770) * 10 ^ 70 + 3065923575861378948141443879008321280013806962763956839167434291476017) * 10 ^ 70 + 9179042878624488714612603757451791735207307599934445039587098139849012)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_336 :
Polynomial.coeff recurrence4Scalar2Exceptional 336 = (((474688132673 * 10 ^ 70 + 2621611615726884455201492803820016239827065140126056115419975527682114) * 10 ^ 70 + 1254485490115068225940974348323639883571526326117055352354675224059046) * 10 ^ 70 + 4853026156157154755387799529139335369010320557063273147221996566513437) * 10 ^ 70 + 667300337154086164309360123833031104699338862232575932590841619303147
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_337 :
Polynomial.coeff recurrence4Scalar2Exceptional 337 = -((((221106886645 * 10 ^ 70 + 5598846847127347714458338779058056544469548626549520975678001161901957) * 10 ^ 70 + 8771053531381283429074237304992108118381100319422979888269889301858965) * 10 ^ 70 + 7489305784680518474385247517108927695575619419934650847415195360712520) * 10 ^ 70 + 409957227582746792545573986733097709752888678660300791717325542715917)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_338 :
Polynomial.coeff recurrence4Scalar2Exceptional 338 = (((102808666266 * 10 ^ 70 + 9600368512829938956232775493754825810689655864539366109500020271404566) * 10 ^ 70 + 6623519068076428669140127576627674356360465643951474135312997255347055) * 10 ^ 70 + 8432980134890684525868280869335456713175399563735497793608364348202372) * 10 ^ 70 + 6949098238995062638486313665123273303758347774771597377609973418121325
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_339 :
Polynomial.coeff recurrence4Scalar2Exceptional 339 = -((((47631145034 * 10 ^ 70 + 3754414000380834603402228508559967335568890607931033173799074749069438) * 10 ^ 70 + 4780148757700321032989985870586507222510378729742884122643489525197890) * 10 ^ 70 + 7554367054703431428522614184712911898848637546601930094246959693260808) * 10 ^ 70 + 8351252924443363094519139569200903107979013790600010839245858412931070)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_340 :
Polynomial.coeff recurrence4Scalar2Exceptional 340 = (((21946309630 * 10 ^ 70 + 8660072995352400154663595409005539012947278326200751596739398268263016) * 10 ^ 70 + 7298492889577800661827250956250530931957964771440716546070654305085575) * 10 ^ 70 + 2764146863079174241310275241737464435432321774292328167641987218377182) * 10 ^ 70 + 9982717379336720400721217600759465674211046496043543120714776602677259
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_341 :
Polynomial.coeff recurrence4Scalar2Exceptional 341 = -((((10038184619 * 10 ^ 70 + 4113420260211404730532085114570899836793154333522854316182906019555633) * 10 ^ 70 + 3063712634591011271062723905360999032814669834045905122417247367554923) * 10 ^ 70 + 2398315501125429346057804695328637819005130705199925910305914595367968) * 10 ^ 70 + 9399691001782294545216154852888452793656673829789924462497146975608247)