Recurrence 2 lookup certificate: Scalar4Exceptional 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.recurrence2Scalar4Exceptional_coeff_332 :
Polynomial.coeff recurrence2Scalar4Exceptional 332 = -((17 * 10 ^ 70 + 9902750306295419048420291963130074878408307273230248246749562222548197) * 10 ^ 70 + 4309812264136892754888363571236633513693556499145460493426147204140625)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_333 :
Polynomial.coeff recurrence2Scalar4Exceptional 333 = -((8 * 10 ^ 70 + 4686236529298110531125704113434925537608961728726116255069455629796338) * 10 ^ 70 + 7541758924047384325304036201745552255984186445035017595762803109087965)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_334 :
Polynomial.coeff recurrence2Scalar4Exceptional 334 = -(2886801395711924498350490421249425380743193071840246167090949460753468 * 10 ^ 70 + 8567263865361630449395235484342937804450351547290129402015610049837007)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_335 :
Polynomial.coeff recurrence2Scalar4Exceptional 335 = 116069032453991659032121760953974672360334030585403780520163164276404 * 10 ^ 70 + 2434008933464405946647082876555596653196920901514004264144379341882111
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_336 :
Polynomial.coeff recurrence2Scalar4Exceptional 336 = 14603284496967528152152938545318463356786790406401575271432556114243 * 10 ^ 70 + 6315155306098254351553522311974810031896391437393623729533456509672634
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_337 :
Polynomial.coeff recurrence2Scalar4Exceptional 337 = 691979033307682220068129378015171041856422206778099653934542990096 * 10 ^ 70 + 7940160444830582684704637837000391169507527741860669677814781755592641
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_338 :
Polynomial.coeff recurrence2Scalar4Exceptional 338 = 20849441095888894010579929848524113707186268992175310231385417555 * 10 ^ 70 + 3464982639666475803051936228964248126690116798252912376439361306987402
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_339 :
Polynomial.coeff recurrence2Scalar4Exceptional 339 = 448194042173330635537653426055045904947884501802371962185365474 * 10 ^ 70 + 979201070523969796984124322236670331079660323463722661281284937030485
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_340 :
Polynomial.coeff recurrence2Scalar4Exceptional 340 = 7197923914561939166096373465369559494328843787469239400732038 * 10 ^ 70 + 6810726199026981526179879533952353095614062336542934451623639177970690
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_341 :
Polynomial.coeff recurrence2Scalar4Exceptional 341 = 88199674571672187901093999421089936281805138630079558980330 * 10 ^ 70 + 6039118618036955972095048392625338368782280631428899683576610715856598
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_342 :
Polynomial.coeff recurrence2Scalar4Exceptional 342 = 830791704622545757749030565314299608295783978746892633880 * 10 ^ 70 + 578935912682468390932542828020009472423802715218296664734786902506163
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_343 :
Polynomial.coeff recurrence2Scalar4Exceptional 343 = 5994119901606682643921309889057215410433825436021810335 * 10 ^ 70 + 6062644531216409929742610645468461102067081641151112563289084245466622
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_344 :
Polynomial.coeff recurrence2Scalar4Exceptional 344 = 32546916810466160917919741515879254934309379972181912 * 10 ^ 70 + 8792149314265784171798092451678267010729990736418366928171701789933808
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_345 :
Polynomial.coeff recurrence2Scalar4Exceptional 345 = 127142206760691542034699376087597550370300582060401 * 10 ^ 70 + 8422272690111485256782606546937152787347829219352470328553077270283252
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_346 :
Polynomial.coeff recurrence2Scalar4Exceptional 346 = 313823954531756183361815971096438784436641354105 * 10 ^ 70 + 9692275728116255381201010339414774869326839490234453045389453666760058
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_347 :
Polynomial.coeff recurrence2Scalar4Exceptional 347 = 210131585923257730688336600589122947798949878 * 10 ^ 70 + 7970535466926744132581087983325579561973439346097234463039095729361770
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_348 :
Polynomial.coeff recurrence2Scalar4Exceptional 348 = -(1743053084072876811621159186349096252357222 * 10 ^ 70 + 9543165650438983959322230126235584661004459375044070471246798957479808)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_349 :
Polynomial.coeff recurrence2Scalar4Exceptional 349 = -(7443389230383853460525359933342839521542 * 10 ^ 70 + 7432847648420064450542529123833511991672553400867545102197780684200263)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_350 :
Polynomial.coeff recurrence2Scalar4Exceptional 350 = -(12459063866979167151192518217327150535 * 10 ^ 70 + 8179860991588439905688523137889949694674016623908838527672169569854546)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_351 :
Polynomial.coeff recurrence2Scalar4Exceptional 351 = 1574434912918844585532364579433209 * 10 ^ 70 + 4753024267347351562016130408190451355360434403961543239843165879550634
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_352 :
Polynomial.coeff recurrence2Scalar4Exceptional 352 = 49347866865681395107451201929760 * 10 ^ 70 + 9008899396447728292535900410590659753782806645524967022845880395421467
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_353 :
Polynomial.coeff recurrence2Scalar4Exceptional 353 = 94153351339516478072949445118 * 10 ^ 70 + 2890881404539263134901352359966393355171892056827015541473231663961560
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_354 :
Polynomial.coeff recurrence2Scalar4Exceptional 354 = 53752501234608625648527559 * 10 ^ 70 + 5678072068752906512372216686834647622096648439158145055021761308210922
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_355 :
Polynomial.coeff recurrence2Scalar4Exceptional 355 = -(82843784593566346081579 * 10 ^ 70 + 535782149348018402694376351088960356917856977852840609729541761760130)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_356 :
Polynomial.coeff recurrence2Scalar4Exceptional 356 = -(196877719029288602299 * 10 ^ 70 + 5843364487800569657838984158020231738941120649569864612075521052332725)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_357 :
Polynomial.coeff recurrence2Scalar4Exceptional 357 = -(188689020300243295 * 10 ^ 70 + 5332332516064785259100087364244069871120371289228578536382745422274911)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_358 :
Polynomial.coeff recurrence2Scalar4Exceptional 358 = -(103636615995708 * 10 ^ 70 + 7670620791837187616514228130375884727904368710501977330471150777293348)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_359 :
Polynomial.coeff recurrence2Scalar4Exceptional 359 = -(34526309222 * 10 ^ 70 + 7843230013186428341720491478809918606131569386011375569444040152872780)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_360 :
Polynomial.coeff recurrence2Scalar4Exceptional 360 = -(6945112 * 10 ^ 70 + 5788767160738750974361603460341706964405445446764043980405197963847464)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_361 :
Polynomial.coeff recurrence2Scalar4Exceptional 361 = -(820 * 10 ^ 70 + 9175256953363857470343879651614168637789123547129117638015618821516203)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_362 :
Polynomial.coeff recurrence2Scalar4Exceptional 362 = -553579653869120253594481098387031836829607782707811626952184156645348
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_363 :
Polynomial.coeff recurrence2Scalar4Exceptional 363 = -20125022237489898250371401369318508091834256904817584990967126230
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_364 :
Polynomial.coeff recurrence2Scalar4Exceptional 364 = -352804146258149357695252210621796573535926531729387519626262
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_365 :
Polynomial.coeff recurrence2Scalar4Exceptional 365 = -2618820130382954920395923334285577735862410527799027583
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_366 :
Polynomial.coeff recurrence2Scalar4Exceptional 366 = -8740486410694444934977191240100770161277291264086