Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3ExceptionalPart0.Coefficients0To90

Recurrence 2 lookup certificate: Scalar3Exceptional 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.recurrence2Scalar3Exceptional_coeff_40 :
Polynomial.coeff recurrence2Scalar3Exceptional 40 = -(431443954653152420563 * 10 ^ 70 + 4796909451469152615575843165328908308313042917208630865941587774163779)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_41 :
Polynomial.coeff recurrence2Scalar3Exceptional 41 = 9229763319288110490663 * 10 ^ 70 + 1962008020962622604602549728206997713459941917764585898127762128245337
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_42 :
Polynomial.coeff recurrence2Scalar3Exceptional 42 = -(227528212549356724438737 * 10 ^ 70 + 5291746611933950903684932213066334531256560013757951095579433293750019)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_43 :
Polynomial.coeff recurrence2Scalar3Exceptional 43 = 6537249361641912455194705 * 10 ^ 70 + 6132376635862155310633500807344018723006629304098788022103989625483326
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_44 :
Polynomial.coeff recurrence2Scalar3Exceptional 44 = -(192851428725022920951978391 * 10 ^ 70 + 7460859522539911940120698639608337018530420454257961034748133131145990)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_45 :
Polynomial.coeff recurrence2Scalar3Exceptional 45 = 5395285126489414259761535406 * 10 ^ 70 + 9848425504348886837932007596736804277098605540954793158616994434176783
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_46 :
Polynomial.coeff recurrence2Scalar3Exceptional 46 = -(141454276058134377148554738909 * 10 ^ 70 + 5008832347070624592636862960092887264387946885647751754421282957552730)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_47 :
Polynomial.coeff recurrence2Scalar3Exceptional 47 = 3508351137907481780743971116933 * 10 ^ 70 + 2697774832565411369227817176115863399232022600714780615931975455933649
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_48 :
Polynomial.coeff recurrence2Scalar3Exceptional 48 = -(82754316076907696086964946724393 * 10 ^ 70 + 8493742158618495734572183252209634611044960155471405032064820267573333)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_49 :
Polynomial.coeff recurrence2Scalar3Exceptional 49 = 1853099325599491923401445727790526 * 10 ^ 70 + 5942291831247405698239436281653858053902063175826951610388095390064526
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_50 :
Polynomial.coeff recurrence2Scalar3Exceptional 50 = -(39276969252355478511421320639970583 * 10 ^ 70 + 3437367281069073803782027135938069022418354761840954221324947054837883)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_51 :
Polynomial.coeff recurrence2Scalar3Exceptional 51 = 788202338611073381309350026994312946 * 10 ^ 70 + 2496527259762875529900828822447841199983784380393013807099357122642095
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_52 :
Polynomial.coeff recurrence2Scalar3Exceptional 52 = -(15028725028822301980770718942398656047 * 10 ^ 70 + 8271578083576077955732435022785066496095072488241341248422375648176846)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_53 :
Polynomial.coeff recurrence2Scalar3Exceptional 53 = 273417393540706798692346975570442251797 * 10 ^ 70 + 3231996332099408598287844811583298964288278668136123928868122188502761
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_54 :
Polynomial.coeff recurrence2Scalar3Exceptional 54 = -(4759481131049642638820512178811628165979 * 10 ^ 70 + 5827785512514437654150940263421162351752143286789839719017112049803304)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_55 :
Polynomial.coeff recurrence2Scalar3Exceptional 55 = 79345850908930736016925441929590898579860 * 10 ^ 70 + 8884725425224782296809645509627561268118401513006053732623667993223749
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_56 :
Polynomial.coeff recurrence2Scalar3Exceptional 56 = -(1266843537822275020315016858278783407708436 * 10 ^ 70 + 2248969091635913332600063280891990530218426428162764829287186353467650)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_57 :
Polynomial.coeff recurrence2Scalar3Exceptional 57 = 19374548887960313750242055310362050511524740 * 10 ^ 70 + 566392536599242250247477209456348170870526245778909824973828499313036
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_58 :
Polynomial.coeff recurrence2Scalar3Exceptional 58 = -(284034649221229124044668719361846481577878309 * 10 ^ 70 + 3350185563448747393246477034989079343755477645579810868896678725250795)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_59 :
Polynomial.coeff recurrence2Scalar3Exceptional 59 = 3995728028427471121938026235403500220411874879 * 10 ^ 70 + 9388813423103861626358484770976178408907958437167286687100206162591593
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_60 :
Polynomial.coeff recurrence2Scalar3Exceptional 60 = -(53990040688159790523317379639798854490464723608 * 10 ^ 70 + 9019311502765837376540022399413977081426340509050526370433658462001107)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_61 :
Polynomial.coeff recurrence2Scalar3Exceptional 61 = 701167869500627533982704630568002751707235133148 * 10 ^ 70 + 7797043529132170859563375086801958271125080253521695323294875907539556
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_62 :
Polynomial.coeff recurrence2Scalar3Exceptional 62 = -(8757261616050230874323769202331441119197206913164 * 10 ^ 70 + 7668770696322432011120948281777569456072224403569376585098182550487069)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_63 :
Polynomial.coeff recurrence2Scalar3Exceptional 63 = 105253001866272951857596891973897259714749733406411 * 10 ^ 70 + 5455689885326807296190388416583774925580945007870276216286149734145619
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_64 :
Polynomial.coeff recurrence2Scalar3Exceptional 64 = -(1218301812486672012965562299064242175384261920533641 * 10 ^ 70 + 1663871154355467601472749948730541554137267980526830423601803172379707)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_65 :
Polynomial.coeff recurrence2Scalar3Exceptional 65 = 13591430957963634461999420112359855951983020264055351 * 10 ^ 70 + 605941098084248228562137308165585670256497566295462105027645908660256
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_66 :
Polynomial.coeff recurrence2Scalar3Exceptional 66 = -(146233349241563376785662306038196932087803714094789634 * 10 ^ 70 + 6716817261518028544937514862839423239345517899338427956050790789747867)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_67 :
Polynomial.coeff recurrence2Scalar3Exceptional 67 = 1518172358974766035568343918606267826971093541267233342 * 10 ^ 70 + 1914782466406741378672097230096869207957192571844876335209180548161443
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_68 :
Polynomial.coeff recurrence2Scalar3Exceptional 68 = -(15215907591346969784669095801338981250852787842795872464 * 10 ^ 70 + 910668799902200287125298834299769651891996427906657664527423977424243)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_69 :
Polynomial.coeff recurrence2Scalar3Exceptional 69 = 147304377514263396950415787525128362325948239390077157968 * 10 ^ 70 + 8922758335059103965410606172396562677241954148499498527508041397195816
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_70 :
Polynomial.coeff recurrence2Scalar3Exceptional 70 = -(1378301291176088622829405840608952367374855022386238450595 * 10 ^ 70 + 4280535942959036100945890142067437333887898458501787865536914211584946)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_71 :
Polynomial.coeff recurrence2Scalar3Exceptional 71 = 12472287639187175385751248744125095372709362291938038702885 * 10 ^ 70 + 7798976626536012659197421467876757326538604108588913468422682314881585
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_72 :
Polynomial.coeff recurrence2Scalar3Exceptional 72 = -(109205130932050816110223777607104489837451462094143399621759 * 10 ^ 70 + 8392062758053472597098399391135270175499487593920372130112624336846671)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_73 :
Polynomial.coeff recurrence2Scalar3Exceptional 73 = 925591773157692507657953561838060640066559334429112799622803 * 10 ^ 70 + 5623568157682876984058294257725023841306365486309947529155025926012817
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_74 :
Polynomial.coeff recurrence2Scalar3Exceptional 74 = -(7597293928053430810413495655055320908438809481462288663038789 * 10 ^ 70 + 1769803347274577769464105253924145360706633908810799180706930887825452)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_75 :
Polynomial.coeff recurrence2Scalar3Exceptional 75 = 60418764344997076839973682324379080041492107690984537055849776 * 10 ^ 70 + 7022324782976387603524070505000108109610238477187746732309154271325602
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_76 :
Polynomial.coeff recurrence2Scalar3Exceptional 76 = -(465784726825751744057457535379440887261746638638802635833236708 * 10 ^ 70 + 5634622118114656950086891643137169679573430757477114101914562314144958)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_77 :
Polynomial.coeff recurrence2Scalar3Exceptional 77 = 3482609769930001763965017495255034568848332215380143613637188059 * 10 ^ 70 + 225016788555030794106704717211060487315220677968059381853141475542488
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_78 :
Polynomial.coeff recurrence2Scalar3Exceptional 78 = -(25263404598414125157642168358765753705700529195544295527163043989 * 10 ^ 70 + 9515052111930776987406240859589547968599958674527138981901437339688758)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_79 :
Polynomial.coeff recurrence2Scalar3Exceptional 79 = 177862617894007227529947905062040198044624712482473279655262328696 * 10 ^ 70 + 5674329235166124720153535578284283380206644805935149751480176676154564
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_80 :
Polynomial.coeff recurrence2Scalar3Exceptional 80 = -(1215753149783934506736127645181464055500452795114368981422483170733 * 10 ^ 70 + 1738935086679627492688600556556608281223663694017687609204544132170632)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_81 :
Polynomial.coeff recurrence2Scalar3Exceptional 81 = 8071992510653526489135039268499917253137874880272440231107727008526 * 10 ^ 70 + 9859021561326427618502842664786407367379611696428174707535218204955482
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_82 :
Polynomial.coeff recurrence2Scalar3Exceptional 82 = -(52084052871981716631251552067665237343102510543598509822712860475321 * 10 ^ 70 + 1686661593954318870786032856557064503162633274204100122122168015973554)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_83 :
Polynomial.coeff recurrence2Scalar3Exceptional 83 = 326719501403155442926075118296505143200191839567914741873982902166220 * 10 ^ 70 + 8330333248959269326670760627860333003484455136990516658365190400938245
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_84 :
Polynomial.coeff recurrence2Scalar3Exceptional 84 = -(1992850654088562997312821617493736444509028844371704841143402333468525 * 10 ^ 70 + 4378953303920747532793773162704722197299763869917847371445463201595117)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_85 :
Polynomial.coeff recurrence2Scalar3Exceptional 85 = (1 * 10 ^ 70 + 1821651978930250581870199049117377951800667033397892134810635834097772) * 10 ^ 70 + 2973137040712411410522771058380691751787467365048364118343047826160505
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_86 :
Polynomial.coeff recurrence2Scalar3Exceptional 86 = -((6 * 10 ^ 70 + 8225363688850475548113425726661537696896192182505574660065678273751272) * 10 ^ 70 + 7019670421275960887693098562061191592079357574248654797491019690446421)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_87 :
Polynomial.coeff recurrence2Scalar3Exceptional 87 = (38 * 10 ^ 70 + 3299468289773170267717585933952443778699509667519455761277281462582781) * 10 ^ 70 + 9802285439816082233878955715761139105141279864705489548487172329130134
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_88 :
Polynomial.coeff recurrence2Scalar3Exceptional 88 = -((209 * 10 ^ 70 + 7474565983201657924666419451773242297162152459780952970126309202631059) * 10 ^ 70 + 3249571390025635689078896133735610942077824338314705341968842473139358)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_89 :
Polynomial.coeff recurrence2Scalar3Exceptional 89 = (1118 * 10 ^ 70 + 1282226605886601161980392745644396780013428483246180730452908046631411) * 10 ^ 70 + 7294102024737217107703292323846339212818907555100967919696353548914411
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_90 :
Polynomial.coeff recurrence2Scalar3Exceptional 90 = -((5805 * 10 ^ 70 + 3084489304033437166947821012528073595835930057541018106983771140486879) * 10 ^ 70 + 5152173469444112496056922578358922880447347815567374412092811386735406)