Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2LeftPart1.Coefficients272To304

Recurrence 2 lookup certificate: Scalar2Left 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.recurrence2Scalar2Left_coeff_272 :

Polynomial.coeff recurrence2Scalar2Left 272 = (16150063731996286846521310063250967917278767763589251408286151564737 * 10 ^ 70 + 5461112700138631852590631726554135837575222701015149704548103443727600) * 10 ^ 70 + 5895078392180348981795355319446967886782733466427617964689951348052059

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_273 :

Polynomial.coeff recurrence2Scalar2Left 273 = -((6650451264548169552259371941696340168223954194458073800075325151317 * 10 ^ 70 + 618121022478228584667127348409022542282058047717743833633549590291228) * 10 ^ 70 + 8826384087534175025202134826218838471563430788316241229729523725929724)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_274 :

Polynomial.coeff recurrence2Scalar2Left 274 = (2552984138627424132147363099118789472386501630899371822559967438867 * 10 ^ 70 + 8382745232699342924267935942082284736009023435493027177042198761579266) * 10 ^ 70 + 5893791041953821311601150020656584704312026867586640117314168659245293

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_275 :

Polynomial.coeff recurrence2Scalar2Left 275 = -((899701160409480602060288097995151460906243155600267294076044796944 * 10 ^ 70 + 3625506946771083152595266319768586767431605905041993784462616865983917) * 10 ^ 70 + 6650550194573493184625033024827577993725898679066996603590514017783347)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_276 :

Polynomial.coeff recurrence2Scalar2Left 276 = (282023394451165310390027896686579310843036052466122651312640233375 * 10 ^ 70 + 2990561565081505615660069598111299824454006865615604890240912311543811) * 10 ^ 70 + 5971975245321719960066686818139107228515155681146023533197840104376895

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_277 :

Polynomial.coeff recurrence2Scalar2Left 277 = -((72596988485396502805635399159477456066817563479716560372510772388 * 10 ^ 70 + 1219965727638192585228860039495528051457625858690590428896184042281778) * 10 ^ 70 + 6958637097485085432187518385076105593673684835758890743237080016175428)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_278 :

Polynomial.coeff recurrence2Scalar2Left 278 = (10958749170513135545560811139204749613060842470178004584335674091 * 10 ^ 70 + 9761599044199857577383852829204906635130687888187324875312988755248639) * 10 ^ 70 + 8478754347280960476769749662306570555119073042226371712249741779407952

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_279 :

Polynomial.coeff recurrence2Scalar2Left 279 = (2862646354922322995973521962883823474717370463160601309493703218 * 10 ^ 70 + 1077758132588223284064557085372203333911715097331998640161772649038851) * 10 ^ 70 + 8777330983453031763352063052958350740646698748355277140280106955360423

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_280 :

Polynomial.coeff recurrence2Scalar2Left 280 = -((3735844766505204283162981168593163073157035728176026640962657191 * 10 ^ 70 + 8194088438870881045975312857613727779918691974682062032316545185143533) * 10 ^ 70 + 2907743819346485631759064236733944864996221433167482279778170717630969)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_281 :

Polynomial.coeff recurrence2Scalar2Left 281 = (2303656156191863267359386895618516041666526133065963858079194097 * 10 ^ 70 + 2435294768400108043774638493412026268871647078901123091556539317783599) * 10 ^ 70 + 8626333354308819061493167745518094918149341191023682255100377578101927

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_282 :

Polynomial.coeff recurrence2Scalar2Left 282 = -((1128082207870393640408135721162305053984981849931798332563383500 * 10 ^ 70 + 1380506842427586311650112416476337127158270132508587716719959475067561) * 10 ^ 70 + 8552832415414056446635137556991847931421194854220483320877219508041171)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_283 :

Polynomial.coeff recurrence2Scalar2Left 283 = (483982186868455425748734712907416562685593111422080561169766731 * 10 ^ 70 + 6682327733001383885467358489201682981365909851501973843268178677145433) * 10 ^ 70 + 7139188223036759370313413732256222872360337650756201477096275457711650

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_284 :

Polynomial.coeff recurrence2Scalar2Left 284 = -((188419578099302611421047342238643968386123602053279818918880193 * 10 ^ 70 + 9473622145457443458531777998234000055059451631110021145015888345732173) * 10 ^ 70 + 8825706685156735187087022643586336871444056328178910332283764566410944)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_285 :

Polynomial.coeff recurrence2Scalar2Left 285 = (67571867301490273694528260317768000400811986196866055122759656 * 10 ^ 70 + 8377113632296049445544335604667648462868217989686067021626745728242366) * 10 ^ 70 + 7830121263758402394846072983946318699536139121603988114716525263817961

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_286 :

Polynomial.coeff recurrence2Scalar2Left 286 = -((22455794779591080576398713939573731991844355921083982398911747 * 10 ^ 70 + 6418764794805774754198346843154062035523202607635843260497863157548220) * 10 ^ 70 + 9215309189186087631094914212309370726501073843808401625900424763198404)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_287 :

Polynomial.coeff recurrence2Scalar2Left 287 = (6916832439593875022854386517176893700067669071183804073781438 * 10 ^ 70 + 5143342449917937436832062730616502646916420267985490206399051266655386) * 10 ^ 70 + 7297429224304453516934557115905656346713289277405719845631936137726517

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_288 :

