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_16 :
Polynomial.coeff recurrence2Scalar3Exceptional 16 = -4322166142015770418100349021596022699857094819620
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_17 :
Polynomial.coeff recurrence2Scalar3Exceptional 17 = 911077692272539216443400885262103270306448707607230
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_18 :
Polynomial.coeff recurrence2Scalar3Exceptional 18 = -141426841381915690260919338303052773344691290827931375
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_19 :
Polynomial.coeff recurrence2Scalar3Exceptional 19 = 15496426236939601562278680935859075275334193475592342332
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_20 :
Polynomial.coeff recurrence2Scalar3Exceptional 20 = -1019407657555669782934151700815368102342470053701685827872
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_21 :
Polynomial.coeff recurrence2Scalar3Exceptional 21 = -5385824201192950064159700510387370216112392412717013540718
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_22 :
Polynomial.coeff recurrence2Scalar3Exceptional 22 = 11046656029044875575533300227454170546940179360540765008709418
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_23 :
Polynomial.coeff recurrence2Scalar3Exceptional 23 = -1544570628407461539159663743546089644646695377317824483162641729
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_24 :
Polynomial.coeff recurrence2Scalar3Exceptional 24 = 124317250329558182146671082857375589207423969138274068390529120118
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_25 :
Polynomial.coeff recurrence2Scalar3Exceptional 25 = -5622941998771786800745057538994287200823520367052813582295404754022
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_26 :
Polynomial.coeff recurrence2Scalar3Exceptional 26 = -26641527131991333837469906294983685060913392376433167311051092586168
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_27 :
Polynomial.coeff recurrence2Scalar3Exceptional 27 = 2 * 10 ^ 70 + 9442742564293847795245774181561649929077208235724693366801115646183330
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_28 :
Polynomial.coeff recurrence2Scalar3Exceptional 28 = -(293 * 10 ^ 70 + 5565767533692479193058167019970531466621509512430338844661843877424725)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_29 :
Polynomial.coeff recurrence2Scalar3Exceptional 29 = 18523 * 10 ^ 70 + 6888472682212404217909650714062677742740889537689273247300487073235204
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_30 :
Polynomial.coeff recurrence2Scalar3Exceptional 30 = -(856285 * 10 ^ 70 + 2159264894324984537436348420231677392110399583239986577847010533763676)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_31 :
Polynomial.coeff recurrence2Scalar3Exceptional 31 = 29877157 * 10 ^ 70 + 4799327605577406525961474124898532060179582539082774641628332885031594
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_32 :
Polynomial.coeff recurrence2Scalar3Exceptional 32 = -(777340642 * 10 ^ 70 + 3009825744070866973892420742019934302121959322963585642344240858458319)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_33 :
Polynomial.coeff recurrence2Scalar3Exceptional 33 = 14746650453 * 10 ^ 70 + 2885048257333693034717482282422441561112685095392046261766046616264953
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_34 :
Polynomial.coeff recurrence2Scalar3Exceptional 34 = -(246809538992 * 10 ^ 70 + 983589331079367359274479898393306460328099476000678548703959274073393)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_35 :
Polynomial.coeff recurrence2Scalar3Exceptional 35 = 8783328150886 * 10 ^ 70 + 3087147360370494578593705327795855376347270047058202701333771514897965
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_36 :
Polynomial.coeff recurrence2Scalar3Exceptional 36 = -(502684597610799 * 10 ^ 70 + 7347003131989812494266002287106690536462744059573719623803233237269822)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_37 :
Polynomial.coeff recurrence2Scalar3Exceptional 37 = 22622748110896411 * 10 ^ 70 + 3731389736182158011657213780479880360293698858600012395377084737000785
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_38 :
Polynomial.coeff recurrence2Scalar3Exceptional 38 = -(754059700537661992 * 10 ^ 70 + 950992757225603142629720443766418629073418075601907101451569149579974)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_39 :
Polynomial.coeff recurrence2Scalar3Exceptional 39 = 19624176760978523920 * 10 ^ 70 + 2398635335548560754552729803199187595408357083708033683656018570488933
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)