Recurrence 5 lookup certificate: Scalar1First 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.recurrence5Scalar1First_coeff_222 :
Polynomial.coeff recurrence5Scalar1First 222 = ((((1089538532 * 10 ^ 70 + 167851081060886660054849966091423516507358935180955200254828036149119) * 10 ^ 70 + 4223456665295661480342624417385491231068138871001475906904441266048049) * 10 ^ 70 + 7023862492897884608091589299586261836703488713620659512227052329797083) * 10 ^ 70 + 8781997177086395377063816935359337631001770200262879919110737447340987) * 10 ^ 70 + 1000572052031211959111002780307229202440893673535232665425536916903136
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_223 :
Polynomial.coeff recurrence5Scalar1First 223 = -(((((1179439533 * 10 ^ 70 + 1724681086922214908584558226205422876482965882615066295671701829046605) * 10 ^ 70 + 6849407877007001112601023222918087100925995864193927077799883590299492) * 10 ^ 70 + 2252102385242772944096281782704643354073653327935123858717353487973628) * 10 ^ 70 + 7471098379745615431928241392540481902481702545241800893250423077891727) * 10 ^ 70 + 611363486669175028812727539554091979157541503518026748285198659248843)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_224 :
Polynomial.coeff recurrence5Scalar1First 224 = ((((1189022805 * 10 ^ 70 + 8523026176595504607435718699091752327704691005817056416678604848590148) * 10 ^ 70 + 8120415043617467372077990473773348119826176093393879398272724848035564) * 10 ^ 70 + 1501182083190939224760456219531599664098711418130262179488981832755875) * 10 ^ 70 + 2023673786411842233844273960132417670471913278951596760531000408883312) * 10 ^ 70 + 324472436738002265112837819297957446898432378263418619326140153546117
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_225 :
Polynomial.coeff recurrence5Scalar1First 225 = -(((((1137314276 * 10 ^ 70 + 8427529145803559556931602624466078820249407940192557112201108276309549) * 10 ^ 70 + 5014576911651584707268998177999553497516836529742866285456940289660116) * 10 ^ 70 + 5821852992690273751106338245122389207375477884926373172102820377281193) * 10 ^ 70 + 9790826916509409553826039610264305832312340945162861357123904376993830) * 10 ^ 70 + 3882473306881918044979600016348663172989943000499513557545747513508239)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_226 :
Polynomial.coeff recurrence5Scalar1First 226 = ((((1042855050 * 10 ^ 70 + 6953718786136237994346108018673600694611469629540347837565815777046896) * 10 ^ 70 + 4017434132741914904649132121198745167117622611707972567877861793262883) * 10 ^ 70 + 5793886978718667541490185552866117242824113672376385178767742014349187) * 10 ^ 70 + 817896531082091106163840061405643654705470412587411206858890731401033) * 10 ^ 70 + 1803485507139238722898943697356031040869861848125660827533753754545515
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_227 :
Polynomial.coeff recurrence5Scalar1First 227 = -(((((922430370 * 10 ^ 70 + 901007018570577626597828565272814369676253604995236126852155592492485) * 10 ^ 70 + 9702889682804385024845667294672576285067961488623452045661189855722939) * 10 ^ 70 + 4005744664365749897377896091195276783572364561501320962770653971865116) * 10 ^ 70 + 5641836418745003493722004701965394017388200264675106801085076507829432) * 10 ^ 70 + 7578013538814567374908908207665069139803959039396027595213601441950854)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_228 :
Polynomial.coeff recurrence5Scalar1First 228 = ((((790226376 * 10 ^ 70 + 296735195667260379860007358758624572808814439429282485022364253352517) * 10 ^ 70 + 7190472519247800765864221261716186393031715522056929995291086589004265) * 10 ^ 70 + 5748659506031792557134429437050612071691024313783723789792843622864044) * 10 ^ 70 + 4148741828327981317546853168369049611586557183116505006134760459772199) * 10 ^ 70 + 738613836868695376760994063799294954332373897834247464550270472396038
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_229 :
Polynomial.coeff recurrence5Scalar1First 229 = -(((((657406396 * 10 ^ 70 + 3140650287027290133099911984874426802735304781181281509433700468179490) * 10 ^ 70 + 8265301714215981000619565297164388621375238242809906374708224206898190) * 10 ^ 70 + 7086884198040062870609013441352732963206450444586594406536185900430944) * 10 ^ 70 + 2355940340766209909548915307927339327081655480137420534844038973574544) * 10 ^ 70 + 6680329120010942872714465512210548380588205892223579424089431933177159)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_230 :
Polynomial.coeff recurrence5Scalar1First 230 = ((((532052606 * 10 ^ 70 + 8745997742051228552714122559370126885082971031186402334584044887951650) * 10 ^ 70 + 1773995938474975125152625814370395935519287190488301028842334162203196) * 10 ^ 70 + 321797341646362580763016840367014024586819998380343495072716301477263) * 10 ^ 70 + 7599603714631738953848461338167180070140854534331128588369658196050815) * 10 ^ 70 + 8838022343909119327827832137568978591070840468816190812444375394738935
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_231 :
Polynomial.coeff recurrence5Scalar1First 231 = -(((((419390229 * 10 ^ 70 + 9777990732994921700598185429774961233937614161353033045911179212506546) * 10 ^ 70 + 6400616896474193731368980956314965744218118475297721995686454274590886) * 10 ^ 70 + 6478498355794679408617181169680937472088556750623631341901443132562499) * 10 ^ 70 + 4977458733662421829373033605815092728237237276857821873017297016101147) * 10 ^ 70 + 474395368677021840593575147746855685491093362764995273648371839903560)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_232 :
Polynomial.coeff recurrence5Scalar1First 232 = ((((322199997 * 10 ^ 70 + 6935890580852879404964929220347422292554372883057938716589230395685739) * 10 ^ 70 + 9819768052422732575544047269496578500668713144627736541598327822951451) * 10 ^ 70 + 3955668055999566822577776234418232632295488758197365209524935710375686) * 10 ^ 70 + 4853496074665819915663242350219433584818613611406322468274917358631418) * 10 ^ 70 + 6907299479505615458912464023049275441436467391460958403185944567098637
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_233 :
Polynomial.coeff recurrence5Scalar1First 233 = -(((((241327823 * 10 ^ 70 + 5320935851613790955782905104305545454730551356624036434668205927342877) * 10 ^ 70 + 9548240879061696510297126117601638157452316813496690333323604318596904) * 10 ^ 70 + 281010656517568735683278365421060725992907993650760648591846153138611) * 10 ^ 70 + 3924558576240362309966854172414204554205731488233756573880061457263532) * 10 ^ 70 + 6407349142679302136534560411669627686434027210446463992752315183131866)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_234 :
Polynomial.coeff recurrence5Scalar1First 234 = ((((176214321 * 10 ^ 70 + 6459835288093272337936892497876193197322385054335381384860853434252968) * 10 ^ 70 + 7149938384949448736263473261912087532763510882563673725637355172423414) * 10 ^ 70 + 7818392160494688442809085405124115501547297317571874146163532487388309) * 10 ^ 70 + 4728105697507794329462267401564139889983073938901076878431530814796030) * 10 ^ 70 + 6249459528373757352688732135862424477530702876642554051053692459835835
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_235 :
Polynomial.coeff recurrence5Scalar1First 235 = -(((((125386330 * 10 ^ 70 + 6682749910271792672592342077463520835085965781666516525948495683702882) * 10 ^ 70 + 2651560079933424267781994837775070443083015066580326220360995408805966) * 10 ^ 70 + 9556262392423629262209076902481554283880927350608292130225903827633012) * 10 ^ 70 + 4122129636719533593102105079028959687051386477645271607027174790503993) * 10 ^ 70 + 3187830780235106637462270665434524117027036193145745470729903904347545)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_236 :
Polynomial.coeff recurrence5Scalar1First 236 = ((((86873672 * 10 ^ 70 + 8521413071205469062148845141046122514972416148006776011415947375679183) * 10 ^ 70 + 2814413129627157623483460871073948304879944463977126748262388343218376) * 10 ^ 70 + 3146707271864264253817876400624819179607316405704873542510817524963693) * 10 ^ 70 + 5587389786300197331225933771135451265672058516963925125284853459405877) * 10 ^ 70 + 6520083241783092186772099100172187021219752924827993335145293328102423
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_237 :
Polynomial.coeff recurrence5Scalar1First 237 = -(((((58533717 * 10 ^ 70 + 8943091520133569347419572881976922217867271923750336691546149862579386) * 10 ^ 70 + 9558900808097947154134221761588632944906689981843418045833628002041041) * 10 ^ 70 + 6501279579922355598994282056680102944675060761684981232623713993660103) * 10 ^ 70 + 1132619196753033137627023521200830633007766295309184995504354083797171) * 10 ^ 70 + 4546998774193776368973979139086149780676460923578052039674033193691821)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_238 :
Polynomial.coeff recurrence5Scalar1First 238 = ((((38281854 * 10 ^ 70 + 7824715376126713196454242230078310595679085456488955303400289210430790) * 10 ^ 70 + 2401849416987034595841243786814331539731658412804805844509774404145809) * 10 ^ 70 + 8610884027493773405025198502136077247792722565230117708179165030589822) * 10 ^ 70 + 8764838772571976708976821759731333806779002882286390357622198926942569) * 10 ^ 70 + 2280947463876718045732703355206355408412551397876095914448613144193510
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_239 :
Polynomial.coeff recurrence5Scalar1First 239 = -(((((24236819 * 10 ^ 70 + 981052114252335454853795541558777945033557827094169998469295798523382) * 10 ^ 70 + 7507029307919752500133779801934449578054947220693394449551498507669887) * 10 ^ 70 + 3370265507710833019394641799377973222094697955506716158937443866954443) * 10 ^ 70 + 3133265094357549221053174110886510051944047732869205912031082505033650) * 10 ^ 70 + 6282244973205282330424633263840658114224857971168750015149904606243937)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_240 :
Polynomial.coeff recurrence5Scalar1First 240 = ((((14796049 * 10 ^ 70 + 4651049463062901449358145944326425727867019514031783356393901330177336) * 10 ^ 70 + 1966748032383497578887753482373766853413664007169107038491038012956062) * 10 ^ 70 + 1073445899326443728871208444615502297476946484030578791810007190570918) * 10 ^ 70 + 2294477636367570645870640161195221256123368259058355833600311820763916) * 10 ^ 70 + 6331675671713309363242402660379330327136023413158618494055417166340349
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_241 :
Polynomial.coeff recurrence5Scalar1First 241 = -(((((8658566 * 10 ^ 70 + 4390872513261155326168119269524638667184855178839330074689065082441563) * 10 ^ 70 + 1922934345922171070547315297008871771689114478644743540075519314805529) * 10 ^ 70 + 2465128055544184791695295052096571542866933919867230271204113110401453) * 10 ^ 70 + 8262674352875967642712527194440630864256876219951910897640995203411720) * 10 ^ 70 + 3837138523498138421673783815402985664270021570313129435286579712470381)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_242 :
Polynomial.coeff recurrence5Scalar1First 242 = ((((4812308 * 10 ^ 70 + 7448072965528632974049265642440471772307851085267062952973365580214864) * 10 ^ 70 + 8756191909685906561767632978318676370364603491829301076058103048244011) * 10 ^ 70 + 3812151260009318352635781691147177233152052602337854908168694445897591) * 10 ^ 70 + 8616029893348779578158451469601247545145620201891750128445406536220927) * 10 ^ 70 + 7877381360960828483179312528798359670338909005559525333298282955569525
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_243 :
Polynomial.coeff recurrence5Scalar1First 243 = -(((((2500505 * 10 ^ 70 + 2898841743709452848109876316190051159567439066768019677624968376837499) * 10 ^ 70 + 5343891097716898434509844617022786798908741593157680376314334516830521) * 10 ^ 70 + 3546878020836207142106435339667677475054859233663378919511006506432647) * 10 ^ 70 + 5839370158090069825513056225728093484629599831259971415416017789083773) * 10 ^ 70 + 1252946298632691645285384080371655579716067501942854213668406343840417)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_244 :
Polynomial.coeff recurrence5Scalar1First 244 = ((((1178455 * 10 ^ 70 + 5647771818349532728871427859219772170811468840794911136938353623827746) * 10 ^ 70 + 19655267371100943905681155974951615248999210357286016161132681699431) * 10 ^ 70 + 4328976747573577555274096657130246577762234833728824771954052788125230) * 10 ^ 70 + 6783314580561453707540754190778603475922203239560363937249201518891694) * 10 ^ 70 + 1937181979266492164830060837548643277520171901863130953972128110972835
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_245 :
Polynomial.coeff recurrence5Scalar1First 245 = -(((((468757 * 10 ^ 70 + 5566048420321242386236133865375554315585036556314335308857690256030300) * 10 ^ 70 + 2583308867219549034818742466497499242304563919602662712876996370112650) * 10 ^ 70 + 272782242198020448540055578177847784195707588109710311473315404168731) * 10 ^ 70 + 6689645778614565503251721672637321625273813734566775930455624840898461) * 10 ^ 70 + 6855973354246340312610135611350801951301286926639551780516403556007139)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_246 :
Polynomial.coeff recurrence5Scalar1First 246 = ((((120031 * 10 ^ 70 + 6672091476978144412863056016968314979352171412417623207485636042757620) * 10 ^ 70 + 3424435883820523005779179098645042336087683137919473078694041158498642) * 10 ^ 70 + 3137263094323670364777853664510665857188818830358957868258625566512589) * 10 ^ 70 + 4830676553399604506390484760670167191517631337744584131961578682764166) * 10 ^ 70 + 9060480809140949232114856118008530988124800902951458298616590193168920
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_247 :
Polynomial.coeff recurrence5Scalar1First 247 = ((((28214 * 10 ^ 70 + 1604408197045483825497254515908468215269581751306527348516062588194495) * 10 ^ 70 + 2159204956012154525198365372660148187527225672923101420950084267278529) * 10 ^ 70 + 1230560108682560822563900548220286823698860033405248255747223317742693) * 10 ^ 70 + 6775612057162260409514717093302096755820495730522946216603507746982150) * 10 ^ 70 + 3865362171168020406659584100656811259353055611868396988517188480445805
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_248 :
Polynomial.coeff recurrence5Scalar1First 248 = -(((((73679 * 10 ^ 70 + 207270215359758092116658502937949318700960375674571890674229061377899) * 10 ^ 70 + 1578347833056843644475113592534235335297995773903748382121914494276434) * 10 ^ 70 + 3240879423126050096782616953274601764565168728953534234053687347333104) * 10 ^ 70 + 4985708390755399121073045834665812041998014624947698430184994262243088) * 10 ^ 70 + 182237137872619417372699829545410206794005773008494679207234956942167)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_249 :
Polynomial.coeff recurrence5Scalar1First 249 = ((((72559 * 10 ^ 70 + 4694106989266104933309929909428543910375620239632902835152299255517731) * 10 ^ 70 + 9273260013116125084316462539419344385039602588994033943685579624902451) * 10 ^ 70 + 9816651611312397988501446892801683754233729836657122769816229243439633) * 10 ^ 70 + 9545628694750259921588364685009219185647593312029959380934877818174676) * 10 ^ 70 + 5792592162469228602309731245214659766071244695376024099117950896077113
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_250 :
Polynomial.coeff recurrence5Scalar1First 250 = -(((((54905 * 10 ^ 70 + 4616648480163701704220134034932189057627360156292677266036585336286109) * 10 ^ 70 + 9547782927424733768486515793555620492315360803619590539685328735704376) * 10 ^ 70 + 1169045591633483442565476528082674515012772044116291173240103248766417) * 10 ^ 70 + 624635720030080343597854664386484246993312468614658064312179512641379) * 10 ^ 70 + 5437471794220125821291954109519782564672655389611475260404644069143992)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_251 :
Polynomial.coeff recurrence5Scalar1First 251 = ((((35174 * 10 ^ 70 + 1901725071692225300136058448613577475136574439613092969192350408227278) * 10 ^ 70 + 3620386590211953823412952736772362522596159488391320592008491514957843) * 10 ^ 70 + 5506814319840913295117022132091654972550057625701020445236814625361087) * 10 ^ 70 + 3743236052354916141711109636704665387168302434646742305246180100939933) * 10 ^ 70 + 2332272389494544617437043228527494142588924264390206244892995313306894