Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2ExceptionalPart0.Coefficients0To90

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_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)