Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupLeadingSquarePart0.Coefficients160To187

Recurrence 5 lookup certificate: LeadingSquare coefficient convolution #

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_160 :
Polynomial.coeff recurrence5LeadingSquare 160 = ((6425423949230125903648932755058402145995 * 10 ^ 70 + 9107689134863497149107474569475567152853703572552493817787060892285439) * 10 ^ 70 + 9692111443874336568255908785417525571781788632011298400222528559446048) * 10 ^ 70 + 1695695409855846280838571107239351117568182830899353138785888339600283
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_161 :
Polynomial.coeff recurrence5LeadingSquare 161 = -(((4439165227384909395979681134310705614880 * 10 ^ 70 + 4305518400676501655120854169873749122118460943762696606220395489244005) * 10 ^ 70 + 6077159183509387126332448532244942720789745414191976429761236269844895) * 10 ^ 70 + 7089561195275130943645016035595296673120443086303513342375978672454898)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_162 :
Polynomial.coeff recurrence5LeadingSquare 162 = ((2862948418876506653745801788398143558801 * 10 ^ 70 + 4342033863230452447010339467086881086871772187631164157894624294651610) * 10 ^ 70 + 6707406225299143557962287302084188272027718352585289411543086819439856) * 10 ^ 70 + 1104597810074096565192150631021927996120120782134180574478000319646749
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_163 :
Polynomial.coeff recurrence5LeadingSquare 163 = -(((1718760669647621934457635887627495546826 * 10 ^ 70 + 8010589723365189467712662890660231554153914974349373823223014157220859) * 10 ^ 70 + 6826436096434461271121827639866567359541582514959621843922423633577687) * 10 ^ 70 + 6620390704950750829584628062835901831109739496861602322838592626174502)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_164 :
Polynomial.coeff recurrence5LeadingSquare 164 = ((950360649181440196787856212102513960515 * 10 ^ 70 + 4922588523308735299202125901044942987429895923875629863193172503236119) * 10 ^ 70 + 7235924378117600869187492313142522813413437286979279745567607607703625) * 10 ^ 70 + 3529559605903812383817924124833149140331345148400672705753696155551413
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_165 :
Polynomial.coeff recurrence5LeadingSquare 165 = -(((472185808235271262756186925677547502532 * 10 ^ 70 + 988094917608214506573925474935877886002906680141254573053614710149737) * 10 ^ 70 + 7229153200723636308385539327574348138592983570809082928468330711985373) * 10 ^ 70 + 1024940422331961560406631149698721425176699147531766941869453546405162)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_166 :
Polynomial.coeff recurrence5LeadingSquare 166 = ((198473809856514260977179898504399251642 * 10 ^ 70 + 4664221899172317483702543756774539866296343774917064591659377727214819) * 10 ^ 70 + 5047820751052134299293664638875141825523225726188791213640090518221088) * 10 ^ 70 + 9470103012563412811990731853576447100913699281602289306409050182252917
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_167 :
Polynomial.coeff recurrence5LeadingSquare 167 = -(((57348314656454286510136904001766476954 * 10 ^ 70 + 7635818327874081938885181900985866615462079902096739492506268553936779) * 10 ^ 70 + 9347618081347566440576935883778225740629175710423182891998190751387076) * 10 ^ 70 + 1203163290567526117717258243248490922452043623183140855475767942977572)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_168 :
Polynomial.coeff recurrence5LeadingSquare 168 = -(((4850875657633937525174223265274474112 * 10 ^ 70 + 3661885233440753027850648712825927221966809664198476881890906254842307) * 10 ^ 70 + 4533014456819735322424291187878816535135525148758918899487301630641325) * 10 ^ 70 + 7273880548539815923683969208289868478661582884344339164704785869331003)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_169 :
Polynomial.coeff recurrence5LeadingSquare 169 = ((24615942181231766299028633526388173920 * 10 ^ 70 + 9561176326598032389717625834784555820885938745271096265097369547749113) * 10 ^ 70 + 3541754712078090031101573963006337363666933311634486150377849289219076) * 10 ^ 70 + 9861906952212343740275334104439705744005616834237670203744920524348488
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_170 :
Polynomial.coeff recurrence5LeadingSquare 170 = -(((24647256487682943410519813583641724372 * 10 ^ 70 + 1111040886867031015905937880231415460607001789474983736284642829085845) * 10 ^ 70 + 9806290932125339572595383447102674766996408875649768634767002196825975) * 10 ^ 70 + 9175458875277999246537784248988738926649355122780990078619021555532972)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_171 :
Polynomial.coeff recurrence5LeadingSquare 171 = ((17723699993655050235792702262561538657 * 10 ^ 70 + 2422709063100780003144839402528979125599548729391550640337406032380337) * 10 ^ 70 + 2789388522391368185123376393371781940632992389093782968735470102228561) * 10 ^ 70 + 1743229797830557100652799772065644868162926124911655020653810528872274
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_172 :
Polynomial.coeff recurrence5LeadingSquare 172 = -(((10136771069821366023074794745634793513 * 10 ^ 70 + 5443428216379032827218174770543859577710606924683670152865447569029513) * 10 ^ 70 + 3639660650627585271536311273721521695590355069527122567961039597957641) * 10 ^ 70 + 6798693109361303826513180862217053931991634917379503490626532955536119)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_173 :
Polynomial.coeff recurrence5LeadingSquare 173 = ((4337847301530408592354699196359107953 * 10 ^ 70 + 6769084747528890704401761030870446837386104295742300863825961385452838) * 10 ^ 70 + 4984119648767122936746765772398155789943809095884195316789890933222975) * 10 ^ 70 + 8066341704349482871163850270409758540159506919102501152740603555633830
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_174 :
Polynomial.coeff recurrence5LeadingSquare 174 = -(((772501120042886170381660363928076186 * 10 ^ 70 + 7033381953269621392031931799538442093595975730160531758533088811658295) * 10 ^ 70 + 6093341422210669211651973145106379831170017344382360881639973671719575) * 10 ^ 70 + 917239562732953543710203152307014276464243152038167645578757776469335)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_175 :
Polynomial.coeff recurrence5LeadingSquare 175 = -(((971586699118649096533545109847260902 * 10 ^ 70 + 7247387351601115832200636951463816346319223483864751683129026636786115) * 10 ^ 70 + 5555701086910947793832710380306527883253768686527126024821765346456457) * 10 ^ 70 + 6096273620797176604049789593774549946380982625488903490368168588952876)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_176 :
Polynomial.coeff recurrence5LeadingSquare 176 = ((1527084401301375530812756696332130064 * 10 ^ 70 + 7165409391883242628920857401336100436389924952632070968389870348643091) * 10 ^ 70 + 4741987304383025039222702276706531217681563622772267367260186084831545) * 10 ^ 70 + 3487430522570172171158383404427286751508510317942296675439722981980879
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_177 :
Polynomial.coeff recurrence5LeadingSquare 177 = -(((1449794278216691863206650677442525486 * 10 ^ 70 + 1755825257447273795969817556793885648245126127830486568632214670525352) * 10 ^ 70 + 8686466292939333499053130658846037868278792193167565833312307578357528) * 10 ^ 70 + 4974187613406874241846333192644480624735359556392183766044137517477004)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_178 :
Polynomial.coeff recurrence5LeadingSquare 178 = ((1123123947603098363254553577225348750 * 10 ^ 70 + 5519246331098613678920585601862659273095777067364448702800470929307197) * 10 ^ 70 + 632373757505121453589629101136792795864568457899393004367174919760126) * 10 ^ 70 + 7795760738909128126333830361997867966544183035428770420967691888760616
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_179 :
Polynomial.coeff recurrence5LeadingSquare 179 = -(((764495114649890410957690948906132155 * 10 ^ 70 + 4113204358121422032546275255887848955746926390718993983937963880804406) * 10 ^ 70 + 7924773051677050131734033525006201510919380757869296223071534313767912) * 10 ^ 70 + 4502380407099773523545544399637704346797796373518315887734878763299960)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_180 :
Polynomial.coeff recurrence5LeadingSquare 180 = ((470240981518705010352951422111349966 * 10 ^ 70 + 4195325043993749746927302253358838779840727075232260761594831597735088) * 10 ^ 70 + 9936872674722504249308553894983483162970436495133542600197117576890675) * 10 ^ 70 + 3451823172165493800332335695638856520070621007843943167646564419812948
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_181 :
Polynomial.coeff recurrence5LeadingSquare 181 = -(((264329563572976696963147303246285676 * 10 ^ 70 + 8123569060404396708844396919642970846779238537128699460264242951530834) * 10 ^ 70 + 2086593299171644101847355594512204553922942053249266422709049112777511) * 10 ^ 70 + 891619002008047795728002564328133279047363764795413330748531375361494)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_182 :
Polynomial.coeff recurrence5LeadingSquare 182 = ((136094685096977444854166396467567873 * 10 ^ 70 + 6115575661953175521698109038307176765239539961016235293763834271492079) * 10 ^ 70 + 4122839101605423350098952092997367887833479199314167013152312074639062) * 10 ^ 70 + 8475245818269039747663641128604509013762952199817834129477970362397775
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_183 :
Polynomial.coeff recurrence5LeadingSquare 183 = -(((63868093960684847454282813095694700 * 10 ^ 70 + 4397053136926962208643106089697223298995707036462979393509930588388571) * 10 ^ 70 + 2093101928877046340501684548125957689274299748555280011306530787929242) * 10 ^ 70 + 4909790030153828021272485981672953897513694813127827871761808744980768)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_184 :
Polynomial.coeff recurrence5LeadingSquare 184 = ((26945838065508253792564806073219029 * 10 ^ 70 + 5561008263949047550841438856291961932595339515462800613769412953949822) * 10 ^ 70 + 9714171260973356925688032651557874633748403025531513092972643466945980) * 10 ^ 70 + 4554749183260100408068992549168305880333192115880746955349797618333052
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_185 :
Polynomial.coeff recurrence5LeadingSquare 185 = -(((9919408325809655371983712446302507 * 10 ^ 70 + 3098056648336627284983651009600198545955780441747063762290043158737618) * 10 ^ 70 + 6505388120873342234367750058959592504618518071433468827664640147408410) * 10 ^ 70 + 3861636299944094868397022411197130988548070871260037334287272277637800)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_186 :
Polynomial.coeff recurrence5LeadingSquare 186 = ((2967448466249035428556383489000030 * 10 ^ 70 + 5188162915108352378794413492229904467090873386884842174139402114581264) * 10 ^ 70 + 5503229074058779638023591381437701088270798720012862172136849110554) * 10 ^ 70 + 2905538545933122631318885923117277407730732967089871148836053253452339
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_187 :
Polynomial.coeff recurrence5LeadingSquare 187 = -(((563156535326957223376422444119698 * 10 ^ 70 + 397985797411772127885081147308318211148351617090766281018658582266438) * 10 ^ 70 + 4034463789857273957313605882886127629991564967811390066885978346157137) * 10 ^ 70 + 2949162906072418599531817932887482913151126633070603884387941886157710)