Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3ShiftPart0.Coefficients0To91

Recurrence 2 lookup certificate: Scalar3Shift coefficient convolution #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_0 :
Polynomial.coeff recurrence2Scalar3Shift 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_1 :
Polynomial.coeff recurrence2Scalar3Shift 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_2 :
Polynomial.coeff recurrence2Scalar3Shift 2 = -797631744
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_3 :
Polynomial.coeff recurrence2Scalar3Shift 3 = -18326166224208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_4 :
Polynomial.coeff recurrence2Scalar3Shift 4 = -10767685210621016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_5 :
Polynomial.coeff recurrence2Scalar3Shift 5 = -376173652302335882888
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_6 :
Polynomial.coeff recurrence2Scalar3Shift 6 = 183462296446569560704840
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_7 :
Polynomial.coeff recurrence2Scalar3Shift 7 = 20903551130359936705145356
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_8 :
Polynomial.coeff recurrence2Scalar3Shift 8 = -275710001951205598278094041620
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_9 :
Polynomial.coeff recurrence2Scalar3Shift 9 = 539718918511024088744545296504092
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_10 :
Polynomial.coeff recurrence2Scalar3Shift 10 = -439930528857644265549746151151945956
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_11 :
Polynomial.coeff recurrence2Scalar3Shift 11 = 302705213405722386269727646356498141946
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_12 :
Polynomial.coeff recurrence2Scalar3Shift 12 = -145893664366891715158480469165230912028766
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_13 :
Polynomial.coeff recurrence2Scalar3Shift 13 = 52081221993368123417696693942401786803010690
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_14 :
Polynomial.coeff recurrence2Scalar3Shift 14 = -14005521883254213365665315343278797241776057424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_15 :
Polynomial.coeff recurrence2Scalar3Shift 15 = 2887217712090811155753644900458101934853784011334
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_16 :
Polynomial.coeff recurrence2Scalar3Shift 16 = -458887557993277136474515778578901296994043659577107
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_17 :
Polynomial.coeff recurrence2Scalar3Shift 17 = 55334995391059967187943873586235955607538598683232109
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_18 :
Polynomial.coeff recurrence2Scalar3Shift 18 = -4808696463933121677067953012080663211548851508006262456
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_19 :
Polynomial.coeff recurrence2Scalar3Shift 19 = 247581233987272948542210226817213986941006609521351537032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_20 :
Polynomial.coeff recurrence2Scalar3Shift 20 = 2734535283042297535330735510114329253881943600446505583842
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_21 :
Polynomial.coeff recurrence2Scalar3Shift 21 = -2069732904741258038639375321732259149538163586266071560037449
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_22 :
Polynomial.coeff recurrence2Scalar3Shift 22 = 241709899059640628682938829098954285998441779506251841527770072
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_23 :
Polynomial.coeff recurrence2Scalar3Shift 23 = -17976168746800090232037092926361664531025356474763992043451442183
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_24 :
Polynomial.coeff recurrence2Scalar3Shift 24 = 979521843046848525064972947501028217200891924958541576755533895062
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_25 :
Polynomial.coeff recurrence2Scalar3Shift 25 = -40818179303325960246155217476695345861987185368762072361620263187852
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_26 :
Polynomial.coeff recurrence2Scalar3Shift 26 = 1323302393711113461327032691559684098942914355740695655390873935322060
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_27 :
Polynomial.coeff recurrence2Scalar3Shift 27 = -(3 * 10 ^ 70 + 3042335587475842278056993067648145572554875256698272632563384034443973)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_28 :
Polynomial.coeff recurrence2Scalar3Shift 28 = 52 * 10 ^ 70 + 3599273500279584409402817522125372799863697054418035951010367602434312
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_29 :
Polynomial.coeff recurrence2Scalar3Shift 29 = 679 * 10 ^ 70 + 30919065994812622011566851871077131717652335866487876515633499969676
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_30 :
Polynomial.coeff recurrence2Scalar3Shift 30 = -(108995 * 10 ^ 70 + 2453424430891402903221787212340237973452110016096723924113502122148744)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_31 :
Polynomial.coeff recurrence2Scalar3Shift 31 = 5585384 * 10 ^ 70 + 7789364196234138447717387860302145413322939803083362594400141562870880
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_32 :
Polynomial.coeff recurrence2Scalar3Shift 32 = -(202551666 * 10 ^ 70 + 6874311661071379306729684032112747460879504327568845029404554460166750)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_33 :
Polynomial.coeff recurrence2Scalar3Shift 33 = 8383378867 * 10 ^ 70 + 5934684525006772237997340726081797078081407263732110198789914073248630
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_34 :
Polynomial.coeff recurrence2Scalar3Shift 34 = -(540896290912 * 10 ^ 70 + 6427253782416219604110651984233271947136611233719300397915359078033110)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_35 :
Polynomial.coeff recurrence2Scalar3Shift 35 = 35692996304414 * 10 ^ 70 + 6290040070070038465668535620967822283021915276396489983011180298200089
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_36 :
Polynomial.coeff recurrence2Scalar3Shift 36 = -(1864850451595602 * 10 ^ 70 + 1857913790094479279177938008709254068379830158696277357572797971860170)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_37 :
Polynomial.coeff recurrence2Scalar3Shift 37 = 75263254899889203 * 10 ^ 70 + 2616401457159632377201484217817177185538589315485450488947583173766431
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_38 :
Polynomial.coeff recurrence2Scalar3Shift 38 = -(2388695585478915605 * 10 ^ 70 + 7194660861770137843188104933073448411663545401153634038561339731626853)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_39 :
Polynomial.coeff recurrence2Scalar3Shift 39 = 60803245393253612856 * 10 ^ 70 + 5681083213677446516548890264539170609231155038711898374301899472213822
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_40 :
Polynomial.coeff recurrence2Scalar3Shift 40 = -(1286521445884463692912 * 10 ^ 70 + 8459247564833905759420660635567292242114135977090255636340545754178245)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_41 :
Polynomial.coeff recurrence2Scalar3Shift 41 = 25571139280691572406961 * 10 ^ 70 + 8691942405781941615045131954265069881764795784664862276472091685306303
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_42 :
Polynomial.coeff recurrence2Scalar3Shift 42 = -(632426078316121134239965 * 10 ^ 70 + 561023857251373076214837777824660821892443615776816189942284631633769)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_43 :
Polynomial.coeff recurrence2Scalar3Shift 43 = 21735588396116787958236657 * 10 ^ 70 + 2580895661104743521832393997584492247601318880038375323664638646203566
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_44 :
Polynomial.coeff recurrence2Scalar3Shift 44 = -(801823604511763193475925849 * 10 ^ 70 + 1572128709155405511682525832331602574479166576862147568298082362751122)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_45 :
Polynomial.coeff recurrence2Scalar3Shift 45 = 26420018773117934212003415569 * 10 ^ 70 + 6350151781126118938778873972447784864103735913996824933262572856640785
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_46 :
Polynomial.coeff recurrence2Scalar3Shift 46 = -(743759291779792806279476326567 * 10 ^ 70 + 3924324799815847243733611115811447870814683577099570897403253542903299)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_47 :
Polynomial.coeff recurrence2Scalar3Shift 47 = 17850721993018814106240366880382 * 10 ^ 70 + 3370076922088250709926385642792032298057901069789181721485040725420250
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_48 :
Polynomial.coeff recurrence2Scalar3Shift 48 = -(365635167427964893662908223444653 * 10 ^ 70 + 1990932780713134408840632834089465568181332344005663959252164115077675)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_49 :
Polynomial.coeff recurrence2Scalar3Shift 49 = 6324241717672233198847179330728010 * 10 ^ 70 + 1984464104138326600572567995957375660511948702032626907984766900431395
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_50 :
Polynomial.coeff recurrence2Scalar3Shift 50 = -(88303337697543628920028155974169277 * 10 ^ 70 + 4019284946066727938628207164662473707016693484769586755798183881801633)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_51 :
Polynomial.coeff recurrence2Scalar3Shift 51 = 823503760175835833103011759368359876 * 10 ^ 70 + 9245185623484382704271487542689746924483718026395239214018112235177615
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_52 :
Polynomial.coeff recurrence2Scalar3Shift 52 = 2004286718022355814797770578015020739 * 10 ^ 70 + 6425307600011572941117301894635599210141708482276778918178875038726890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_53 :
Polynomial.coeff recurrence2Scalar3Shift 53 = -(342305531141979571370044161553546670138 * 10 ^ 70 + 9533205715216278095969281041529253633750578620602236259737752295049696)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_54 :
Polynomial.coeff recurrence2Scalar3Shift 54 = 10864691281978292228589276644269731165690 * 10 ^ 70 + 2535711659083008228588647924600996561050390726099547291583033166121691
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_55 :
Polynomial.coeff recurrence2Scalar3Shift 55 = -(252833699877463715400782010856570823625377 * 10 ^ 70 + 101808422112847314612118154243716442748673650016648746268865732592317)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_56 :
Polynomial.coeff recurrence2Scalar3Shift 56 = 4942618408308960291452293896354473902318229 * 10 ^ 70 + 9715564362850074366154711325728839954345290789155891605186165238483119
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_57 :
Polynomial.coeff recurrence2Scalar3Shift 57 = -(84101524523098678001238665917825653989865441 * 10 ^ 70 + 2744256202282595378248526348438370005991770439268625691057921640683863)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_58 :
Polynomial.coeff recurrence2Scalar3Shift 58 = 1249740674822938333633312895827557361472836203 * 10 ^ 70 + 9797312634760257542330539940307146574919081344815751868304944432808115
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_59 :
Polynomial.coeff recurrence2Scalar3Shift 59 = -(15878870938238133363645397018846682100386598708 * 10 ^ 70 + 9708055420592358932047827603513537379140659640197276106142797052422227)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_60 :
Polynomial.coeff recurrence2Scalar3Shift 60 = 160579284536683014780651905746714659433395233830 * 10 ^ 70 + 8002841665698386985843167337209418583629635967263600516393072762372715
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_61 :
Polynomial.coeff recurrence2Scalar3Shift 61 = -(937376154163998859242363880388460448172625892832 * 10 ^ 70 + 2807696104193236286026239575201445790345560911509730131641132798408840)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_62 :
Polynomial.coeff recurrence2Scalar3Shift 62 = -(8571967366436783283083711099270833347256897504583 * 10 ^ 70 + 4638065501749618272162786131781134988340655043110074010086134693196326)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_63 :
Polynomial.coeff recurrence2Scalar3Shift 63 = 420566606921190524269451466893399591912399338179167 * 10 ^ 70 + 2478387003807078958367159230710162632908522196698657863974844558553974
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_64 :
Polynomial.coeff recurrence2Scalar3Shift 64 = -(9407644772013945771244691376590761763730389580822006 * 10 ^ 70 + 6065096753036826119489798140891006840908023318454074946697836802259151)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_65 :
Polynomial.coeff recurrence2Scalar3Shift 65 = 165138234206905874331254674778824644136281682190321095 * 10 ^ 70 + 7420555885625775387855601641743120632439125692759665388655584791328329
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_66 :
Polynomial.coeff recurrence2Scalar3Shift 66 = -(2523454938122732161291344814796216210345528294243875088 * 10 ^ 70 + 4535247165961758124249097356232288736916605502639711787818389883544441)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_67 :
Polynomial.coeff recurrence2Scalar3Shift 67 = 34913745614174053766965902547615383931573152609048440439 * 10 ^ 70 + 330688553146205589707424411428618979598404357713065662179485537024242
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_68 :
Polynomial.coeff recurrence2Scalar3Shift 68 = -(445936762453058075686855929968559931554589098734059495805 * 10 ^ 70 + 1131125257958413913555610381190823121485453607382011582126665672046611)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_69 :
Polynomial.coeff recurrence2Scalar3Shift 69 = 5317060418586390973601773499882866766340909514336046879077 * 10 ^ 70 + 8523468620645828616688164729634777276928747484969867421954957932096433
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_70 :
Polynomial.coeff recurrence2Scalar3Shift 70 = -(59607704660602254643234635459126867821929501765928597958317 * 10 ^ 70 + 6374907936053863108553518586535906049126740702113094899873240224517412)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_71 :
Polynomial.coeff recurrence2Scalar3Shift 71 = 631457262443573697161663489885093804486606148308912163541302 * 10 ^ 70 + 38596035231376156011255223577369496686586345539243414795249807488843
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_72 :
Polynomial.coeff recurrence2Scalar3Shift 72 = -(6344908916285235703509304857603218698413057693790268933738518 * 10 ^ 70 + 474314616493383492589771438568546092337873755049181861191360733740021)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_73 :
Polynomial.coeff recurrence2Scalar3Shift 73 = 60648197912435404833261178889988516540546509299851647040959476 * 10 ^ 70 + 719207863487093111235900865190436956636345143555462060673175798394806
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_74 :
Polynomial.coeff recurrence2Scalar3Shift 74 = -(552756254390675685254330593909056140397340492596576289735065794 * 10 ^ 70 + 4064834681125392669258621698914231226824695168567718998051147413858909)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_75 :
Polynomial.coeff recurrence2Scalar3Shift 75 = 4812636230110894171266004871258331583256962134208292535034513899 * 10 ^ 70 + 8585747466037356581124747338354140201081999770723940747934939997626093
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_76 :
Polynomial.coeff recurrence2Scalar3Shift 76 = -(40088200493227718657420934187095633711189931631199470939097107685 * 10 ^ 70 + 7912230567921913897540691569862052018573415686847307057694619726550542)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_77 :
Polynomial.coeff recurrence2Scalar3Shift 77 = 319862327750816022375915872518672993436956743011034107353478319912 * 10 ^ 70 + 9410751913301485221092301350869337034536048755211471963101706318967656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_78 :
Polynomial.coeff recurrence2Scalar3Shift 78 = -(2447175889588990389847327736901763033872931820314034885087717082036 * 10 ^ 70 + 7424018659279317993428861311262843027696373507745102508051621188320300)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_79 :
Polynomial.coeff recurrence2Scalar3Shift 79 = 17968326870005559671611342963000327327607083244597022568920330776553 * 10 ^ 70 + 9179561645018022676962372909143085475604826413207076909886990099737775
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_80 :
Polynomial.coeff recurrence2Scalar3Shift 80 = -(126716840133292507519062792474126598242677063832490552712974833053169 * 10 ^ 70 + 8452480434698601488393975360383637523017859899132768422746883508967672)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_81 :
Polynomial.coeff recurrence2Scalar3Shift 81 = 858917471803755404968830107610421926526934190327384975056046129250412 * 10 ^ 70 + 7560899870848591437984448472118471880302467066874499334213992015684063
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_82 :
Polynomial.coeff recurrence2Scalar3Shift 82 = -(5599120448075681744806241251780717528944316540901106774598264462718634 * 10 ^ 70 + 7617671947883306162941858017159151814258603862074071736404404386623038)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_83 :
Polynomial.coeff recurrence2Scalar3Shift 83 = (3 * 10 ^ 70 + 5119111984499369175520951990191245593359089585013118156264752839273425) * 10 ^ 70 + 1853245371571893485772444854581498852680569444341941275762315869922689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_84 :
Polynomial.coeff recurrence2Scalar3Shift 84 = -((21 * 10 ^ 70 + 2013154975942035444915767923057467198769253117772492284217554535942374) * 10 ^ 70 + 489151508199813022848853970018730805235906427463992991589590953731712)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_85 :
Polynomial.coeff recurrence2Scalar3Shift 85 = (123 * 10 ^ 70 + 2132537103125159515442533546143174785047609705050502082650550864352901) * 10 ^ 70 + 7227622829650378175189440642969817267294860066183935816017605730564618
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_86 :
Polynomial.coeff recurrence2Scalar3Shift 86 = -((689 * 10 ^ 70 + 3834905953447785589975894482817784470727041500707218325357876368923346) * 10 ^ 70 + 4842716193741428075120981251757011381365705338785167277106049611113811)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_87 :
Polynomial.coeff recurrence2Scalar3Shift 87 = (3713 * 10 ^ 70 + 4585306279723199071033179678319167544510179500621194206230754003728615) * 10 ^ 70 + 3468914688524636540499910519801071539535418457581799542722085423946002
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_88 :
Polynomial.coeff recurrence2Scalar3Shift 88 = -((19257 * 10 ^ 70 + 3880340066356196312621049989514654079910149960451772627892124478476101) * 10 ^ 70 + 6613511199588976092765232876375048793040920932906988637225660280395068)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_89 :
Polynomial.coeff recurrence2Scalar3Shift 89 = (96132 * 10 ^ 70 + 9986755742638534798293044483041875718798544105648117127350859427431582) * 10 ^ 70 + 1967407579165753659943741427972011685314653225505132484365083149784834
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_90 :
Polynomial.coeff recurrence2Scalar3Shift 90 = -((461831 * 10 ^ 70 + 2398442934909898064988555013289139126373254124825860414708978212787945) * 10 ^ 70 + 939063994266364026589011046471835886815263904628167152668381962914545)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_91 :
Polynomial.coeff recurrence2Scalar3Shift 91 = (2133844 * 10 ^ 70 + 2419589655030458662198397002654878680589952994731227632771607116260544) * 10 ^ 70 + 3343044269499842802010893772311909096371059792137974301333781377703446