Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupA4SquarePart1.Coefficients253To284

Recurrence 4 lookup certificate: A4Square coefficient convolution #

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_253 :

Polynomial.coeff recurrence4A4Square 253 = (3334250186570544621330134459424936062695 * 10 ^ 70 + 1365642914120568709955954841996561192315049940443501524744020493620935) * 10 ^ 70 + 8892171425198616415680499600498661504149052057252028366445587770925068

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_254 :

Polynomial.coeff recurrence4A4Square 254 = -((1307424369779126776600925686421881005534 * 10 ^ 70 + 7231538897068108938789322819870093568795802602749443026836035311645980) * 10 ^ 70 + 7946700394089438610074641759910412507733010966040620289015975441742460)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_255 :

Polynomial.coeff recurrence4A4Square 255 = (496745582674089117666607219370469191337 * 10 ^ 70 + 1597278715026185124692445737934678945561106670498926000664243364059104) * 10 ^ 70 + 2706488513373146760588449396167535757164785986487327294514573279405050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_256 :

Polynomial.coeff recurrence4A4Square 256 = -((182752558064251318911874502804192682097 * 10 ^ 70 + 3736834581292419291420656036119288618057711710514643386020138037414463) * 10 ^ 70 + 9437015380529109675981557326154620576425926650292556885776285435952631)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_257 :

Polynomial.coeff recurrence4A4Square 257 = (65007007383412086367735723936935476798 * 10 ^ 70 + 9662611089418312747624184879602734725596686569083046628504878581217805) * 10 ^ 70 + 8698238459337009132349756374880349679568335087621790200655851857207338

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_258 :

Polynomial.coeff recurrence4A4Square 258 = -((22295104583538099814363591962019919249 * 10 ^ 70 + 1424863237821284784619420427366634535942303070462772977253966768265856) * 10 ^ 70 + 7559759012614211865089947630288293425897526169911443444847983220682226)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_259 :

Polynomial.coeff recurrence4A4Square 259 = (7334171452723174731146014079360866816 * 10 ^ 70 + 125978382959504597067814839512187395915514793498863362664943324220143) * 10 ^ 70 + 7577909518695966032947171713225010795242616041436098072408584079576142

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_260 :

Polynomial.coeff recurrence4A4Square 260 = -((2290867580753899267215172520636134469 * 10 ^ 70 + 2907822296986258418593987471610610123708437362523472196327337629908544) * 10 ^ 70 + 4402912408821580925960515963234514536977366939002110623249009866552144)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_261 :

Polynomial.coeff recurrence4A4Square 261 = (665166819272931587410741094221310527 * 10 ^ 70 + 7416063421358579756330377165313893199511596426883041110286292243344772) * 10 ^ 70 + 9582145180662193573835905177002351298983836120114375825878016192420266

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_262 :

Polynomial.coeff recurrence4A4Square 262 = -((170458667554407295520505928129163860 * 10 ^ 70 + 2429359770272207102889305070155813801150307332339984176006931379440410) * 10 ^ 70 + 4923849576166556023455161694652168512836105405508591308468297119384279)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_263 :

Polynomial.coeff recurrence4A4Square 263 = (32343209955751840269224398128175565 * 10 ^ 70 + 3966156552588713625613624366046719366396048088429609357518211258295674) * 10 ^ 70 + 4834350559079847170820194723995366926495289409235890677299496251423624

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_264 :

Polynomial.coeff recurrence4A4Square 264 = (424327842247054629122606528344247 * 10 ^ 70 + 2956897354526727039556405152279339230471395581528785080030128168415656) * 10 ^ 70 + 4603883038758783870797677745465982314531198607413327501891848558267855

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_265 :

Polynomial.coeff recurrence4A4Square 265 = -((5156434765122720605117203530084609 * 10 ^ 70 + 9643610314087882190183697372014130333169830756230998937318509477667722) * 10 ^ 70 + 9924427374790941143511516943066459586506160311723128033726534388002810)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_266 :

Polynomial.coeff recurrence4A4Square 266 = (3926986961067766470550426793556010 * 10 ^ 70 + 1161486613839964308525806215300343327325115192936365835096623729060572) * 10 ^ 70 + 3181105558000728180463220863705797508079537334430031107640641498664827

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_267 :

Polynomial.coeff recurrence4A4Square 267 = -((2264053692000016079092199177864114 * 10 ^ 70 + 174017694976982485987867841279579014824618437698688444732924851669480) * 10 ^ 70 + 5562147895332512023097829110429083162000191887708794145607685505776382)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_268 :

Polynomial.coeff recurrence4A4Square 268 = (1157890624054774037667119761868875 * 10 ^ 70 + 40844520168753960779614130053879855228073488239902382769447446607660) * 10 ^ 70 + 6076937046684130295197276011184184818398157550164320931957182239709672

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_269 :