Polynomial.coeff recurrence2Scalar2Left 288 = -((1964723198218348619018996914022181438230618457332696439260387 * 10 ^ 70 + 145483107980094242800310743648730045228085161629259800791064401488510) * 10 ^ 70 + 701060375288500055219726862279543372019529219593035836827832172443135)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_289 :

Polynomial.coeff recurrence2Scalar2Left 289 = (508327318691584257513614362877159426411846728899222819241668 * 10 ^ 70 + 3953935873638015227655201877162604869048171691850219071475646824359606) * 10 ^ 70 + 7880598339831077800311530875466207538799173316184984478496797441406423

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_290 :

Polynomial.coeff recurrence2Scalar2Left 290 = -((116659566775793600102829623727546197398752093763060364855476 * 10 ^ 70 + 2660270471494121708379079115379984601514242563353341347818070000440250) * 10 ^ 70 + 2079163416919828552973282089682270365141009421705508863720199768902003)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_291 :

Polynomial.coeff recurrence2Scalar2Left 291 = (22265891157163054047844412710910237775242269399815171091500 * 10 ^ 70 + 7600328750187964795132319749063766313457553065264768049364631550502879) * 10 ^ 70 + 5562224238142381927988120001826618088017373844649694474231242022723190

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_292 :

Polynomial.coeff recurrence2Scalar2Left 292 = -((2801360093301985412250015427885369642024878724974540547173 * 10 ^ 70 + 1697853892346426211637940284372087669807567349701805546574427411085948) * 10 ^ 70 + 4062303255119357557845322748384013198288060978543728679319144578111597)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_293 :

Polynomial.coeff recurrence2Scalar2Left 293 = -((186098020529858540701799266179606616046214039679207424858 * 10 ^ 70 + 150616317545651079392201463619553421924908070579654834097710704650929) * 10 ^ 70 + 9694303843240807521609695094303769951863375549642832953433399082922708)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_294 :

Polynomial.coeff recurrence2Scalar2Left 294 = (287616063192653576593960078543851837089868127431046487700 * 10 ^ 70 + 3825663580987589200073121978176759771146990152849798548071010221455839) * 10 ^ 70 + 6614587448725964317375683115194933029375556556519814544194548374567133

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_295 :

Polynomial.coeff recurrence2Scalar2Left 295 = -((127741103707792504867696752779089594665504292157696457215 * 10 ^ 70 + 1580681019315809928235773165936256828265350457926788363092783979622658) * 10 ^ 70 + 7345039328010944674006377133090458089981754512400345044817218649643763)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_296 :

Polynomial.coeff recurrence2Scalar2Left 296 = (42483084601076049248025347753164726266707742842239577144 * 10 ^ 70 + 8471488233519559110719246550719490075497296628120036940351152994609295) * 10 ^ 70 + 4163490465321024968190376075953838423547070729127057989852919785476483

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_297 :

Polynomial.coeff recurrence2Scalar2Left 297 = -((11978756424162249396720527522431273938403778817294423562 * 10 ^ 70 + 2211526767137543737784611662293764216788906528990131010132143280205768) * 10 ^ 70 + 203799536365612396740724423017277693181891145600733499734053128226333)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_298 :

Polynomial.coeff recurrence2Scalar2Left 298 = (2973189705221168828693456714760794845540513526372774966 * 10 ^ 70 + 1369236900715496825144541878611674600410547592401554533688338079123587) * 10 ^ 70 + 1316572366274756121573513033952456020527249406255097184707514051732482

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_299 :

Polynomial.coeff recurrence2Scalar2Left 299 = -((656216470122983872287573079808537642144608597346658890 * 10 ^ 70 + 1383325125106790819603193742494070767644120639804112869809790208872511) * 10 ^ 70 + 7812749555577828838982854818928817614994619175380750464858865544370582)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_300 :

Polynomial.coeff recurrence2Scalar2Left 300 = (127987718661675486541966266636279306833005924883990580 * 10 ^ 70 + 5585333612261965108814268836148285027769487009341981984561829307312449) * 10 ^ 70 + 1572035772211896767321903725867968650596419403185774154315830015836830

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_301 :

Polynomial.coeff recurrence2Scalar2Left 301 = -((21479449134845973702037846328376245312179923357275133 * 10 ^ 70 + 9166668032760308383204801394091587405275885204385341329971464610349092) * 10 ^ 70 + 8150246118730315631340987439607754005327882880584185829868461641113820)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_302 :

Polynomial.coeff recurrence2Scalar2Left 302 = (2874866375870631189101967707687495936845888080609990 * 10 ^ 70 + 9304023408767000636634589402738522563433136715841361424685943026154410) * 10 ^ 70 + 801745853438272848199970055607156929712098335208327807503851076243972

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_303 :

Polynomial.coeff recurrence2Scalar2Left 303 = -((222756117590763750190336552654529825418458199041235 * 10 ^ 70 + 5429941804328850457104696808313917390101351538198327909008426115509971) * 10 ^ 70 + 6665012173051740520017493044618978498709291476140364531623614627101972)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_304 :

Polynomial.coeff recurrence2Scalar2Left 304 = -((25267707342556567618060670547252174032493324174661 * 10 ^ 70 + 8053022986011846762238945259962982977429061875531556526074958207403703) * 10 ^ 70 + 5425492374075220324735179309721609415498294354047615090099440598058048)