Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_40 :
Polynomial.coeff recurrence4Scalar0Exceptional 40 = (323 * 10 ^ 70 + 1001619914652702783941897820370995271466392053862206061267599325030123) * 10 ^ 70 + 1110233522375455859515763069718470803154730798542086753661648534684327
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_41 :
Polynomial.coeff recurrence4Scalar0Exceptional 41 = -((35200 * 10 ^ 70 + 7111257103052931089307842289539771255790513090181890897051885411397996) * 10 ^ 70 + 4731099370715565099685789332407522107678893658479843801985080622064380)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_42 :
Polynomial.coeff recurrence4Scalar0Exceptional 42 = (3604408 * 10 ^ 70 + 9503123989017289245252357649343190634364047873430895822778896381411033) * 10 ^ 70 + 1988267641841498199831558464241421904070751479122103516085301780930643
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_43 :
Polynomial.coeff recurrence4Scalar0Exceptional 43 = -((347474387 * 10 ^ 70 + 4532705621303426310452548451302698937067204971918335670218603025552747) * 10 ^ 70 + 540983224264275163645803315248669599550716439772649932423004141124464)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_44 :
Polynomial.coeff recurrence4Scalar0Exceptional 44 = (31586215566 * 10 ^ 70 + 5331071085941592412027978768100555710232040857022442025168349735208228) * 10 ^ 70 + 7897726917879504057829043079033565969814048380847704464778395917006085
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_45 :
Polynomial.coeff recurrence4Scalar0Exceptional 45 = -((2711376670588 * 10 ^ 70 + 7766674970859664948940897859816475138180093593689320879242537774980887) * 10 ^ 70 + 9863618510994620105887003279107803583391914658043449105030048604753037)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_46 :
Polynomial.coeff recurrence4Scalar0Exceptional 46 = (220084480517894 * 10 ^ 70 + 3240514343069003768699182103275080921562968747145442090086120250848523) * 10 ^ 70 + 8876558758420633553153998047561005620373715443173810984161798492444560
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_47 :
Polynomial.coeff recurrence4Scalar0Exceptional 47 = -((16914140785099865 * 10 ^ 70 + 6151500345344068458133946728711418940517545636636622559484648318464730) * 10 ^ 70 + 7388428794918226742029287863799383890880238483454400940569244962349036)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_48 :
Polynomial.coeff recurrence4Scalar0Exceptional 48 = (1232233872464748121 * 10 ^ 70 + 2355327385249283458514122012907148960961982410728404998257830907688867) * 10 ^ 70 + 1281065424515729018243549248747063205754378504735424454097465058873613
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_49 :
Polynomial.coeff recurrence4Scalar0Exceptional 49 = -((85194637194791108494 * 10 ^ 70 + 5374186753317969288665821514387011187066674985014986429022753035137463) * 10 ^ 70 + 4705247031995855424673632632151772250937697646374430432805783024281442)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_50 :
Polynomial.coeff recurrence4Scalar0Exceptional 50 = (5595963595861903506149 * 10 ^ 70 + 6808095799388765994557535291353526754942055208692736466800962906159422) * 10 ^ 70 + 403683556859317261472678533739141468831460051114365803508547861833440
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_51 :
Polynomial.coeff recurrence4Scalar0Exceptional 51 = -((349562920479708725967885 * 10 ^ 70 + 5991566913408363993386527337672201553152925307229395136364161585589922) * 10 ^ 70 + 8990049300172141455795008243656409395202809051938542229582294029605947)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_52 :
Polynomial.coeff recurrence4Scalar0Exceptional 52 = (20786761468580724511418346 * 10 ^ 70 + 7195535166481780716556635336107797377550281392170000264871851536096751) * 10 ^ 70 + 4680576152557908790081528083090120114046632555361084940619861743411449
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_53 :
Polynomial.coeff recurrence4Scalar0Exceptional 53 = -((1177776771419505277400289343 * 10 ^ 70 + 6629065076235969295450068752143250011977851087683580513084095951293900) * 10 ^ 70 + 5810142930056260124782951782022206374768375316799362029310259089033381)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_54 :
Polynomial.coeff recurrence4Scalar0Exceptional 54 = (63641376894588640449369544083 * 10 ^ 70 + 6233935499525264677056820268775757338388195450736634485167825920823005) * 10 ^ 70 + 4692658082364390204251028875065624884947695659645608539060907203151980
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_55 :
Polynomial.coeff recurrence4Scalar0Exceptional 55 = -((3282356358263433701131901728857 * 10 ^ 70 + 6789180094513407835002980360750982940301969705232329676923919922570887) * 10 ^ 70 + 6355028154140018215433888296221587540587720761135609495118356995384190)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_56 :
Polynomial.coeff recurrence4Scalar0Exceptional 56 = (161716819932414684983441521504609 * 10 ^ 70 + 2996570670710797545929153329653867416826127896597711313268842039684150) * 10 ^ 70 + 8901499206801120816282177242307270564395721878959645180161406592685808
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_57 :
Polynomial.coeff recurrence4Scalar0Exceptional 57 = -((7617058345935387686783732996418999 * 10 ^ 70 + 316720284892707678647552891132329412386414944867568145339427960046265) * 10 ^ 70 + 1437104570630814274353950388088611068641043951110003413172192974681961)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_58 :
Polynomial.coeff recurrence4Scalar0Exceptional 58 = (343247870521302989136521601991284919 * 10 ^ 70 + 3611121478402185809434309288329735465934390396877456337919248793432601) * 10 ^ 70 + 2943338169451157828629522083581656871088931484628692969010955335942575
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_59 :
Polynomial.coeff recurrence4Scalar0Exceptional 59 = -((14809148933834455177826599277443376344 * 10 ^ 70 + 3479128099772058016256568718552925683396174142038080346360038535826236) * 10 ^ 70 + 9198694141909197938495721916606336872594397060888737929238834411613159)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_60 :
Polynomial.coeff recurrence4Scalar0Exceptional 60 = (612146416688732842009643733894807226954 * 10 ^ 70 + 8612299626883818024616169473656866086395531611873493795183530882706730) * 10 ^ 70 + 2875373824219128119295786553733903959739221502049559308836034824377101
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_61 :
Polynomial.coeff recurrence4Scalar0Exceptional 61 = -((24259034162506025664200675292035315660320 * 10 ^ 70 + 6964623083375353139560878085741927073168040871360657540049424173586677) * 10 ^ 70 + 6887331546545485136027519110276767610022988747254028900699363075124501)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_62 :
Polynomial.coeff recurrence4Scalar0Exceptional 62 = (922282649813951046883634269090954800067862 * 10 ^ 70 + 6763171032819448189455867042740438600839141194371651994208860730948934) * 10 ^ 70 + 9729337843416118362643494446385660185340618824563751410157684378180834
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_63 :
Polynomial.coeff recurrence4Scalar0Exceptional 63 = -((33658606320454981196020161826010052602980864 * 10 ^ 70 + 5483338817762124619380023054311808468264023570198523347616084176195998) * 10 ^ 70 + 3992369668439384291783119176372263288760507875835455360546481350890011)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_64 :
Polynomial.coeff recurrence4Scalar0Exceptional 64 = (1179856921726164767187212154188458853593581489 * 10 ^ 70 + 5450831047937885355779156826262000549835364636546520067119068224845681) * 10 ^ 70 + 6264522714952847168326550406504741017919300573242507772170366683638011
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_65 :
Polynomial.coeff recurrence4Scalar0Exceptional 65 = -((39747885475610179253634685263736703524895905778 * 10 ^ 70 + 6982928377379042634257456995740231881704593454184418262739875479960631) * 10 ^ 70 + 2688883127606174985901371451708507569652924637780635296964801617311590)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_66 :
Polynomial.coeff recurrence4Scalar0Exceptional 66 = (1287631817746898291629573669289252248064356498950 * 10 ^ 70 + 4663456351236917916362730053671555386120405939352597944024666382851203) * 10 ^ 70 + 5751475841919634922213302048673478641139717435309349670402142501349049
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_67 :
Polynomial.coeff recurrence4Scalar0Exceptional 67 = -((40132423759599084953651951389058069727417537013608 * 10 ^ 70 + 3311747903974089186662195720248184441068409589585848256605134756352373) * 10 ^ 70 + 1872788753036388123595121841494081939881522556296188402577441034456634)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_68 :
Polynomial.coeff recurrence4Scalar0Exceptional 68 = (1204065100480281950768999922628772473848259425999441 * 10 ^ 70 + 7624855348512564865472950550516497257114683467290818937060116720751264) * 10 ^ 70 + 3110562644208748047486866207127752633768339757954177202211280547383828
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_69 :
Polynomial.coeff recurrence4Scalar0Exceptional 69 = -((34791441519606895734383357350966221917624607465329379 * 10 ^ 70 + 5208399345411074918132201560243931464910740551911737857853998339398189) * 10 ^ 70 + 6978434597575996957717463404048551297651823051813369783026462358885233)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_70 :
Polynomial.coeff recurrence4Scalar0Exceptional 70 = (968661644964157465484115125646143255981671034545294826 * 10 ^ 70 + 6599577115059319860691740005517191622773458948415896410805368969619617) * 10 ^ 70 + 2996860021013661197325972142043059092801493166616641692613603157094009
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_71 :
Polynomial.coeff recurrence4Scalar0Exceptional 71 = -((25998658796832925715278496829716559037309868522699526249 * 10 ^ 70 + 64648396431940170887554479455087268721262741144066897347132783007490) * 10 ^ 70 + 8089397696064933260918279633831720816391780266833584764670637165673570)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_72 :
Polynomial.coeff recurrence4Scalar0Exceptional 72 = (672982317371067603325056585667352433543750126799784420137 * 10 ^ 70 + 3282804690160885803660932644984406292656635374120236658011768890557715) * 10 ^ 70 + 3413932151877209648661299354708959482036595711215705471810819400341061
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_73 :
Polynomial.coeff recurrence4Scalar0Exceptional 73 = -((16808070990632138278344584469286408240073670451577045822331 * 10 ^ 70 + 8999035033098124448105301266742204265499173426264107587134278923039215) * 10 ^ 70 + 5055662687292603469598781402547918656455094401034623988849143737596370)