Recurrence 2 lookup certificate: Scalar4Left 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.recurrence2Scalar4Left_coeff_92 :
Polynomial.coeff recurrence2Scalar4Left 92 = -((12386482 * 10 ^ 70 + 4177527357057794655028943003792375381717281835983967451089516109893981) * 10 ^ 70 + 4894284263082841815965889223468718979131325106391780161410265857446284)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_93 :
Polynomial.coeff recurrence2Scalar4Left 93 = (49924199 * 10 ^ 70 + 6813327601432781398839731143336455233956867282867382387948216334940608) * 10 ^ 70 + 8386161807965431025562731885130051353424813043753494108102881866767308
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_94 :
Polynomial.coeff recurrence2Scalar4Left 94 = -((191283669 * 10 ^ 70 + 1726024791563070804498916001341752493006595265217465252937195585535497) * 10 ^ 70 + 7309096050330261335023869478030955596102193724084505623773278148872298)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_95 :
Polynomial.coeff recurrence2Scalar4Left 95 = (692562248 * 10 ^ 70 + 8264816458393518809017665738725991074551049663282781449341722324599238) * 10 ^ 70 + 7035571588580587992168253947547792113903512696409624985597122377426341
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_96 :
Polynomial.coeff recurrence2Scalar4Left 96 = -((2347207580 * 10 ^ 70 + 5742551967935295168824217951080802254208324845005617354115454940852727) * 10 ^ 70 + 6874176197083842218235380068565371759660927330692414888813784021464144)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_97 :
Polynomial.coeff recurrence2Scalar4Left 97 = (7326617187 * 10 ^ 70 + 7583327569027614213828344517862689740036291590684713037907639961957600) * 10 ^ 70 + 2448922415697601430716456783779427529333078311970499416222165128260647
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_98 :
Polynomial.coeff recurrence2Scalar4Left 98 = -((20397217374 * 10 ^ 70 + 2421320164488604025258517329451743451785601266055605642842020914284586) * 10 ^ 70 + 1856230906351554834757236406686610939971542776421790120889261079109845)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_99 :
Polynomial.coeff recurrence2Scalar4Left 99 = (46723266417 * 10 ^ 70 + 4554531396645250297647272410426422615765593780564179907770470639618543) * 10 ^ 70 + 2003264309475901192677569171796731314370644899398117764137041731478895
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_100 :
Polynomial.coeff recurrence2Scalar4Left 100 = -((62406636414 * 10 ^ 70 + 7089224815362462078108856635390129140634894529368471798532382730439659) * 10 ^ 70 + 7676646961359804713869735568894030849049533827489440880974778548263166)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_101 :
Polynomial.coeff recurrence2Scalar4Left 101 = -((154329546821 * 10 ^ 70 + 6450531341553683009346789850629935408872183863185219971824617176695712) * 10 ^ 70 + 8847526866718103006751987168470596703463002355142365872293867505790743)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_102 :
Polynomial.coeff recurrence2Scalar4Left 102 = (1783587597340 * 10 ^ 70 + 8902600963390413939509447581687174642745918373766164584597188494369799) * 10 ^ 70 + 9416263719595859003653093941487009989793674918898402173393690128616628
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_103 :
Polynomial.coeff recurrence2Scalar4Left 103 = -((9937276052513 * 10 ^ 70 + 276520081574506416641215406432296345499069517160872416385394619561219) * 10 ^ 70 + 7962905632572096570272861648651402800360655365732884878924666562214559)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_104 :
Polynomial.coeff recurrence2Scalar4Left 104 = (44005775233064 * 10 ^ 70 + 1352184713371900677215361934020669208291326003894416581465151047943686) * 10 ^ 70 + 6192626688461385179281864274805263426408501325683273106808793919307410
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_105 :
Polynomial.coeff recurrence2Scalar4Left 105 = -((169589339732919 * 10 ^ 70 + 9098049032697166432347255046240617061235938304222118135614027806645024) * 10 ^ 70 + 84973526183932413199788693015288198161632968974997168582555211280076)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_106 :
Polynomial.coeff recurrence2Scalar4Left 106 = (583967038931294 * 10 ^ 70 + 8123646086556281231412682490533573311700026623139452848787071986238268) * 10 ^ 70 + 4558787145733485455761192866826452932191432575798073585511160577176727
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_107 :
Polynomial.coeff recurrence2Scalar4Left 107 = -((1807359447335394 * 10 ^ 70 + 3994006914691517810499472738668479626353297382861133591878172874928517) * 10 ^ 70 + 5286349189886208261949380909884233276968704619458519320373871575165381)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_108 :
Polynomial.coeff recurrence2Scalar4Left 108 = (5038569563880457 * 10 ^ 70 + 1037340573208384315390800867810834495187509892288930885341583143051585) * 10 ^ 70 + 2486831883821657514720242338810227671340866142244016042281695735981756
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_109 :
Polynomial.coeff recurrence2Scalar4Left 109 = -((12892136418236667 * 10 ^ 70 + 318346683467111814175845531794745019769079893283158054615400810883630) * 10 ^ 70 + 8997529525966517845622849139519313247616491368879544026268392047392382)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_110 :
Polynomial.coeff recurrence2Scalar4Left 110 = (32298720992951532 * 10 ^ 70 + 5773566256223815978128624923106724558689189706461488797120233116433374) * 10 ^ 70 + 3137735456950770448424478430071239137542896812695929199608508510241662
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_111 :
Polynomial.coeff recurrence2Scalar4Left 111 = -((86286244830624092 * 10 ^ 70 + 3425672512970892469661225372967053039463021642586835548113194908663573) * 10 ^ 70 + 2818265801211379297964745053712681114591147187634145925294247786426436)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_112 :
Polynomial.coeff recurrence2Scalar4Left 112 = (226152889126670595 * 10 ^ 70 + 6410226460207183119365299120594465724953143000507650061958721209658748) * 10 ^ 70 + 7632854101603336193021639088286593225344043132265910827662733474927517
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_113 :
Polynomial.coeff recurrence2Scalar4Left 113 = -((299845404441476839 * 10 ^ 70 + 1707119966342592155221177417444779068650143906209113660542246567545150) * 10 ^ 70 + 5157539088651256374191133204510742546529011908263066911400007186804328)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_114 :
Polynomial.coeff recurrence2Scalar4Left 114 = -((1970442017415426741 * 10 ^ 70 + 2504502907226847610938962767913817672425747236952865803905954019231539) * 10 ^ 70 + 3192015557332355423629711172121982610448622870218244614549380192775596)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_115 :
Polynomial.coeff recurrence2Scalar4Left 115 = (19034235499761657915 * 10 ^ 70 + 654165797022196665585253867859813817263296406714486693068036303738047) * 10 ^ 70 + 5591619060056354087393531221093810312214901660622898347821662945535972
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_116 :
Polynomial.coeff recurrence2Scalar4Left 116 = -((90381237928145533599 * 10 ^ 70 + 197947491952711954810846295787087214291015779629247809241682748155447) * 10 ^ 70 + 8585532466299386726250570778217162209470339506455173687941335794060983)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_117 :
Polynomial.coeff recurrence2Scalar4Left 117 = (262735444214392529498 * 10 ^ 70 + 4857010444277391575961768614823891195557536092274110418458438463667551) * 10 ^ 70 + 3108232155602977864098582456667007977648268814014734291631715007808569
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_118 :
Polynomial.coeff recurrence2Scalar4Left 118 = -((272841493072263858046 * 10 ^ 70 + 3500979670752361795460253040798072692152914394374528279010752658919477) * 10 ^ 70 + 9140426849690351622054192808486947016268786950612884679324771667424142)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_119 :
Polynomial.coeff recurrence2Scalar4Left 119 = -((1813436841870717019310 * 10 ^ 70 + 1910094346638153951345474429265052518650475033007081078797083235121567) * 10 ^ 70 + 5034061333069825004049412881896585156241350973752909184479409997515031)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_120 :
Polynomial.coeff recurrence2Scalar4Left 120 = (12513019137563323165051 * 10 ^ 70 + 7856411364675009458947594065989670443602269652690132740527058746179855) * 10 ^ 70 + 1536649943727711015011195431687941903039452627065909219377635572902621
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_121 :
Polynomial.coeff recurrence2Scalar4Left 121 = -((39277927190620584597949 * 10 ^ 70 + 7206016974092560528649107905972849539681561886057332597349036987166749) * 10 ^ 70 + 1720915757251579166780343438225319389046648707048560599583486767965782)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_122 :
Polynomial.coeff recurrence2Scalar4Left 122 = (24934197720162022649988 * 10 ^ 70 + 637188129436850516546545727194651010891792436594104954621832332583553) * 10 ^ 70 + 6646512775268353775786030101399818295287562084849044240456559598615461
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_123 :
Polynomial.coeff recurrence2Scalar4Left 123 = (456205404628667992814031 * 10 ^ 70 + 1165003356843074834218572157262706082128078959866613161614337494639072) * 10 ^ 70 + 6848284824160671486764611363975991894283979344146934368753501125443054
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_124 :
Polynomial.coeff recurrence2Scalar4Left 124 = -((2780431439932103405501538 * 10 ^ 70 + 6208457735823345730322394106165801839044283760083953048604145512419757) * 10 ^ 70 + 4231218063131354716992211231972757765943274043551036059403326652548886)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_125 :
Polynomial.coeff recurrence2Scalar4Left 125 = (8010844829303995634855589 * 10 ^ 70 + 2949027590342968920824904577092088497739402704125099131315385800129617) * 10 ^ 70 + 781626213554226554796399854106644601705214571493461810956259214843047
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_126 :
Polynomial.coeff recurrence2Scalar4Left 126 = -((7468484638975642947458692 * 10 ^ 70 + 1804523080192372898742964994294110192912854593864771992120952169815455) * 10 ^ 70 + 591987641702225937734906787651277661789810786462982996934661821587506)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_127 :
Polynomial.coeff recurrence2Scalar4Left 127 = -((17331021611144372787976777 * 10 ^ 70 + 2640662742797661888345838114271211597507138673305063790086774132825886) * 10 ^ 70 + 2244762687954472202299065758576694778237230431612153698785106300610174)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_128 :
Polynomial.coeff recurrence2Scalar4Left 128 = -((49844373502006962935882162 * 10 ^ 70 + 8536729192547874228632201826388620195402570874535415247719494376216841) * 10 ^ 70 + 7040296643185445364379579805974401825067200046573345964919357589165002)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_129 :
Polynomial.coeff recurrence2Scalar4Left 129 = (546104713969803732079355812 * 10 ^ 70 + 9846742740315633063247415535867903410737799376486953530620673558152794) * 10 ^ 70 + 4919048028573828501361511558485652474691578112714459983628049676695156
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_130 :
Polynomial.coeff recurrence2Scalar4Left 130 = (2692610385420627680577425526 * 10 ^ 70 + 153473078604382837583857892007691797008059289569223464427984574018974) * 10 ^ 70 + 1557376573085903274948103959140494811670582227128022816793985823391175
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_131 :
Polynomial.coeff recurrence2Scalar4Left 131 = -((44522646370733572211456720171 * 10 ^ 70 + 6140061308906167932464704539527628950767811291665185237593039889945830) * 10 ^ 70 + 8382193646000926143832907225004877217352605181661986779733031097689613)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_132 :
Polynomial.coeff recurrence2Scalar4Left 132 = (209573661799076231107067166247 * 10 ^ 70 + 5428720492622010952516914315442846694068023516850571752068051596848417) * 10 ^ 70 + 1858535874280981098516093596565530301705948873120836902824699835016558
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_133 :
Polynomial.coeff recurrence2Scalar4Left 133 = -((188106800644912474402774914160 * 10 ^ 70 + 8931160225072001652808771881959790869311679204908190388221562619690813) * 10 ^ 70 + 5280170623077060976953635045321587106993433895766034342175705598787038)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_134 :
Polynomial.coeff recurrence2Scalar4Left 134 = -((3049262546120484070176474186921 * 10 ^ 70 + 9879008807093498228483599844127161136009551230903497513905535987955149) * 10 ^ 70 + 6743620220775346808868401815365889072092038929041193895479569861950569)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_135 :
Polynomial.coeff recurrence2Scalar4Left 135 = (17548813072879125081958983939050 * 10 ^ 70 + 5940574347720143437302335878221969231401797260548608492905417707917202) * 10 ^ 70 + 3272204603185933982235867319740517742245793139008081861417973846886111
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_136 :
Polynomial.coeff recurrence2Scalar4Left 136 = -((28902554736574572213488030882563 * 10 ^ 70 + 6595479266250287982052893012396958856265632008809398721864116930378336) * 10 ^ 70 + 2786753605437075416378152622909637759206509238122045124508799304280286)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_137 :
Polynomial.coeff recurrence2Scalar4Left 137 = -((137991320345582148214155534347927 * 10 ^ 70 + 6281364241808863210039485850309031905778408861429523271916300358355700) * 10 ^ 70 + 2588489695575993029509928527639022312822562684981900842702897981601721)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_138 :
Polynomial.coeff recurrence2Scalar4Left 138 = (922408292309697517846165857549460 * 10 ^ 70 + 7924628473497421478457351171375155258593373720458725261068336169518434) * 10 ^ 70 + 2302971459795882973156235413739626018485939210947845862045128144481805
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_139 :
Polynomial.coeff recurrence2Scalar4Left 139 = -((1441469331387171781223281928413725 * 10 ^ 70 + 8456462162563712240215281862508377328052849692812039573363673889118451) * 10 ^ 70 + 1904809237834288301344929705679899165641862699171067210365544395746824)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_140 :
Polynomial.coeff recurrence2Scalar4Left 140 = -((7348773007351291141367865724461546 * 10 ^ 70 + 5967696701980965985853959616943055080304591535712360114073577607132047) * 10 ^ 70 + 3070768636007825991831235745897217541763362426012535095655093589387121)