Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3ShiftPart0.Coefficients153To193

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_153 :
Polynomial.coeff recurrence2Scalar3Shift 153 = -((81468665989986180789924249248377597031716 * 10 ^ 70 + 2799768159874043811953837521923455826041668527564969344742161636063707) * 10 ^ 70 + 6401210147125554272511196035712196032975840496412314253875995878574389)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_154 :
Polynomial.coeff recurrence2Scalar3Shift 154 = -((2835026430081224321770572766005771221995117 * 10 ^ 70 + 7094006481550377611906127449648518547848747936916154613874216231036299) * 10 ^ 70 + 115358906609776109022630630506217797056885549942178988947155288634861)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_155 :
Polynomial.coeff recurrence2Scalar3Shift 155 = (11037303070979080906845240123516539586406024 * 10 ^ 70 + 7114702803647535492544296846573833545072715558265095196925119539829767) * 10 ^ 70 + 9031969067847684140005355204236379558399449042296931633457008325880960
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_156 :
Polynomial.coeff recurrence2Scalar3Shift 156 = -((5501809289725788901402351403341080152109638 * 10 ^ 70 + 6475730537204749330581551493595442418749471907004445601184486527012287) * 10 ^ 70 + 4354220887822479273100460418282225317186361243403219094495664836584201)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_157 :
Polynomial.coeff recurrence2Scalar3Shift 157 = -((111216042764848306251494588269297198495512035 * 10 ^ 70 + 4756185320479037714321418044490016127203981810753470981151736457334417) * 10 ^ 70 + 7004201785041072124111625679467201491472841911230786229464127658662396)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_158 :
Polynomial.coeff recurrence2Scalar3Shift 158 = (469706903038386060014111285545528789069839490 * 10 ^ 70 + 3373250401181582370904267236366199861810849874028790894647168294659174) * 10 ^ 70 + 3713865163618447121974224948814823199716831319408742118906446285698240
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_159 :
Polynomial.coeff recurrence2Scalar3Shift 159 = -((435863946780772822697541453296721087005319778 * 10 ^ 70 + 6837793689141999683587709053565233259671281592372943982055127640478848) * 10 ^ 70 + 870745965112288401190804289871867774007884167408862256296826847933018)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_160 :
Polynomial.coeff recurrence2Scalar3Shift 160 = -((3753665361542200877432072687325691884871835834 * 10 ^ 70 + 9633275277520679915237431481775325844024955304882846468337146734384430) * 10 ^ 70 + 8273720267245717234980710970889374209367551997414611072251372009854227)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_161 :
Polynomial.coeff recurrence2Scalar3Shift 161 = (18884001503145949894152753339905778337792255948 * 10 ^ 70 + 1563755453696311757265186589732057612918510443538097375293318575908971) * 10 ^ 70 + 5609228984272285313313297225485906996309870201182345628704695677233300
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_162 :
Polynomial.coeff recurrence2Scalar3Shift 162 = -((29263874371678269989523141818626184191602663596 * 10 ^ 70 + 9761509737605323189296151501092569456662347972405333981012840833515180) * 10 ^ 70 + 2291618513893013258763855069848681521912069636275770312636682649632580)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_163 :
Polynomial.coeff recurrence2Scalar3Shift 163 = -((94628295077454830002402421557398044291585547047 * 10 ^ 70 + 7738875885647185258973475126294835370521275035469593711219835965574468) * 10 ^ 70 + 3578269855448502697050561481857766757238341029971304534942772765383998)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_164 :
Polynomial.coeff recurrence2Scalar3Shift 164 = (667555444138041952920227930804366208259480391479 * 10 ^ 70 + 461369448923307457787473337847682565232924087557450584815633727095908) * 10 ^ 70 + 659434666460671234938417895961080364503447890319659998758113749678773
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_165 :
Polynomial.coeff recurrence2Scalar3Shift 165 = -((1534100728704687048577128870792623412285660685729 * 10 ^ 70 + 3571004664345008131212153661468834082063615624676257108836586719357985) * 10 ^ 70 + 1042002937887938941760993702376438939150277335796095499586298879192785)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_166 :
Polynomial.coeff recurrence2Scalar3Shift 166 = -((1019163377748713692323801689410221105747799086347 * 10 ^ 70 + 2470226184918275207792471993222450109959685586529999345859474649342375) * 10 ^ 70 + 4399251623102571350799650012758413148714257226095408052478430038018200)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_167 :
Polynomial.coeff recurrence2Scalar3Shift 167 = (19198142209700721453202714787710054988361840200748 * 10 ^ 70 + 4782786442432929497198878994918084072186055472000623800007987693539874) * 10 ^ 70 + 7675723922045585223808495998311987094224720168058110158017741679898111
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_168 :
Polynomial.coeff recurrence2Scalar3Shift 168 = -((62509562219346061999946335553332450872564828592735 * 10 ^ 70 + 1310542975392122557909807391813969717131978676335732338098416256975648) * 10 ^ 70 + 2098540903868206692613685437205522071332531519858950584521704826948323)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_169 :
Polynomial.coeff recurrence2Scalar3Shift 169 = (51258227449741461269345056800482866055362498364027 * 10 ^ 70 + 9756908339063560387627929101773883000481981107047097084014758216662484) * 10 ^ 70 + 1189663774330818373104883894447463555976953318462384484930698564451755
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_170 :
Polynomial.coeff recurrence2Scalar3Shift 170 = (396868486930722952016739359318772818029339992006424 * 10 ^ 70 + 3767313499249938486150156811349075491942771871853856214125436655927327) * 10 ^ 70 + 1856399822448679625846804954607371730940042634628794137386433897322489
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_171 :
Polynomial.coeff recurrence2Scalar3Shift 171 = -((1972380266312303808040372254996075872057649975288913 * 10 ^ 70 + 8279512727623031775812043019703243984087626318816008762159581493242095) * 10 ^ 70 + 2881184469292085763012915134504412233575727391147766951333071809965448)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_172 :
Polynomial.coeff recurrence2Scalar3Shift 172 = (3823713938391227624828659223104384706987246525294173 * 10 ^ 70 + 2345631493101963856564144002513184347620468719420608513374847294909432) * 10 ^ 70 + 7450654530414869734920106862526178978951102874574204812256796057532242
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_173 :
Polynomial.coeff recurrence2Scalar3Shift 173 = (3239554824422180330814584093541087180693180147759368 * 10 ^ 70 + 723306323158250300868784001924426645086193076247720214190414100258706) * 10 ^ 70 + 9242080433852004292497986837258087837793961361314992227222216863887308
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_174 :
Polynomial.coeff recurrence2Scalar3Shift 174 = -((45909923651969754591361804072824035614930661998783657 * 10 ^ 70 + 4559494488891595777202312985004575941509437925594218990717352891692167) * 10 ^ 70 + 6068525264300682372211060630034254027642010209872054762524249826887321)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_175 :
Polynomial.coeff recurrence2Scalar3Shift 175 = (145405735663449747561410513627340145936968553481957609 * 10 ^ 70 + 9856946805635743651131990939705351144558092258951553526622469639287183) * 10 ^ 70 + 2664792800786697295929539963378203495708944065048879320726158434108878
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_176 :
Polynomial.coeff recurrence2Scalar3Shift 176 = -((158726805548970846304583953876377062230735366816289685 * 10 ^ 70 + 1654679587573347802353302302879107079587680919093719494517175645950700) * 10 ^ 70 + 9887527904546268851726714798539826445913155739258837150096439064868450)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_177 :
Polynomial.coeff recurrence2Scalar3Shift 177 = -((618148691879452430885130700434081241798720674004037918 * 10 ^ 70 + 5490889947059363719834917490365311008024298939501919992835417759741218) * 10 ^ 70 + 2246582924308845689259614030681123696947491546160533471937598709571792)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_178 :
Polynomial.coeff recurrence2Scalar3Shift 178 = (3654722310154998627780558037856579391812275172431806874 * 10 ^ 70 + 4015317207121611043147136718973716745637151122120759609902680647783817) * 10 ^ 70 + 9375470739222101517155409072662631012201833926256938844248969072616283
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_179 :
Polynomial.coeff recurrence2Scalar3Shift 179 = -((8870827724221676230746220724002389467148180252886259493 * 10 ^ 70 + 9420160660235692567994262936548842815542975792517594394771245898925495) * 10 ^ 70 + 9779098771393554148969791941534771170389350655669742814427024928249895)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_180 :
Polynomial.coeff recurrence2Scalar3Shift 180 = (4594842227086738595751684934659831327881519748065526687 * 10 ^ 70 + 5590461841658212555576395867755798192240255014051499319164965488733962) * 10 ^ 70 + 9925283906743670701504123628159114257813959850699441086807398499099867
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_181 :
Polynomial.coeff recurrence2Scalar3Shift 181 = (52068144627096211807581271952658750268713950814159434442 * 10 ^ 70 + 6277505697154912504173046137190637665366527382443183718069991588643994) * 10 ^ 70 + 9965516006291887463487872816650972992689232977128058784578285264926899
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_182 :
Polynomial.coeff recurrence2Scalar3Shift 182 = -((234026634952173438830290046925778115085568404659995918693 * 10 ^ 70 + 192436322438757415130905725241741057789296159697711300532886907754337) * 10 ^ 70 + 4296024215889431454286050230906343173213742758663976237343828224310323)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_183 :
Polynomial.coeff recurrence2Scalar3Shift 183 = (499195232997513314012764576349976584442088063926758164792 * 10 ^ 70 + 4702288302326583629180391112873760096424629141168779866116770937214296) * 10 ^ 70 + 5694033893318328806993034002227852883148521728287018249101554752784191
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_184 :
Polynomial.coeff recurrence2Scalar3Shift 184 = -((166248006315937458013710974539351212109309417276016802330 * 10 ^ 70 + 9553769675753775899819321718928956977694759305324554364924088382918768) * 10 ^ 70 + 9935148805692368647974229535123304570755606065262728959893245073777573)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_185 :
Polynomial.coeff recurrence2Scalar3Shift 185 = -((3013041961112276637661986517848484160008517496583087421007 * 10 ^ 70 + 1058120493161501490769033176667418681162654750675502708496436851986403) * 10 ^ 70 + 6171527315251892706567098158633203958588638775834651719962251484197940)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_186 :
Polynomial.coeff recurrence2Scalar3Shift 186 = (12722761279915026636329494917699421546909032678651095583270 * 10 ^ 70 + 2376912818099386379679004696454387487370053251546572499078246287132345) * 10 ^ 70 + 9035215969503296314884095487563846081178172326839946699848286366485795
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_187 :
Polynomial.coeff recurrence2Scalar3Shift 187 = -((27461863230088454769476340528496363907248749826602648481254 * 10 ^ 70 + 6700361414785445749512694940889595956919800564823761409328047036467506) * 10 ^ 70 + 6288014690920514527480501452526336806521970252262502682193895932505406)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_188 :
Polynomial.coeff recurrence2Scalar3Shift 188 = (17074540913738883852474944537469798915104704744300025015574 * 10 ^ 70 + 5220180598950547115469077493376955177843441708344151823760591457698305) * 10 ^ 70 + 46267176506205510951380608357965893019468966474384969593985062282095
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_189 :
Polynomial.coeff recurrence2Scalar3Shift 189 = (121348441059211346575064884991976308049126703828981565968676 * 10 ^ 70 + 1111092012402808910553832914188340626954524626702422964777339159919202) * 10 ^ 70 + 1506464856601432186460881971143515298339081322985848402127927184927633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_190 :
Polynomial.coeff recurrence2Scalar3Shift 190 = -((579207715759652673330394565298674457458689793763025232881828 * 10 ^ 70 + 4380039350392152229107683394633530125940133992156632508983544632677375) * 10 ^ 70 + 5913414291538946378203359518773022570257448300982073879832602181076101)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_191 :
Polynomial.coeff recurrence2Scalar3Shift 191 = (1425253554506197002289548736801505487527698755846217978396859 * 10 ^ 70 + 3634234056722963998762257973704823213326459400973023857325791214541475) * 10 ^ 70 + 5020870750823737363856501878415107176688363535661553467636072862041066
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_192 :
Polynomial.coeff recurrence2Scalar3Shift 192 = -((1737672259765204840266102165903303807118096759173493644733856 * 10 ^ 70 + 7951415668180214161277530471987905004965101646619695208872988237708610) * 10 ^ 70 + 5954025712118473542193533091477959056252573135651308877574364453962814)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_193 :
Polynomial.coeff recurrence2Scalar3Shift 193 = -((2341213264667649007432497334380806019915742198671486700744085 * 10 ^ 70 + 1583733026427652210261387153516457221071705028264831894975995607254881) * 10 ^ 70 + 7672014356697147754300282264022145207441739717780744625844064254730728)