Polynomial.coeff recurrence4A4Square 269 = -((550644677130346430402569767001389 * 10 ^ 70 + 8502545217100047341644197395825296025436406237639648255749199853730173) * 10 ^ 70 + 7295849693696514149744371264515360903570104213859558347638119584665176)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_270 :

Polynomial.coeff recurrence4A4Square 270 = (247918440393908032496062288544353 * 10 ^ 70 + 8881994330801484194631800991244827224183764096163661928720190902118182) * 10 ^ 70 + 9358556686925026661867085373413011873079548592098672873367494150545646

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_271 :

Polynomial.coeff recurrence4A4Square 271 = -((106398701128939315039237782857771 * 10 ^ 70 + 7374200466788896383918442549871848837313270040455460086933490785175778) * 10 ^ 70 + 9735079223596904357419695470048254168236551580166689271090446987987374)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_272 :

Polynomial.coeff recurrence4A4Square 272 = (43592530608905618360187516329307 * 10 ^ 70 + 2408147547096942175392759613382114161261831695877230597323258031885604) * 10 ^ 70 + 2876180190651664937321385319233217514308892555160121125500218671081093

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_273 :

Polynomial.coeff recurrence4A4Square 273 = -((17024560882164365378638021536230 * 10 ^ 70 + 3456696192245086027856059826688109515349839787091359051054544693638230) * 10 ^ 70 + 6179918376392574918768571816775847534020763465665751763481004279073376)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_274 :

Polynomial.coeff recurrence4A4Square 274 = (6313595267652041714267414899162 * 10 ^ 70 + 241993690662354807561082546704081874107523464595282902304389821482125) * 10 ^ 70 + 8350079805890920095943951191992427827565827650643567583734803376430814

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_275 :

Polynomial.coeff recurrence4A4Square 275 = -((2209544450645312787362870846500 * 10 ^ 70 + 5708189127529489478849469959835526005970831265466301706189464295625863) * 10 ^ 70 + 69652939985572293704122443571372554836564664277109233951834147419492)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_276 :

Polynomial.coeff recurrence4A4Square 276 = (722577472554235050082938608506 * 10 ^ 70 + 3775887527901364549921129380987940726424170237982345273130430874196577) * 10 ^ 70 + 3373891627297531773483570474773421130822307338946494187339008414239055

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_277 :

Polynomial.coeff recurrence4A4Square 277 = -((217215955554990834236777202409 * 10 ^ 70 + 2646356862113469060279649431721257025113227571147558399698569884379493) * 10 ^ 70 + 4767660983995530661790002899737793609578418268793299419312033337232332)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_278 :

Polynomial.coeff recurrence4A4Square 278 = (58186368348956106168888862718 * 10 ^ 70 + 9191682092688179667452230630317489875765623863933950907402351999092447) * 10 ^ 70 + 8393267785659121438264355260460151666374330561393560272747595026944948

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_279 :

Polynomial.coeff recurrence4A4Square 279 = -((12905931283503570123803351408 * 10 ^ 70 + 9675115328719241106117701239065243853307322559995838989447548090054355) * 10 ^ 70 + 6654199794177137893054266716335010079749968438496122826185023396361562)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_280 :

Polynomial.coeff recurrence4A4Square 280 = (1794557209716433293654742641 * 10 ^ 70 + 4969638033672432542154865183536163352113706601556875623619304218813293) * 10 ^ 70 + 3777809508752058976464882131064898402801653804979942920627630352224759

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_281 :

Polynomial.coeff recurrence4A4Square 281 = (244785599943422337929280395 * 10 ^ 70 + 6781484951184627586482320229335687926170149681698346614706191595003797) * 10 ^ 70 + 2037731931613561594563042561568510032898283860650635105648011826071954

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_282 :

Polynomial.coeff recurrence4A4Square 282 = -((326600351085050430358689152 * 10 ^ 70 + 521701596221820382243467582019039399564134987622052959885840025263386) * 10 ^ 70 + 8116325332156284113931686214603381843760013859405319404857999469798419)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_283 :

Polynomial.coeff recurrence4A4Square 283 = (167640772833160863247047263 * 10 ^ 70 + 4360305673167277817940981790743257446667037058393323873752334769314684) * 10 ^ 70 + 1502267367399127798402459602720354853915635015894945106144274782991822

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_284 :

Polynomial.coeff recurrence4A4Square 284 = -((65651846528189018273312465 * 10 ^ 70 + 222957886584490560603238205096307477561316492769620927048641016172180) * 10 ^ 70 + 6009413692020685033269394103124955285338477129407190935236817218499485)