Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2FirstPart1.Coefficients224To249

Recurrence 4 lookup certificate: Scalar2First coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_224 :
Polynomial.coeff recurrence4Scalar2First 224 = (((29779670545848756549524873 * 10 ^ 70 + 9486535928457399151725290212775034765462419143820543724222144791963051) * 10 ^ 70 + 4170898506202786533018580513862731413649669269367376241870295125228831) * 10 ^ 70 + 1489115152082784709983547529763785766571781742549681073050235161302075) * 10 ^ 70 + 1029783705751015677914777242033256333193289452041714641409290220801050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_225 :
Polynomial.coeff recurrence4Scalar2First 225 = -((((42713566116555600745441056 * 10 ^ 70 + 1046522700109605050784673291534885199144021204113206389808786659921210) * 10 ^ 70 + 5640007263592535623274143804653257058466763855007617468658189688708742) * 10 ^ 70 + 6885688744386906446875987123457454785773003181530734453521861799042741) * 10 ^ 70 + 6467805654117793798577947442346322698222872879947255760220025236567085)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_226 :
Polynomial.coeff recurrence4Scalar2First 226 = (((60395488201633375156740613 * 10 ^ 70 + 3735595892424475782493236241017265447211859258675294433756779704129879) * 10 ^ 70 + 3680268390022895102079025259422305952059935005183282539117697119352543) * 10 ^ 70 + 1769878827907047829768001978671989100092631340233744869141685680430427) * 10 ^ 70 + 4215694173777142610635380789397233316144529750511434634622024222897517
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_227 :
Polynomial.coeff recurrence4Scalar2First 227 = -((((84181027840910637881844599 * 10 ^ 70 + 1292775877765901764679433570745485508430717599890776973473820086482019) * 10 ^ 70 + 842122537701048485077871075333396139479920465006703730824498397510515) * 10 ^ 70 + 1692802234765999634183810139010032935909855289643645795913922013819727) * 10 ^ 70 + 6385595733882945278461198911891679995148708525969492900526052405952176)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_228 :
Polynomial.coeff recurrence4Scalar2First 228 = (((115656712166275357445617125 * 10 ^ 70 + 9279293702105091934189425617051165719756692560276845103921320896324876) * 10 ^ 70 + 8674868344330368978416645763617355075705823076578605293431740024963506) * 10 ^ 70 + 6611898140365364250895713977346796466488104793893510195542642982973378) * 10 ^ 70 + 7180055105924045521843757598045594788085315702888303912977581153271968
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_229 :
Polynomial.coeff recurrence4Scalar2First 229 = -((((156620062915992876864164357 * 10 ^ 70 + 5321527077818792035419211472803600337106511835498971566979021759002202) * 10 ^ 70 + 4650548587008875730323975620815924879592018118747403194146266725877976) * 10 ^ 70 + 9371682164144374349654875988062685912842372738346027947118097989222520) * 10 ^ 70 + 4336625168926428732226541785198550218503852718865305252962777540881986)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_230 :
Polynomial.coeff recurrence4Scalar2First 230 = (((209032507385703260322899197 * 10 ^ 70 + 5916513711022549577124911040072186420261449789395386440959441936004657) * 10 ^ 70 + 838403014519629064505536947793843744480865758266640502522432536791058) * 10 ^ 70 + 4296623705257329838895477621667644646743899027403427892044174181581387) * 10 ^ 70 + 2222223605468285977744022951368062695838207013677482071603537361168784
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_231 :
Polynomial.coeff recurrence4Scalar2First 231 = -((((274939187987268097577134605 * 10 ^ 70 + 9061339435967021827220790679095649267890297447073554826005610425807726) * 10 ^ 70 + 3932932053934581244281892419622031641850173178700489508114775641020034) * 10 ^ 70 + 4245632599680862341141996702604989600879951054392603865304437487193797) * 10 ^ 70 + 6629755427427240379078162812537242863653210171823092816503513312138042)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_232 :
Polynomial.coeff recurrence4Scalar2First 232 = (((356351391428846571829383708 * 10 ^ 70 + 85247423630771696833899162458628839871168427675876620635224224226539) * 10 ^ 70 + 1561967019486428274141328685992701069950953176155405690705348149760432) * 10 ^ 70 + 7296533166116420102612496459114078393108121734050246798812961949923220) * 10 ^ 70 + 5306107546022854578748523474934766451464328062073482511548839391207663
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_233 :
Polynomial.coeff recurrence4Scalar2First 233 = -((((455090230018128916212706796 * 10 ^ 70 + 314141608666961469059860691149883176546452698873373257761902807295970) * 10 ^ 70 + 7723752128589139813165736419718253568226276913087270142996196637103167) * 10 ^ 70 + 5241280874817025428507595812284099242899192835430316541694889973469064) * 10 ^ 70 + 9168139025941792450243129440868527721952417202032401078771566393524995)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_234 :
Polynomial.coeff recurrence4Scalar2First 234 = (((572594382231456766588969514 * 10 ^ 70 + 153753253937416025121508919709331280352736449852724614339935537645982) * 10 ^ 70 + 5846909286734347429684561628061130274713286773341459625961693040363618) * 10 ^ 70 + 3498082931675780704991821435456457072761061314821776682471962469092227) * 10 ^ 70 + 5851327525824927911358804416629806453746541574159644410947681423807514
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_235 :
Polynomial.coeff recurrence4Scalar2First 235 = -((((709699962731139355198373666 * 10 ^ 70 + 3125479108718790874114030031047846870252873966567107136749143843150482) * 10 ^ 70 + 4522281264799554815110567238616591364308744010617496855862416901229606) * 10 ^ 70 + 8918726703654774469275759468376460926515505577437349397164135070429436) * 10 ^ 70 + 8393179719531458334590496912406775610124298029897133783299491081209777)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_236 :
Polynomial.coeff recurrence4Scalar2First 236 = (((866406525944924555177135901 * 10 ^ 70 + 412639311150970936021038688798939601847369786457296156649369616939379) * 10 ^ 70 + 6002431172609203683838262832547185222585862600940829587672783454932633) * 10 ^ 70 + 4282027949688132492789259180287085741927433503649544956977608519174159) * 10 ^ 70 + 8124335865867481971379243482321942459176868909261296141741204424255720
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_237 :
Polynomial.coeff recurrence4Scalar2First 237 = -((((1041649143216617533601874208 * 10 ^ 70 + 7702958943315884287647323199190574121420343005926607217551991906654606) * 10 ^ 70 + 4753889387699237932822395356894064638916161359587641618796736897046587) * 10 ^ 70 + 2168176497689440870349083583570931323067287334197690414681588026422119) * 10 ^ 70 + 2516851428031015191179549494000261042837981263280770096099805048105504)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_238 :
Polynomial.coeff recurrence4Scalar2First 238 = (((1233101548437668503738407164 * 10 ^ 70 + 856595564905061631232750733481286768256665407617723266291194918838372) * 10 ^ 70 + 1121227197340350716737908677431862654523488438420316089009492211007661) * 10 ^ 70 + 728133156963652650173430135335523483149970777428384862680308766650497) * 10 ^ 70 + 6459561584405393416707513185303832331622270331986051218033460846932570
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_239 :
Polynomial.coeff recurrence4Scalar2First 239 = -((((1437038514858019344040235686 * 10 ^ 70 + 2443545431832096053222024954832593826592657188819315423534063139715782) * 10 ^ 70 + 2387127192999081692620430469904886828666049066921112988355646868160385) * 10 ^ 70 + 164195937017975109896157198041696262637827054105116247129794518846280) * 10 ^ 70 + 6079356825465060833454105378935727591533697011034444297387716709945275)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_240 :
Polynomial.coeff recurrence4Scalar2First 240 = (((1648285919412869266047619925 * 10 ^ 70 + 8713805443643998466536052095015221999252773934643131937816753523651535) * 10 ^ 70 + 9741606837053493237035167431010627931164822452679014879002036548884933) * 10 ^ 70 + 8802280797620478109263413309733166338990688107774640232481158201893410) * 10 ^ 70 + 9318589225896097163301683485302316226540619797204593562297773769528153
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_241 :
Polynomial.coeff recurrence4Scalar2First 241 = -((((1860283581930751958362105194 * 10 ^ 70 + 1501750838419572023727319581560023899866562103907698676163086314901273) * 10 ^ 70 + 9340823512159671842726402647813430474776257299585712780583994340655464) * 10 ^ 70 + 8863040808419628518586626647158251282717537186366847295002915654005564) * 10 ^ 70 + 5819890424551424673592897260972314605479459535600179130535805265440776)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_242 :
Polynomial.coeff recurrence4Scalar2First 242 = (((2065278535487233381859692151 * 10 ^ 70 + 5017057060762204499562477059454482430148587967483623822045544254620835) * 10 ^ 70 + 971689083141721030381805039562302450061876899532193930579599468081752) * 10 ^ 70 + 6944288861157130265106167190444256946576074839334759937122294335289808) * 10 ^ 70 + 8629653884386916434986260574806826462319669918206786629260762388375193
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_243 :
Polynomial.coeff recurrence4Scalar2First 243 = -((((2254655045615650545996717367 * 10 ^ 70 + 5767094324580463008548474553439456171010702724188247515605433799449411) * 10 ^ 70 + 4840097494437139345429756051802270117650895882478365720399697084641244) * 10 ^ 70 + 5757190698876543973195589151899776187255230090544006876109180867906778) * 10 ^ 70 + 9993431461085122928184461197706367203862845118183595580139614406083991)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_244 :
Polynomial.coeff recurrence4Scalar2First 244 = (((2419393259382966163679188345 * 10 ^ 70 + 3532044659263427359434533706998934004071859363393027238846242904769604) * 10 ^ 70 + 278706173860328651786494680505487316553604560257272335180162106344637) * 10 ^ 70 + 1538716237027858293091301935748217978931003883240578876245355911899967) * 10 ^ 70 + 5968978931808557721284596328250244943102714278768412336149874549960557
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_245 :
Polynomial.coeff recurrence4Scalar2First 245 = -((((2550632294730470008007678171 * 10 ^ 70 + 2728500684706056088049090816739060856124848267667403872408079075680108) * 10 ^ 70 + 6126771487072964214226304224388031108150926048685738364199173075186361) * 10 ^ 70 + 1973516142456010248201467567299744574356462407357092018831170890966537) * 10 ^ 70 + 9391099394408064214277270525282210012499798768400885292022624282779870)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_246 :
Polynomial.coeff recurrence4Scalar2First 246 = (((2640297873689708097729878250 * 10 ^ 70 + 2802901634950504742474564321658498876239799102674611144302119948406176) * 10 ^ 70 + 4273998695475590961249909033116573646534889472638838048747141438710297) * 10 ^ 70 + 644032437126068223785554018488194348564037565573549231813128152940896) * 10 ^ 70 + 3412225997576160179636436661462794192746442809031749114615685134124464
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_247 :
Polynomial.coeff recurrence4Scalar2First 247 = -((((2681741547870752980950100706 * 10 ^ 70 + 9265158976811070124928729764553514243352657005159872565077381779096428) * 10 ^ 70 + 9187020581600595217352631738539873953291321832044264019372660185069667) * 10 ^ 70 + 1167113908864913801811476215999402174316457898509112317843680500541127) * 10 ^ 70 + 3100757351882069350891506018259773223985665840383612089948425905839320)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_248 :
Polynomial.coeff recurrence4Scalar2First 248 = (((2670330399030223936246806548 * 10 ^ 70 + 5206830888257802689744677207977916387766754915922916379245445573923012) * 10 ^ 70 + 3652841184800831963242122932264554551350313172996613169885699241316647) * 10 ^ 70 + 6114908964549017402971133832026769901983657189830004729982515221762519) * 10 ^ 70 + 4837629758531480092399603147363753917343387313191582187060344603651731
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_249 :
Polynomial.coeff recurrence4Scalar2First 249 = -((((2603924624465504293563147265 * 10 ^ 70 + 9829421029659085340931753409733351444592887749786916963063713908407196) * 10 ^ 70 + 9912960673575216087217004003337812241647032386427579341528272767697533) * 10 ^ 70 + 8045624586772618898696327654746772005497544390175363212255992839325281) * 10 ^ 70 + 3022871026695349534587627003438372040604073019314033823363271587875906)