Recurrence 2 lookup certificate: Scalar0Exceptional coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_285 :
Polynomial.coeff recurrence2Scalar0Exceptional 285 = -((9031232310568192897131610957578057198865019450 * 10 ^ 70 + 2662371373671294440274674428674269108397055956142748752155058926769049) * 10 ^ 70 + 7608449550739387918509485329317118674558178599646699118188875957996879)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_286 :
Polynomial.coeff recurrence2Scalar0Exceptional 286 = (3477257079003777260064689037241071226900479260 * 10 ^ 70 + 6095479396473462921932381510295652267809260132587383921198669092308462) * 10 ^ 70 + 7858914435787439795741445636255729333234560058204688745758693639694881
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_287 :
Polynomial.coeff recurrence2Scalar0Exceptional 287 = -((986275830818298752758092396506938294725165949 * 10 ^ 70 + 5634176197444832250829302094734285377117475798383179538302867860109845) * 10 ^ 70 + 9220014701956661578098856281207397712063949328524514589173784713174708)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_288 :
Polynomial.coeff recurrence2Scalar0Exceptional 288 = (103850703629986681979282755359676384366684092 * 10 ^ 70 + 5596555828303277517139198072472081587117172196145451666234070783467908) * 10 ^ 70 + 9757008319189099139296390023131492428869450348526069389520495913318783
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_289 :
Polynomial.coeff recurrence2Scalar0Exceptional 289 = (100661751106653770208312736912618390366410038 * 10 ^ 70 + 7495907397546604558727506657402136591691156522505803730563662522087096) * 10 ^ 70 + 333593146892745385523690800375432841084639549877943100050005595777577
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_290 :
Polynomial.coeff recurrence2Scalar0Exceptional 290 = -((91217586290464130543062067134602829982008443 * 10 ^ 70 + 4471209121708100428812089915851868167275703882058793971280854146557444) * 10 ^ 70 + 5230797157591983674153969606999049861192196358706057451226798154098679)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_291 :
Polynomial.coeff recurrence2Scalar0Exceptional 291 = (47903544903716036279216274404310002323703278 * 10 ^ 70 + 4154938504842652253166472969777628014886024867747404867168961424166909) * 10 ^ 70 + 8805630597305702067368711106284803157583361399726483135687383930625474
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_292 :
Polynomial.coeff recurrence2Scalar0Exceptional 292 = -((18595438731048746520761380851909616899031612 * 10 ^ 70 + 5495310638448737661057883975102574746030906298841309810790551072767011) * 10 ^ 70 + 4831013470547463962251017780513033270705874698485280474646089386716687)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_293 :
Polynomial.coeff recurrence2Scalar0Exceptional 293 = (5271779662193762877330367265046517329799434 * 10 ^ 70 + 5427889256990116159752114690984952586223946682102525878947802225218057) * 10 ^ 70 + 1898876802353891133302084449323078667903459119330077056848327629678256
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_294 :
Polynomial.coeff recurrence2Scalar0Exceptional 294 = -((794523697022878238783776881660381150954330 * 10 ^ 70 + 7284522775989033209640218057276114916889567933207312218413715595459812) * 10 ^ 70 + 1532126486036928427063551416924358409669439940687286378457950174480554)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_295 :
Polynomial.coeff recurrence2Scalar0Exceptional 295 = -((198203704580831704598501712582600197177937 * 10 ^ 70 + 2623216497966687838509697371019125596890166890831417372336403916590900) * 10 ^ 70 + 760033362882206157288525575316036479882249296198776181306236709339660)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_296 :
Polynomial.coeff recurrence2Scalar0Exceptional 296 = (215748273008172603621773961899480104855558 * 10 ^ 70 + 2485234301596296015964767060648101316398562402442504050237575935649864) * 10 ^ 70 + 2817199018859368089769956584969745669279272075654846788614137199207480
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_297 :
Polynomial.coeff recurrence2Scalar0Exceptional 297 = -((100692873916926646330089868069434533161361 * 10 ^ 70 + 5529700539999993557873720901575870089476083147863123012555643205116964) * 10 ^ 70 + 2011616498177950290705961948294610954475941588076903873321426782271163)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_298 :
Polynomial.coeff recurrence2Scalar0Exceptional 298 = (31950088344221728331244176872123347775449 * 10 ^ 70 + 5299048596238384920926540688202158934586499668657283361439796694303106) * 10 ^ 70 + 1340587463618238639936696356966238421607444062079018297218386822218763
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_299 :
Polynomial.coeff recurrence2Scalar0Exceptional 299 = -((6538342611127800872809271026431956234167 * 10 ^ 70 + 2792743386416239208887967765063396248482801432409480640915075426036644) * 10 ^ 70 + 3424164830566510864224150598657292604170879616501940518535313476292325)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_300 :
Polynomial.coeff recurrence2Scalar0Exceptional 300 = (195346873959921214974951757954154271113 * 10 ^ 70 + 1607528453295162297085808654324438265477703552488520205101835019975345) * 10 ^ 70 + 6664298938202483918145487706669106283553679420179065478560060169913319
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_301 :
Polynomial.coeff recurrence2Scalar0Exceptional 301 = (524088084362626649751119389742499092420 * 10 ^ 70 + 9956310096478604304268089175870979376546918729522970983261498996295996) * 10 ^ 70 + 7809131425629601236038630738740811445958867164135083967823506525852527
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_302 :
Polynomial.coeff recurrence2Scalar0Exceptional 302 = -((272293275653152659394566600786884558945 * 10 ^ 70 + 2897486058980761110957307644528768819622109518901978403694546134688495) * 10 ^ 70 + 8980706938189558512163728404069629099417745553698420195262383193788393)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_303 :
Polynomial.coeff recurrence2Scalar0Exceptional 303 = (82962591607376042739630291343450871259 * 10 ^ 70 + 3779109103804788843966776640860806357351239735177821068822013777481237) * 10 ^ 70 + 8844982610309197570766560094758787220342387066632703543488691702913680
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_304 :
Polynomial.coeff recurrence2Scalar0Exceptional 304 = -((15525885817255860421272834562664625061 * 10 ^ 70 + 2732770046042193445143300246195695767380951876791326364552053100373210) * 10 ^ 70 + 8776690490029578691308798137841629086871530083458131722163171321968608)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_305 :
Polynomial.coeff recurrence2Scalar0Exceptional 305 = (426122416542210317160255980390437656 * 10 ^ 70 + 108906338716468382509756635196492258230581715368625470085966091559292) * 10 ^ 70 + 3616215521972990692748227173661311015465488313882879476285291522612644
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_306 :
Polynomial.coeff recurrence2Scalar0Exceptional 306 = (944606842636181125558460104942465837 * 10 ^ 70 + 8185476352513757009266797602350928494235115624177354222318509114701514) * 10 ^ 70 + 9421853854548005642767708925159626467285490903447112184580444400185441
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_307 :
Polynomial.coeff recurrence2Scalar0Exceptional 307 = -((411696224307459583803238131256290741 * 10 ^ 70 + 8182973858416140219153691222650716096493821345630323581138935581872638) * 10 ^ 70 + 8572859317881720392472504468549391090226855350325059228126110866904305)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_308 :
Polynomial.coeff recurrence2Scalar0Exceptional 308 = (99434259403802749164378602763887267 * 10 ^ 70 + 7170035148039052319025121947236304447322443504285379808295445405591430) * 10 ^ 70 + 1410043848723277539288591596521761956006704820850653388322298365504199
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_309 :
Polynomial.coeff recurrence2Scalar0Exceptional 309 = -((12190566843226861165395506277678649 * 10 ^ 70 + 5505003720308630404880990305220618047048735927870662792270541818654341) * 10 ^ 70 + 5134196617561270954575450100737261715161136602995627947783200507610872)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_310 :
Polynomial.coeff recurrence2Scalar0Exceptional 310 = -((1305617410328489646504263538053352 * 10 ^ 70 + 4544752423295079043346673483604158094172882242815036534286300918557696) * 10 ^ 70 + 3818201367311048955288348304712251590713382348161852392946272142572007)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_311 :
Polynomial.coeff recurrence2Scalar0Exceptional 311 = (1101622057683942146512656942553104 * 10 ^ 70 + 2337372735550455929594088210047941481070829327955075358841828471022175) * 10 ^ 70 + 7401141827765621376617205228678533106316732087319622748197714726705463
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_312 :
Polynomial.coeff recurrence2Scalar0Exceptional 312 = -((295656816215071070914874682356595 * 10 ^ 70 + 6879101434023321750369482856104792505803201698657724141673237385949718) * 10 ^ 70 + 8033388181600019908924709544598112590028994458310253387742267906563791)