Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1ExceptionalPart2.Coefficients360To382

Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_360 :

Polynomial.coeff recurrence4Scalar1Exceptional 360 = -((((9338 * 10 ^ 70 + 3261254314628054523021829557110196966750550057293192522769364739612186) * 10 ^ 70 + 8310327363483544705881590126530024630876934343909808514164284026840074) * 10 ^ 70 + 9256095209076598469846314005563918024396934472658396646016602089172793) * 10 ^ 70 + 9533427029520305650079858446883736472397384314884034660743374795620946)

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

Polynomial.coeff recurrence4Scalar1Exceptional 361 = (((3233 * 10 ^ 70 + 2874210103881027202435304172486999140522753686800794834093130427224629) * 10 ^ 70 + 6955715443984568546916196254241761558777276705273247687643812471933075) * 10 ^ 70 + 280608966501642660892481681576182888568259484256220418585513546888178) * 10 ^ 70 + 9929899691360070199697754920959883790443390776543396369806393848644640

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

Polynomial.coeff recurrence4Scalar1Exceptional 362 = -((((1063 * 10 ^ 70 + 5249056201281744760275717010896938634479590212223120835382222038239118) * 10 ^ 70 + 1323221366865851445301278645897570206584945349206828486888072110298191) * 10 ^ 70 + 2720687165390902890041305433567684750193409268773753376808211137991309) * 10 ^ 70 + 7824829457818677613808078215990115921414450976275516421436633742651690)

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

Polynomial.coeff recurrence4Scalar1Exceptional 363 = (((326 * 10 ^ 70 + 2025582543476069575931930355015581854831193984081890350188596356066913) * 10 ^ 70 + 6722033192139229516541136419497651498555966850403567666338674439311511) * 10 ^ 70 + 7721795513803744628444009714720029902814352530872333141472114707397191) * 10 ^ 70 + 2610904834625079692251189722910848274658588102428057854799991462315045

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

Polynomial.coeff recurrence4Scalar1Exceptional 364 = -((((89 * 10 ^ 70 + 5510138895895699561640806266743409114250294054727159921425966696399820) * 10 ^ 70 + 7323268306238071928567036198930738148200508883728122747792734705553379) * 10 ^ 70 + 3290337871432009694642902365599699135736323252270760944480287827937228) * 10 ^ 70 + 5534715584505578378486114263528814656995980157896655032913652308697441)

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

Polynomial.coeff recurrence4Scalar1Exceptional 365 = (((19 * 10 ^ 70 + 5325134345780802259849257304341058374711823886251328758199945287267524) * 10 ^ 70 + 3193805410022875561909885305412865121647881236862705230441964498249422) * 10 ^ 70 + 8994589320383403692715072260644332917204908272082804259607195847663610) * 10 ^ 70 + 7564588044708827458933564989162347807085621921130152319621749474874741

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

Polynomial.coeff recurrence4Scalar1Exceptional 366 = -((((1 * 10 ^ 70 + 5128743315695287713186368569607847553104734850984514545839318544733238) * 10 ^ 70 + 5566773276648736786958341400747604323902836923812983233584144518972657) * 10 ^ 70 + 939455256300665367624253854943671232711897177353676404095983836613315) * 10 ^ 70 + 3539265449626840701484939590754562872750869874615410904351376087105703)

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

Polynomial.coeff recurrence4Scalar1Exceptional 367 = -((((1 * 10 ^ 70 + 7796832809661783847714579448735735517376209843099687846041355565111358) * 10 ^ 70 + 7459599795620751968127381267911769186695313691905600050535830326777902) * 10 ^ 70 + 5839851135007745284361198683837527809042181781033712836330187733334470) * 10 ^ 70 + 445870928862988515864099491404757144933836561258226087751573321475979)

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

Polynomial.coeff recurrence4Scalar1Exceptional 368 = (((1 * 10 ^ 70 + 6004845870171700904850279026247375560859055817785568484024066045202399) * 10 ^ 70 + 3995591748570273112208135796693612865655083851281976356218052451535252) * 10 ^ 70 + 8916843113738174091558420933085087577774854130798703319839323349361591) * 10 ^ 70 + 3402989592753341141620469367857974823094121997901004666264395935296103

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

Polynomial.coeff recurrence4Scalar1Exceptional 369 = -(((9673735015895763794632328272203612405270846227820966138073634843822976 * 10 ^ 70 + 2049108783558268270207866713731327661269715578942194610041372565953074) * 10 ^ 70 + 732664115778743503476385214194962824072582260766534087560581492504446) * 10 ^ 70 + 4462129441393284945401573933438415271331950723178873658703164155274414)

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

Polynomial.coeff recurrence4Scalar1Exceptional 370 = ((5060295351764261427115721359061479645209915341772905547136019275992204 * 10 ^ 70 + 8442783638669295920761111449853293157219898414232487344229264670168633) * 10 ^ 70 + 5538734989504458187514829822757808664449809407491691780364741932345929) * 10 ^ 70 + 8712719440515873642454626239925172004044942907564060839527926579269663

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

