Recurrence 2 lookup certificate: Scalar2Exceptional 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.recurrence2Scalar2Exceptional_coeff_16 :
Polynomial.coeff recurrence2Scalar2Exceptional 16 = -539801578973208916252537648560366623185112192394
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_17 :
Polynomial.coeff recurrence2Scalar2Exceptional 17 = 138283831980999794509026683149346327307211364981648
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_18 :
Polynomial.coeff recurrence2Scalar2Exceptional 18 = -24728241247262378343831968385929370968527873596853773
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_19 :
Polynomial.coeff recurrence2Scalar2Exceptional 19 = 3267793142065702115374130347878755618617528072908658894
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_20 :
Polynomial.coeff recurrence2Scalar2Exceptional 20 = -297953589528712318904472787116177339613565692880672108983
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_21 :
Polynomial.coeff recurrence2Scalar2Exceptional 21 = 12556348584175479876522190095211554238150555207918759579861
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_22 :
Polynomial.coeff recurrence2Scalar2Exceptional 22 = 1182316948700703425579968628843762104343736575810627698314237
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_23 :
Polynomial.coeff recurrence2Scalar2Exceptional 23 = -295548308061389732433651520870935843275563325544550561869079201
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_24 :
Polynomial.coeff recurrence2Scalar2Exceptional 24 = 31671633980768215111309752049507133046361119116637567623674744804
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_25 :
Polynomial.coeff recurrence2Scalar2Exceptional 25 = -2055996302681523949142934743845676749453139501052588075402357964678
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_26 :
Polynomial.coeff recurrence2Scalar2Exceptional 26 = 59725401877766932850969378953025443986121774715709515467248120549441
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_27 :
Polynomial.coeff recurrence2Scalar2Exceptional 27 = 3800604256691773114056598024287856549349973070786265383887231961655497
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_28 :
Polynomial.coeff recurrence2Scalar2Exceptional 28 = -(67 * 10 ^ 70 + 1861990946240132416753714328800692081733900470038078274828923020322354)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_29 :
Polynomial.coeff recurrence2Scalar2Exceptional 29 = 5357 * 10 ^ 70 + 1300589838975709468824739429120533486081853512444470285168007376258615
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_30 :
Polynomial.coeff recurrence2Scalar2Exceptional 30 = -(295890 * 10 ^ 70 + 8927065698826227923257733347219028416927901989311941077065190254904627)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_31 :
Polynomial.coeff recurrence2Scalar2Exceptional 31 = 12242741 * 10 ^ 70 + 5047966094139169179628929520739606698548378065733201550685470479743727
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_32 :
Polynomial.coeff recurrence2Scalar2Exceptional 32 = -(383439869 * 10 ^ 70 + 6313747227013933377075671865441285276569586349483095961650376350764291)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_33 :
Polynomial.coeff recurrence2Scalar2Exceptional 33 = 8915206210 * 10 ^ 70 + 3444795164872742251606655070914675888022053532664906432388459635163150
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_34 :
Polynomial.coeff recurrence2Scalar2Exceptional 34 = -(155759258451 * 10 ^ 70 + 7506647002785612664735919531011246951229462040846931253848645001257330)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_35 :
Polynomial.coeff recurrence2Scalar2Exceptional 35 = 3174128136302 * 10 ^ 70 + 8378816634453994993790919144184627139878956101754728595625234277432828
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_36 :
Polynomial.coeff recurrence2Scalar2Exceptional 36 = -(150474725534202 * 10 ^ 70 + 2632773875306689995170181323986377599170881048879605422751442890043137)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_37 :
Polynomial.coeff recurrence2Scalar2Exceptional 37 = 7971137903442488 * 10 ^ 70 + 5587039814706060468462809735203086617323103021403667610791876181868932
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_38 :
Polynomial.coeff recurrence2Scalar2Exceptional 38 = -(317679440271282661 * 10 ^ 70 + 4596166908207586124962183931053513863339505834824998076558260756469206)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_39 :
Polynomial.coeff recurrence2Scalar2Exceptional 39 = 9601147534810505207 * 10 ^ 70 + 130506639253086652713426100908795354044769007438911875313340381237343
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_40 :
Polynomial.coeff recurrence2Scalar2Exceptional 40 = -(233253762473783160398 * 10 ^ 70 + 6320842875727538143781396478840519984233825469486078327422577625207601)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_41 :
Polynomial.coeff recurrence2Scalar2Exceptional 41 = 5009495622506558355849 * 10 ^ 70 + 6375720194902609072569938088443028549865919191392878493885343220964419
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_42 :
Polynomial.coeff recurrence2Scalar2Exceptional 42 = -(111620749824496532483117 * 10 ^ 70 + 4946586176926211018360941947524037481388909074657667590181952420044824)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_43 :
Polynomial.coeff recurrence2Scalar2Exceptional 43 = 2932475323884633888023014 * 10 ^ 70 + 9087087765929985439301400754104635667527037973300415434406715102855446
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_44 :
Polynomial.coeff recurrence2Scalar2Exceptional 44 = -(85918431266893648374461306 * 10 ^ 70 + 2385017906315691189333344235568083182116153578755983191769751143487801)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_45 :
Polynomial.coeff recurrence2Scalar2Exceptional 45 = 2492039040061173659097351659 * 10 ^ 70 + 9539385040753164065585078449152292991487507397417344017504710846394829
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_46 :
Polynomial.coeff recurrence2Scalar2Exceptional 46 = -(68042651545804621720932786294 * 10 ^ 70 + 2450754717382745552056651327380060766133544505385906527250921901388180)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_47 :
Polynomial.coeff recurrence2Scalar2Exceptional 47 = 1747371763248872318980158991542 * 10 ^ 70 + 2565308977021319656406110635604324574315459376158414278548213695682601
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_48 :
Polynomial.coeff recurrence2Scalar2Exceptional 48 = -(42571724436759444317882517537760 * 10 ^ 70 + 5733186653059835096322558753929533245860642578428447139830338869931739)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_49 :
Polynomial.coeff recurrence2Scalar2Exceptional 49 = 986298386627345672463067026828363 * 10 ^ 70 + 8084890432515218559258345549394353359800709012290423420793249453690185
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_50 :
Polynomial.coeff recurrence2Scalar2Exceptional 50 = -(21670927618418269980108764985958758 * 10 ^ 70 + 4925162713553001853916339409086557525206938793331922367140068561426232)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_51 :
Polynomial.coeff recurrence2Scalar2Exceptional 51 = 450707868084794720088551682579765267 * 10 ^ 70 + 1551127671829686749448940480275804906135813683490341417698176468668120
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_52 :
Polynomial.coeff recurrence2Scalar2Exceptional 52 = -(8886703101051215123923658910817626179 * 10 ^ 70 + 2649618462730901176097969852448084038211663861902931960145051672947493)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_53 :
Polynomial.coeff recurrence2Scalar2Exceptional 53 = 166768832422671864817173294401948986241 * 10 ^ 70 + 6907704177716386008023293515866253432900243843481843385386629231348880
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_54 :
Polynomial.coeff recurrence2Scalar2Exceptional 54 = -(2989918479878485773880861888422768935051 * 10 ^ 70 + 9445331357219945723429404022754262588256735364583665877243606883293105)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_55 :
Polynomial.coeff recurrence2Scalar2Exceptional 55 = 51319673352608504481896367699395100064923 * 10 ^ 70 + 7117390509686381106922143593159015780261213317793332939202803469589010
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_56 :
Polynomial.coeff recurrence2Scalar2Exceptional 56 = -(843760257255137977954493606740937400421090 * 10 ^ 70 + 8995994578227330703315366337184827534474987366997548866144193402620533)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_57 :
Polynomial.coeff recurrence2Scalar2Exceptional 57 = 13288421039898593082772373533864010515708404 * 10 ^ 70 + 4574182023473394453035830684136845560005791680118039513781614771933732
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_58 :
Polynomial.coeff recurrence2Scalar2Exceptional 58 = -(200542409766793970164965988566461551574429074 * 10 ^ 70 + 6642800029797547655201785724172393890595030198320045839963022772304514)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_59 :
Polynomial.coeff recurrence2Scalar2Exceptional 59 = 2902632952996072745853054416551448572903856003 * 10 ^ 70 + 9237634873912122630369177853301659813127437631373917230719530158756763
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_60 :
Polynomial.coeff recurrence2Scalar2Exceptional 60 = -(40334279389536261066207378228967608288592219204 * 10 ^ 70 + 3849711785954783335603348353810186678339787245559810038868679903764057)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_61 :
Polynomial.coeff recurrence2Scalar2Exceptional 61 = 538544185459173799623208448094874242379812231224 * 10 ^ 70 + 9239331637720642138368862311116370835735790908151425655714226007576791
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_62 :
Polynomial.coeff recurrence2Scalar2Exceptional 62 = -(6913655102819921192581061510182571430366795385882 * 10 ^ 70 + 4216318276094676390047752583015090028802804786392419706600973469812729)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_63 :
Polynomial.coeff recurrence2Scalar2Exceptional 63 = 85386163867939351173768623626615263003887497299132 * 10 ^ 70 + 4323531372278377783332273631019512400691218673148186651132994799735366
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_64 :
Polynomial.coeff recurrence2Scalar2Exceptional 64 = -(1015217219050865615665672002748483551203741309926084 * 10 ^ 70 + 8442579244760219131865347344842016700560621688905224209565875321310915)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_65 :
Polynomial.coeff recurrence2Scalar2Exceptional 65 = 11629423461608626253504466611068928343881393596287451 * 10 ^ 70 + 1339533773349943599104532779882424866327541901592245951279923969579901
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_66 :
Polynomial.coeff recurrence2Scalar2Exceptional 66 = -(128440967274300007264883102675261706613133128199752380 * 10 ^ 70 + 4029033047305593775809872806152958892476377679074814315894626579094215)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_67 :
Polynomial.coeff recurrence2Scalar2Exceptional 67 = 1368534028926862015699900627892647691722432137110108367 * 10 ^ 70 + 8592070529966687014920623945522653646000892776978697931135705412928553
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_68 :
Polynomial.coeff recurrence2Scalar2Exceptional 68 = -(14074380588554221456081056572237665127010413446595637720 * 10 ^ 70 + 3004791898666042193418010430923587949145161881719001758681929724497497)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_69 :
Polynomial.coeff recurrence2Scalar2Exceptional 69 = 139778489683112274236358750714053308627023579079920461068 * 10 ^ 70 + 7075346191017560385463973453190476570382731248588379364600208793309855
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_70 :
Polynomial.coeff recurrence2Scalar2Exceptional 70 = -(1341332037653868178867037290184320359444281654841631148562 * 10 ^ 70 + 3903397852850922566932512247494031736825962291598526484171470627587431)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_71 :
Polynomial.coeff recurrence2Scalar2Exceptional 71 = 12444709059048412613533549140384358189660611927035218067282 * 10 ^ 70 + 4413511968641716357158752168428393797870253736408520136043676634837403
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_72 :
Polynomial.coeff recurrence2Scalar2Exceptional 72 = -(111695472683793843522445574759382143468898741844585754703892 * 10 ^ 70 + 6837120635549617508827881405069886692066101184658440813826652216643333)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_73 :
Polynomial.coeff recurrence2Scalar2Exceptional 73 = 970281601965909279897145579734090179482179470813605988684843 * 10 ^ 70 + 7134136997118740145402086781664189510755788347880173724542532263795849
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_74 :
Polynomial.coeff recurrence2Scalar2Exceptional 74 = -(8161193307926903191453546625107588721436984398593273349839694 * 10 ^ 70 + 4076869189093823495550113666953136425869721693378328370885147383869077)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_75 :
Polynomial.coeff recurrence2Scalar2Exceptional 75 = 66495609087365510437059738580685296579584827287010723804225056 * 10 ^ 70 + 7155612627985319539935820312158024626128360947216895377471162622565888
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_76 :
Polynomial.coeff recurrence2Scalar2Exceptional 76 = -(525085827947394558393872861443273078887704210193660862165543952 * 10 ^ 70 + 1916868652281628304397417378149237465343921471577461818736960700991661)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_77 :
Polynomial.coeff recurrence2Scalar2Exceptional 77 = 4020559223616634520086102278001056599116187269026298951448113749 * 10 ^ 70 + 315666195902606224131117107368412622542817137510062654611427056263137
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_78 :
Polynomial.coeff recurrence2Scalar2Exceptional 78 = -(29864429392323937997874360082216562766532061528607714102282681706 * 10 ^ 70 + 6496819325065542959178936665445129704591319887625676495514456886474240)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_79 :
Polynomial.coeff recurrence2Scalar2Exceptional 79 = 215271843350903837562499416423958701917807857021175560645182979394 * 10 ^ 70 + 8600781656973551423590836149896117930086751093381029175132108980691518
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_80 :
Polynomial.coeff recurrence2Scalar2Exceptional 80 = -(1506359010818537747045087209613037716519679310506072693857728463100 * 10 ^ 70 + 3267505363091000088381356516522679636052842734430539283166444857783896)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_81 :
Polynomial.coeff recurrence2Scalar2Exceptional 81 = 10236480380747348243021606575580574369710869768799220230489084242875 * 10 ^ 70 + 560621521275098838817014354535888046474746895059953391027897601247795
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_82 :
Polynomial.coeff recurrence2Scalar2Exceptional 82 = -(67586780734600260497986121714353569175829759471584324171168477910512 * 10 ^ 70 + 6330910235689934059681062930138477578773533467126821608158799978098366)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_83 :
Polynomial.coeff recurrence2Scalar2Exceptional 83 = 433771775651590646749587781581127283037373660225600129540795545724654 * 10 ^ 70 + 601143304300424668311944572756740113612735244340759203957761331367820
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_84 :
Polynomial.coeff recurrence2Scalar2Exceptional 84 = -(2706998111370401402567598837089438981100212992890189116708676884019816 * 10 ^ 70 + 171164829210085577800449958108428960225985055765006979497922698199245)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_85 :
Polynomial.coeff recurrence2Scalar2Exceptional 85 = (1 * 10 ^ 70 + 6429412129824181357071120949515497103306304739813536779121904868660773) * 10 ^ 70 + 2207448484335229708333007403458939574232892858805172464334539087838496
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_86 :
Polynomial.coeff recurrence2Scalar2Exceptional 86 = -((9 * 10 ^ 70 + 6996767339946283217857279669156890891292546475190047349727235246931895) * 10 ^ 70 + 2653186121310458124001608772762246093434777030036552364217589416004725)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_87 :
Polynomial.coeff recurrence2Scalar2Exceptional 87 = (55 * 10 ^ 70 + 7283065058350687228185724844750208611212856380954170216075996639567516) * 10 ^ 70 + 2996148301202140759018465731934391805630834189404226061002070522722535
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_88 :
Polynomial.coeff recurrence2Scalar2Exceptional 88 = -((311 * 10 ^ 70 + 7682189464264727838055324831937256579096610352175722785220308232207396) * 10 ^ 70 + 9863772389771690255266661065668885062575075171930098647071606103117254)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_89 :
Polynomial.coeff recurrence2Scalar2Exceptional 89 = (1699 * 10 ^ 70 + 1328649427189470338124199528288781665265874435791632637681174385727421) * 10 ^ 70 + 7901649003665045051537567494170987073739154842805380375356849617265031
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_90 :
Polynomial.coeff recurrence2Scalar2Exceptional 90 = -((9021 * 10 ^ 70 + 8855472036491244432969149582571280456687055715511745183486715356439849) * 10 ^ 70 + 3657654680996786773762200043281206936338008212253888103631050507062350)