Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2ShiftPart0.Coefficients0To91

Recurrence 2 lookup certificate: Scalar2Shift 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.recurrence2Scalar2Shift_coeff_0 :
Polynomial.coeff recurrence2Scalar2Shift 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_1 :
Polynomial.coeff recurrence2Scalar2Shift 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_2 :
Polynomial.coeff recurrence2Scalar2Shift 2 = -30639360
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_3 :
Polynomial.coeff recurrence2Scalar2Shift 3 = -534745352016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_4 :
Polynomial.coeff recurrence2Scalar2Shift 4 = -620674798134872
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_5 :
Polynomial.coeff recurrence2Scalar2Shift 5 = -11418197174276105368
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_6 :
Polynomial.coeff recurrence2Scalar2Shift 6 = 2384109950161019549536
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_7 :
Polynomial.coeff recurrence2Scalar2Shift 7 = -8342373451761820338365116
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_8 :
Polynomial.coeff recurrence2Scalar2Shift 8 = -1812378605507060833273378752
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_9 :
Polynomial.coeff recurrence2Scalar2Shift 9 = 19660549659925200026410512094064
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_10 :
Polynomial.coeff recurrence2Scalar2Shift 10 = -19337911760526632686221325979725972
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_11 :
Polynomial.coeff recurrence2Scalar2Shift 11 = 16824971678446981232829741686081064054
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_12 :
Polynomial.coeff recurrence2Scalar2Shift 12 = -9188854940356392855852732433829781096912
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_13 :
Polynomial.coeff recurrence2Scalar2Shift 13 = 3759457601858054355081735496383164031307654
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_14 :
Polynomial.coeff recurrence2Scalar2Shift 14 = -1151118405413128775116581289767509010030313526
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_15 :
Polynomial.coeff recurrence2Scalar2Shift 15 = 270302743341955979386472569007394313312911794680
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_16 :
Polynomial.coeff recurrence2Scalar2Shift 16 = -49166243905767789708065888629341412510671450135667
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_17 :
Polynomial.coeff recurrence2Scalar2Shift 17 = 6882778072195135000382868609184940099429222882528746
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_18 :
Polynomial.coeff recurrence2Scalar2Shift 18 = -723656170133465455598305468246667738603215190240640710
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_19 :
Polynomial.coeff recurrence2Scalar2Shift 19 = 52442830644631946538423790239741466188774843369411525639
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_20 :
Polynomial.coeff recurrence2Scalar2Shift 20 = -1709861789112135246465205271971173805734604242280072021722
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_21 :
Polynomial.coeff recurrence2Scalar2Shift 21 = -153839139118102138436911625875488975025990319750775590134919
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_22 :
Polynomial.coeff recurrence2Scalar2Shift 22 = 31100433519452612865436328984727503869866321719965202196381430
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_23 :
Polynomial.coeff recurrence2Scalar2Shift 23 = -2955078921078864582587362379735891641763960149034077410764188016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_24 :
Polynomial.coeff recurrence2Scalar2Shift 24 = 195785537294689977889919744584592878199345634430344884455691771018
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_25 :
Polynomial.coeff recurrence2Scalar2Shift 25 = -9837942489700065925175937315458303281513556617766496347948046881128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_26 :
Polynomial.coeff recurrence2Scalar2Shift 26 = 384712570728356784530284081192084035473337128025409119086343006598204
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_27 :
Polynomial.coeff recurrence2Scalar2Shift 27 = -(1 * 10 ^ 70 + 1446121550269349499868076784899760795374299996298257146640681124096508)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_28 :
Polynomial.coeff recurrence2Scalar2Shift 28 = 20 * 10 ^ 70 + 3955581127891715535524327169044130138789329953629732450629769329800439
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_29 :
Polynomial.coeff recurrence2Scalar2Shift 29 = 394 * 10 ^ 70 + 6348982565848008906177941765467497839882891726292939686925031574352260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_30 :
Polynomial.coeff recurrence2Scalar2Shift 30 = -(63551 * 10 ^ 70 + 7385303923578045342948376784899635488151040462958818820471300501880253)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_31 :
Polynomial.coeff recurrence2Scalar2Shift 31 = 3881229 * 10 ^ 70 + 8412248534982272953222235656931872741435232425885284022676157579269789
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_32 :
Polynomial.coeff recurrence2Scalar2Shift 32 = -(166615766 * 10 ^ 70 + 6148694074551742988006375787422867906935871396185169464455586474207438)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_33 :
Polynomial.coeff recurrence2Scalar2Shift 33 = 5601887328 * 10 ^ 70 + 1644210916860104091962466446812918894739061620680898549971126434774433
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_34 :
Polynomial.coeff recurrence2Scalar2Shift 34 = -(164168382449 * 10 ^ 70 + 286258727443761426445363213819222823355930900957193820481936281214985)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_35 :
Polynomial.coeff recurrence2Scalar2Shift 35 = 4959807142065 * 10 ^ 70 + 1600210178955236543981277413248159790565252657356324581082454178957965
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_36 :
Polynomial.coeff recurrence2Scalar2Shift 36 = -(167045443773982 * 10 ^ 70 + 9064675812984057237527348080739739593717034292595601626989605497877081)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_37 :
Polynomial.coeff recurrence2Scalar2Shift 37 = 5470735784638216 * 10 ^ 70 + 7194057442350709265759504464479799697998510562513466699431277987530180
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_38 :
Polynomial.coeff recurrence2Scalar2Shift 38 = -(148391253896546217 * 10 ^ 70 + 9898871969946850451395677778450286363916164762167002053479512848027060)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_39 :
Polynomial.coeff recurrence2Scalar2Shift 39 = 3109335852260633168 * 10 ^ 70 + 155957835552264027108864218445736357864868274120665244805544541411303
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_40 :
Polynomial.coeff recurrence2Scalar2Shift 40 = -(54617210936240068684 * 10 ^ 70 + 2696289637362860165945883779391729226344454322580049760757328455095863)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_41 :
Polynomial.coeff recurrence2Scalar2Shift 41 = 1264088883244646595617 * 10 ^ 70 + 5352713801129232837369157521668871528346859190241489117101632695033954
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_42 :
Polynomial.coeff recurrence2Scalar2Shift 42 = -(47774796911062409063735 * 10 ^ 70 + 4818456557116431321054409623845579708165240678738844425381191404738942)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_43 :
Polynomial.coeff recurrence2Scalar2Shift 43 = 1770107279010636934079751 * 10 ^ 70 + 1146730944005590433839147899737472306385965160778190647317261994047071
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_44 :
Polynomial.coeff recurrence2Scalar2Shift 44 = -(50956321396444875796203546 * 10 ^ 70 + 6677717294167274549386189067840491742555967093965839273719344087972114)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_45 :
Polynomial.coeff recurrence2Scalar2Shift 45 = 1104204152752554005408037146 * 10 ^ 70 + 7064206517511048361598304587836325202572023545865123015089043432498527
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_46 :
Polynomial.coeff recurrence2Scalar2Shift 46 = -(17045869485603230471483008482 * 10 ^ 70 + 6138990901272661769123818762043994514629784859327729789969572873223771)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_47 :
Polynomial.coeff recurrence2Scalar2Shift 47 = 116849270889357251520008261510 * 10 ^ 70 + 2772841013390073380416276080622207654929888256220418070713893124753212
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_48 :
Polynomial.coeff recurrence2Scalar2Shift 48 = 3950000313079038616590946316461 * 10 ^ 70 + 1343687988635082512959666247361961827417657279877822232786445251620338
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_49 :
Polynomial.coeff recurrence2Scalar2Shift 49 = -(231500000020365444430485235557149 * 10 ^ 70 + 4569813785219599217169602120407458899673168967194013452730252084137461)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_50 :
Polynomial.coeff recurrence2Scalar2Shift 50 = 8030920671814158029587590657148565 * 10 ^ 70 + 655044108597539472719287445140718590573347051476928327492769297288556
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_51 :
Polynomial.coeff recurrence2Scalar2Shift 51 = -(227705675059387695528835886035024863 * 10 ^ 70 + 6563507657929955787345076307318985992307031337583029304317308651127896)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_52 :
Polynomial.coeff recurrence2Scalar2Shift 52 = 5631045014602534857391249153614654600 * 10 ^ 70 + 6256153460554439537032509893808786171324284229114807314161139118605774
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_53 :
Polynomial.coeff recurrence2Scalar2Shift 53 = -(124322442461715205220453290969963387875 * 10 ^ 70 + 8579713086001535559436658670634169265637196989629398640113888917023753)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_54 :
Polynomial.coeff recurrence2Scalar2Shift 54 = 2485435038092370307446553698254797737312 * 10 ^ 70 + 8626265023231267186797410219885501761418924153387119859365577445712797
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_55 :
Polynomial.coeff recurrence2Scalar2Shift 55 = -(45467887128740407506663298389141944438706 * 10 ^ 70 + 6027154809824897044021377499388768576200089419671454090840554267393793)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_56 :
Polynomial.coeff recurrence2Scalar2Shift 56 = 765363891250251296825446481098778602763297 * 10 ^ 70 + 3010572120200290657291541443032552941375301670766423935873774098246420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_57 :
Polynomial.coeff recurrence2Scalar2Shift 57 = -(11822966223175245224715539286922518683547561 * 10 ^ 70 + 9895677653680832943258709199621927992012534347816511233458638023155777)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_58 :
Polynomial.coeff recurrence2Scalar2Shift 58 = 164969185509954581656781654924408684217122665 * 10 ^ 70 + 7970005042709308318087936010636204267831021790621446087341984807815109
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_59 :
Polynomial.coeff recurrence2Scalar2Shift 59 = -(1996006906006141581457034176894986388200860003 * 10 ^ 70 + 3451761792948069240428206724761568245568924670262574119112944295588122)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_60 :
Polynomial.coeff recurrence2Scalar2Shift 60 = 18652825165490197828480246059831590039033996323 * 10 ^ 70 + 7488837068961733999040412656003712702364222878283338986345845930970259
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_61 :
Polynomial.coeff recurrence2Scalar2Shift 61 = -(66778380423699728231407507224517283857068099104 * 10 ^ 70 + 9616684381054332378520144061253444701110616342392333768805354139079621)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_62 :
Polynomial.coeff recurrence2Scalar2Shift 62 = -(2410921831322823616852990269361768613212722753972 * 10 ^ 70 + 2851447425619262105173286449413650095053652196383263387573625254645682)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_63 :
Polynomial.coeff recurrence2Scalar2Shift 63 = 83129328932182959635143814065704210367080113620813 * 10 ^ 70 + 9582783801282271248782874274623235615334031813705537383471626310556424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_64 :
Polynomial.coeff recurrence2Scalar2Shift 64 = -(1792038479274851819110132880727609341081114839259406 * 10 ^ 70 + 5135805114890858842383820319644928298811923325601359832259452255813181)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_65 :
Polynomial.coeff recurrence2Scalar2Shift 65 = 31806537929491054003153088687303411191714739232716304 * 10 ^ 70 + 4266310983967362818878084807703052674473381181525989621111511805080978
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_66 :
Polynomial.coeff recurrence2Scalar2Shift 66 = -(499803849784767478393303904837384413427037552011314388 * 10 ^ 70 + 9680365756888283613396977928297233407323977562812915792600639146659237)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_67 :
Polynomial.coeff recurrence2Scalar2Shift 67 = 7169460384311588612936826579496983381762154448234793031 * 10 ^ 70 + 4778135648651181008677452175049134193898219639266722193364466355114176
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_68 :
Polynomial.coeff recurrence2Scalar2Shift 68 = -(95389545251772832855358437387528000404510895446436542802 * 10 ^ 70 + 3127764354393057832441722648625107402665555594002788633234579342726229)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_69 :
Polynomial.coeff recurrence2Scalar2Shift 69 = 1188288980407361669238495572529759969105071222681595703733 * 10 ^ 70 + 9139113346218888874972526680790634638589233836643556642899829815133102
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_70 :
Polynomial.coeff recurrence2Scalar2Shift 70 = -(13943619835422967741956941985941591187013508124946106664200 * 10 ^ 70 + 8780455966587953034391593831945095360727974739251200929635789367242475)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_71 :
Polynomial.coeff recurrence2Scalar2Shift 71 = 154770970884548426567206627998061848709386448721048730416748 * 10 ^ 70 + 8539103586825073166366859523777386827871328128578026818290048407214779
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_72 :
Polynomial.coeff recurrence2Scalar2Shift 72 = -(1630188560479360282932877718168184556291243251139931138991499 * 10 ^ 70 + 1523076792210168142802010992316285851763740086899463833646523410274483)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_73 :
Polynomial.coeff recurrence2Scalar2Shift 73 = 16335036192687585719396096035104601153880926703011485338073879 * 10 ^ 70 + 2024120580322328656745065546651337673985620196487508977675411854759692
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_74 :
Polynomial.coeff recurrence2Scalar2Shift 74 = -(156045165693984283672003622929164538074485685802683847489792696 * 10 ^ 70 + 2015615946199478852804559986363838670631423875065761328300272958330477)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_75 :
Polynomial.coeff recurrence2Scalar2Shift 75 = 1423627214328900300764938960098672082919659066263828526160522324 * 10 ^ 70 + 6604860669312051163466957628348975147602709013248960418576744371383726
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_76 :
Polynomial.coeff recurrence2Scalar2Shift 76 = -(12422183301159873864480197842177071547894375015208577335174501898 * 10 ^ 70 + 321781446962230521245994262384727820431549018436791275056162092258230)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_77 :
Polynomial.coeff recurrence2Scalar2Shift 77 = 103796594643458262135234497373911149275913937616668450550255143375 * 10 ^ 70 + 3033641766420148738040524205976010910560255008746467232799657167453546
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_78 :
Polynomial.coeff recurrence2Scalar2Shift 78 = -(831358960075386552931968328255640947889688932639861374705574738102 * 10 ^ 70 + 5396942612524517587375081069193506333195235662107280364739612570837922)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_79 :
Polynomial.coeff recurrence2Scalar2Shift 79 = 6388304321729578252629816376971963144704278634183502165071848120053 * 10 ^ 70 + 2644852357560131869757189857188874218546049840779550527905794361802861
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_80 :
Polynomial.coeff recurrence2Scalar2Shift 80 = -(47130650093387607201752500283573703216238173481218747550250220699940 * 10 ^ 70 + 3560528915880285752614979573984814479592606676121869009341622262830236)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_81 :
Polynomial.coeff recurrence2Scalar2Shift 81 = 334075059953538692007461242785037991102606443190852743698580743422440 * 10 ^ 70 + 304040198589670963668783509019358798314704198971262972542672945398580
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_82 :
Polynomial.coeff recurrence2Scalar2Shift 82 = -(2276586377443358973351736041883391831174244471780427642972881513823815 * 10 ^ 70 + 7287070317679756508378741800949628730693697540778565030407888413220001)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_83 :
Polynomial.coeff recurrence2Scalar2Shift 83 = (1 * 10 ^ 70 + 4923338788693767078856223458304747387286028712655908794908472450073198) * 10 ^ 70 + 2981314447969016796534138141410370352111124540542905622133728610815999
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_84 :
Polynomial.coeff recurrence2Scalar2Shift 84 = -((9 * 10 ^ 70 + 4142123828390364892549316441837219309614411420430553414692595713912616) * 10 ^ 70 + 563757076912328732148301131139523801694805357071578269042224518611134)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_85 :
Polynomial.coeff recurrence2Scalar2Shift 85 = (57 * 10 ^ 70 + 1708313202026739568669708367959536131994025139750177802929714309602871) * 10 ^ 70 + 8097481210454300171286872113987475647213937330832887764381344987579171
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_86 :
Polynomial.coeff recurrence2Scalar2Shift 86 = -((334 * 10 ^ 70 + 2845970040868055590874620502530844446375698679163690870819357524537369) * 10 ^ 70 + 8690483599212224912474556371118294510420399935363309588672327713053834)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_87 :
Polynomial.coeff recurrence2Scalar2Shift 87 = (1882 * 10 ^ 70 + 1007456708783159368757490096807866769365003855308792346741742860228247) * 10 ^ 70 + 7156955128842250581300351330325644061069126785051598868458188841659980
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_88 :
Polynomial.coeff recurrence2Scalar2Shift 88 = -((10203 * 10 ^ 70 + 7500108107187663751551036005927328904451845536687091949227528675827178) * 10 ^ 70 + 2908888593592574492147689671659220275234176041781752268378589773223129)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_89 :
Polynomial.coeff recurrence2Scalar2Shift 89 = (53266 * 10 ^ 70 + 9114485002043276123051070513524990710834741905972637812040230773366566) * 10 ^ 70 + 1150097993881312869838440895529659563444393885021384143651752905938234
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_90 :
Polynomial.coeff recurrence2Scalar2Shift 90 = -((267733 * 10 ^ 70 + 3980417949143250407062798136922712940118696408925002834834093706037922) * 10 ^ 70 + 8510885133639972778630647342395662605771966501477552106986471747824538)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_91 :
Polynomial.coeff recurrence2Scalar2Shift 91 = (1295385 * 10 ^ 70 + 9313437747900560737057655232717435350257272836704412233012626829020701) * 10 ^ 70 + 8422204610015609137601854812288504305978278319975977174341576371256177