Polynomial.coeff recurrence4Scalar1Exceptional 371 = -(((2450400881246336126743943643431664173417710899428042033916140698749456 * 10 ^ 70 + 9946199170780872530248039448937928500110627772608352060491247081088076) * 10 ^ 70 + 473670923988825520531427804804183406877470439457645536384787950750827) * 10 ^ 70 + 9432766920223989460841533382753035690463352239730442219543622464658801)

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

Polynomial.coeff recurrence4Scalar1Exceptional 372 = ((1128374236491658342061114212005907551418260129795465043282151805073601 * 10 ^ 70 + 7510777008297573843917174816036828269706340488565291171650962807088257) * 10 ^ 70 + 9682262072898298983269795295882784257377153683906687043768220423865471) * 10 ^ 70 + 8160709174987997845208596579433932344034156464304783448875984192709744

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

Polynomial.coeff recurrence4Scalar1Exceptional 373 = -(((500201204403585630359838139518939424883766000400478289888301618757444 * 10 ^ 70 + 7546249909292678433312651975514256414816859550055347068716537243890618) * 10 ^ 70 + 3145020542686121055295930183164361346441962085704570834161674001172990) * 10 ^ 70 + 2033403573956889733330340905907866098571223608424349843581209981879866)

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

Polynomial.coeff recurrence4Scalar1Exceptional 374 = ((214626093688518059438017211451530616657489872125541398892544544249912 * 10 ^ 70 + 4576067261154120758273474806685402033542399263019988723370754003801915) * 10 ^ 70 + 3196748643701608694902520570804552519985173925887817191893154037455573) * 10 ^ 70 + 6706808140254365787714717351658378087401531468193980452257485958522363

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

Polynomial.coeff recurrence4Scalar1Exceptional 375 = -(((89299701045799645013895468969660524328668125271682754989055872290012 * 10 ^ 70 + 2989095564442020552645489084930162456059773195897549406215503093909614) * 10 ^ 70 + 1615003906534050443274040385126199024847295611649731582823265139404696) * 10 ^ 70 + 8586347043146032292818735347335464887615979352652456692000845036850997)

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

Polynomial.coeff recurrence4Scalar1Exceptional 376 = ((36014924033741463364435427390356483301658719124580542689601701568791 * 10 ^ 70 + 4377557690453167106962876169440487961064199880597698931588614237843762) * 10 ^ 70 + 2597430390390391864474383729783932968183376711755192631669864644334666) * 10 ^ 70 + 3435890922387900843970758173151993729554340617622586746181429715970754

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

Polynomial.coeff recurrence4Scalar1Exceptional 377 = -(((14053253501468797426241601724513341651014841574569634773220900379381 * 10 ^ 70 + 4864380470454688229279859565939545569018529639552395446388733961060342) * 10 ^ 70 + 6990017508230490798738310403025295109312089891194811356287447274808301) * 10 ^ 70 + 6760413150722463550932057366422804461097395771445641817185323899321181)

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

Polynomial.coeff recurrence4Scalar1Exceptional 378 = ((5289420272725199184226421489904075992044184223183230667215659746936 * 10 ^ 70 + 8975722493132312838108676238438280154450807757839784187838963782160650) * 10 ^ 70 + 5253189455069377848246083646042519772625227887876599739842909934957400) * 10 ^ 70 + 4384528097780627009770820349876646828331567998087103254796062370511412

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

Polynomial.coeff recurrence4Scalar1Exceptional 379 = -(((1912017810631492468323058372591987731642076648082403539931707620080 * 10 ^ 70 + 6273807964601144064329395014748613100369854905811501311217489682645839) * 10 ^ 70 + 7406009621769920956495864647697609736729792913783295007246367062457459) * 10 ^ 70 + 9491088791073373212520388204475895338171533311658300068768500749433490)

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

Polynomial.coeff recurrence4Scalar1Exceptional 380 = ((659734121039728085180097221952101661336647704624497346323990998735 * 10 ^ 70 + 1188998150132435118925782612491729617728755550989358440527050048878806) * 10 ^ 70 + 737536064283986820689901586774929977113471751937943572997911743070950) * 10 ^ 70 + 4459554628328935814539740938716358198790557948944846812812386611537137

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

Polynomial.coeff recurrence4Scalar1Exceptional 381 = -(((215319689293408322001758653740023008124377095802080510214547200234 * 10 ^ 70 + 3584005357379339135248089170966200370483713270102387077009161333282830) * 10 ^ 70 + 8849344127181712224775288812480393377417500255841415470113801310724236) * 10 ^ 70 + 4737136135391745735981421797860706551768489271017424201768839561925383)

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

Polynomial.coeff recurrence4Scalar1Exceptional 382 = ((65490488871895209253048086667787864506020495951695019152158882907 * 10 ^ 70 + 1589160243980865769373071388437149788723598917945921228309087443025178) * 10 ^ 70 + 3556095096093366551183209434852477485560008741546849347421350915746429) * 10 ^ 70 + 8910078003939086557890000724332326231024309016025536666425337499648759