Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupB1Low

Recurrence 4 lookup certificate: B1 source coefficients, low half #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_0 :
Polynomial.coeff remainder5Coefficient1 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_1 :
Polynomial.coeff remainder5Coefficient1 1 = 260832740765859690536
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_2 :
Polynomial.coeff remainder5Coefficient1 2 = -599798859925772952688186
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_3 :
Polynomial.coeff remainder5Coefficient1 3 = 515010438763430378824396622
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_4 :
Polynomial.coeff remainder5Coefficient1 4 = -76912847307884185746204152022
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_5 :
Polynomial.coeff remainder5Coefficient1 5 = -39528662864659869708437973812678
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_6 :
Polynomial.coeff remainder5Coefficient1 6 = 22423278808863624534504605339183226
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_7 :
Polynomial.coeff remainder5Coefficient1 7 = 1089539022471937695962046850508211745
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_8 :
Polynomial.coeff remainder5Coefficient1 8 = -5539138044347443264592969557290651346342
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_9 :
Polynomial.coeff remainder5Coefficient1 9 = 2759182459620370707593704668275573321509342
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_10 :
Polynomial.coeff remainder5Coefficient1 10 = -747400383590690394016557379090120796900268778
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_11 :
Polynomial.coeff remainder5Coefficient1 11 = 126612037565207748711252839349707309075819048058
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_12 :
Polynomial.coeff remainder5Coefficient1 12 = -12860469566166149164120902333488903484738828469792
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_13 :
Polynomial.coeff remainder5Coefficient1 13 = 404418412191306202383123061756659703928354139879885
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_14 :
Polynomial.coeff remainder5Coefficient1 14 = 107750878548261641043501687245211387141932508084083991
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_15 :
Polynomial.coeff remainder5Coefficient1 15 = -23166381876054735843275285873213589333475539084952971659
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_16 :
Polynomial.coeff remainder5Coefficient1 16 = 2688529921402536393055733759606458252566391905484993603159
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_17 :
Polynomial.coeff remainder5Coefficient1 17 = -224171429964828927017100655951580555169129913077115092787821
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_18 :
Polynomial.coeff remainder5Coefficient1 18 = 14566404178546139416758100729272237835136887482028211602144981
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_19 :
Polynomial.coeff remainder5Coefficient1 19 = -765722068558499201180134478315214402263190045596988877938205075
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_20 :
Polynomial.coeff remainder5Coefficient1 20 = 33253152462493620736482618023761878117727901650417223642924796770
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_21 :
Polynomial.coeff remainder5Coefficient1 21 = -1207697414782672261991814930754965149898711722039585827325328614888
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_22 :
Polynomial.coeff remainder5Coefficient1 22 = 36894752563148269340382387511433123990836885797389013633548790264222
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_23 :
Polynomial.coeff remainder5Coefficient1 23 = -946889771867600408490987391079160752275595124773646170957269967190265
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_24 :
Polynomial.coeff remainder5Coefficient1 24 = 2 * 10 ^ 70 + 158473225132267568099372506683966939613222119820016704611350742232622
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_25 :
Polynomial.coeff remainder5Coefficient1 25 = -(34 * 10 ^ 70 + 2425635355046085094224113851230423708246451970946047611114168504570070)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_26 :
Polynomial.coeff remainder5Coefficient1 26 = 407 * 10 ^ 70 + 2966914225350199131521764868335241934997033198683544626147080883863034
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_27 :
Polynomial.coeff remainder5Coefficient1 27 = -(1073 * 10 ^ 70 + 4137178338839485712271756532299302949713032291706874478304724376772173)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_28 :
Polynomial.coeff remainder5Coefficient1 28 = -(107800 * 10 ^ 70 + 822150445056023164343532454246889584875027742088150663327162512260997)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_29 :
Polynomial.coeff remainder5Coefficient1 29 = 3841409 * 10 ^ 70 + 127400061991043226322678611284363736158020364771961742198172298435886
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_30 :
Polynomial.coeff remainder5Coefficient1 30 = -(88204154 * 10 ^ 70 + 5277031475068952765368880376134639482003752248789748046311794563337986)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_31 :
Polynomial.coeff remainder5Coefficient1 31 = 1624376868 * 10 ^ 70 + 9274205282493336470461503415753298775876686096885081681426971485566054
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_32 :
Polynomial.coeff remainder5Coefficient1 32 = -(25612410183 * 10 ^ 70 + 8609413040640021198707750544394788394553795502344981693366672515298724)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_33 :
Polynomial.coeff remainder5Coefficient1 33 = 356230591766 * 10 ^ 70 + 1329170384249737344716042195594487796638397433682672419481570058154464
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_34 :
Polynomial.coeff remainder5Coefficient1 34 = -(4445085026502 * 10 ^ 70 + 131513557458933692752871780838246964906310792875834306288393098836574)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_35 :
Polynomial.coeff remainder5Coefficient1 35 = 50313218345640 * 10 ^ 70 + 3169612861687876152407403211734562201205103934585558011710669101002613
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_36 :
Polynomial.coeff remainder5Coefficient1 36 = -(520664163330927 * 10 ^ 70 + 8800692962456451470131845868029784506859201261348669540912263401122315)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_37 :
Polynomial.coeff remainder5Coefficient1 37 = 4955864976207658 * 10 ^ 70 + 8815247979212087498968122289188079145106302773575188546356153777684103
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_38 :
Polynomial.coeff remainder5Coefficient1 38 = -(43597444005474814 * 10 ^ 70 + 7263746612908301238772220104262591674595095327302637059241243467470476)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_39 :
Polynomial.coeff remainder5Coefficient1 39 = 355893318220401883 * 10 ^ 70 + 7163127712136060469025333540172237070052394559799856379258362651353854
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_40 :
Polynomial.coeff remainder5Coefficient1 40 = -(2705050941619091308 * 10 ^ 70 + 2110795204372530891369750778502519732436438563209689474061662518286595)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_41 :
Polynomial.coeff remainder5Coefficient1 41 = 19200481117689800232 * 10 ^ 70 + 4668342056095532238274417706144057471425387160163332738910171036444153
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_42 :
Polynomial.coeff remainder5Coefficient1 42 = -(127602872909224349786 * 10 ^ 70 + 9027916509621896435233097878544966867450350838696907788334343998397699)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_43 :
Polynomial.coeff remainder5Coefficient1 43 = 795841185785076740165 * 10 ^ 70 + 9309173945927028272794101628623613643603091437016767625488751027851187
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_44 :
Polynomial.coeff remainder5Coefficient1 44 = -(4667797368998863559042 * 10 ^ 70 + 714201812552778422945165845372512322415198528862474212366226333448589)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_45 :
Polynomial.coeff remainder5Coefficient1 45 = 25794710418122814887995 * 10 ^ 70 + 4206068277389735340088939657367322612721668027982701572002143131173881
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_46 :
Polynomial.coeff remainder5Coefficient1 46 = -(134529957951725175415850 * 10 ^ 70 + 7694084246620578150355531150212314546178526879133543930020982494219926)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_47 :
Polynomial.coeff remainder5Coefficient1 47 = 663202243208303198526325 * 10 ^ 70 + 9521270539713472251764250298244190751857845645230390853073436424114775
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_48 :
Polynomial.coeff remainder5Coefficient1 48 = -(3094712002575881337884174 * 10 ^ 70 + 5002306532671953443516011954395699408791339283093914526076844646793612)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_49 :
Polynomial.coeff remainder5Coefficient1 49 = 13686618786856234219723315 * 10 ^ 70 + 8599816138809727317571813853001191393711101520666531130396927921262073
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_50 :
Polynomial.coeff remainder5Coefficient1 50 = -(57435321246250417877565368 * 10 ^ 70 + 7460719276143192048655766796279689455667934253768308250671922172155502)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_51 :
Polynomial.coeff remainder5Coefficient1 51 = 228944076478171014327903225 * 10 ^ 70 + 2076153767400093530774958642662054428751749943706116246021682538798597
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_52 :
Polynomial.coeff remainder5Coefficient1 52 = -(867694494161462255265845676 * 10 ^ 70 + 3606382991812857909026448457243261595585057927929636871343728258157446)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_53 :
Polynomial.coeff remainder5Coefficient1 53 = 3129488911946689640468618177 * 10 ^ 70 + 7818291972969409688734379246803722826318332304639390383296188373497996
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_54 :
Polynomial.coeff remainder5Coefficient1 54 = -(10749709307353405726762716903 * 10 ^ 70 + 3365536188971723394128674540542921456842504585340615132630263373065458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_55 :
Polynomial.coeff remainder5Coefficient1 55 = 35192699711861319155000110771 * 10 ^ 70 + 1037904887955372379142707270985603210853177172072853393838620378017565
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_56 :
Polynomial.coeff remainder5Coefficient1 56 = -(109882256146846934735222112234 * 10 ^ 70 + 9495691637242789127257042836062309316848315626134489909779037896320075)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_57 :
Polynomial.coeff remainder5Coefficient1 57 = 327401902230678581643222116579 * 10 ^ 70 + 6185792676965783441327175243979437270619246487090808305435057920569657
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_58 :
Polynomial.coeff remainder5Coefficient1 58 = -(931425194070347587255716696523 * 10 ^ 70 + 5877657872432593133714054016638145486911276485112104330236456965530760)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_59 :
Polynomial.coeff remainder5Coefficient1 59 = 2531274248765978708787738179331 * 10 ^ 70 + 8062082897426744081475736567353011692991460807645362675105244652854633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_60 :
Polynomial.coeff remainder5Coefficient1 60 = -(6574224210245251490678681380417 * 10 ^ 70 + 4077850819745080020207550473555282732712569579444717465936907310939783)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_61 :
Polynomial.coeff remainder5Coefficient1 61 = 16324252803432586294735877047285 * 10 ^ 70 + 4567351443877819205206286940715924185024883925610669479882835221655651
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_62 :
Polynomial.coeff remainder5Coefficient1 62 = -(38766439695288143246873265423796 * 10 ^ 70 + 6661341681036478585522743700151877700915854619518719937291500761193633)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_63 :
Polynomial.coeff remainder5Coefficient1 63 = 88073349567423609195841951843886 * 10 ^ 70 + 9480306512099937629229735307258490759353328846412203271867716980014357
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_64 :
Polynomial.coeff remainder5Coefficient1 64 = -(191475800236824200576440103082636 * 10 ^ 70 + 2768671618406765034722462103054454347224394111805903178374041819370269)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_65 :
Polynomial.coeff remainder5Coefficient1 65 = 398439112484155484454543642408985 * 10 ^ 70 + 5926369066589357910244045669887108952349869008025282308239974386602362
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_66 :
Polynomial.coeff remainder5Coefficient1 66 = -(793724917959088796271662148830966 * 10 ^ 70 + 1040010171879851744342916069759079336552183625067516128368252079476487)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_67 :
Polynomial.coeff remainder5Coefficient1 67 = 1513919274157322364974261659701795 * 10 ^ 70 + 2638368444775011300095486686675917903890092706225413621571703147503639
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_68 :
Polynomial.coeff remainder5Coefficient1 68 = -(2765080906557860093968305786589136 * 10 ^ 70 + 8005431794885430156686738237415682262568325843772676649259820542168183)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_69 :
Polynomial.coeff remainder5Coefficient1 69 = 4836326705641471512964273717373941 * 10 ^ 70 + 7399435002114797499621492445237287120868873848717277562153309748872497
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_70 :
Polynomial.coeff remainder5Coefficient1 70 = -(8100984003137201844308502178452100 * 10 ^ 70 + 1201688770830957762093564716878437988898279448072883073675188576330695)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_71 :
Polynomial.coeff remainder5Coefficient1 71 = 12994689989334740222107964620929393 * 10 ^ 70 + 8986843356094522206051351167500757880829332701099353556922973040191525
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_72 :
Polynomial.coeff remainder5Coefficient1 72 = -(19960415658616801947711267355696551 * 10 ^ 70 + 6618464674616421778582691312075227002277185448735786639161226919167657)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_73 :
Polynomial.coeff remainder5Coefficient1 73 = 29355753946918704488511248595012026 * 10 ^ 70 + 5071827747381710424814929060998090220837605529668388213985010020650927
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_74 :
Polynomial.coeff remainder5Coefficient1 74 = -(41328771065320954458440160990262688 * 10 ^ 70 + 8784001651799251341035120097729985619761423225828734123153002700954741)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_75 :
Polynomial.coeff remainder5Coefficient1 75 = 55683789718674219808269469519884074 * 10 ^ 70 + 8155095611012771295292110777456662744328633941339939204505041449521115
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_76 :
Polynomial.coeff remainder5Coefficient1 76 = -(71773194589557849430582637285555590 * 10 ^ 70 + 464336861567756238624503874974234256039546158770114337946374500744016)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_77 :
Polynomial.coeff remainder5Coefficient1 77 = 88459000415688255401536702013611969 * 10 ^ 70 + 2055935274931512972043592762038760647193996013469868075004960325258254
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_78 :
Polynomial.coeff remainder5Coefficient1 78 = -(104181909449697134798825256617201205 * 10 ^ 70 + 2046982980144205215251939705895737777838282496905739211284947426952092)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_79 :
Polynomial.coeff remainder5Coefficient1 79 = 117152932286896160528705451782234577 * 10 ^ 70 + 3727316604543730825773918474294094830047892377492460614076233102857312
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_80 :
Polynomial.coeff remainder5Coefficient1 80 = -(125646967891916076365455898103245637 * 10 ^ 70 + 3148787759601894169257866424209917877602285577248005226024999315143782)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_81 :
Polynomial.coeff remainder5Coefficient1 81 = 128339748807534899191758880623368029 * 10 ^ 70 + 1918839967780649202750197799380652208993110768963547060051632330317693
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_82 :
Polynomial.coeff remainder5Coefficient1 82 = -(124603962005887468537940198277894970 * 10 ^ 70 + 901918805242665368372861146248992055337322634897121428896457212950608)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_83 :
Polynomial.coeff remainder5Coefficient1 83 = 114679802770548765775131674553523012 * 10 ^ 70 + 1691193807801869751323090289444338208487672193991713137673883181927419
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_84 :
Polynomial.coeff remainder5Coefficient1 84 = -(99663920944982480597854668225328918 * 10 ^ 70 + 3251337419108034336012450281045586616627122103451732432835090818807429)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_85 :
Polynomial.coeff remainder5Coefficient1 85 = 81311150157989053420972502069536814 * 10 ^ 70 + 3231864727386637690052997031326248837970792695250957580282997289735816
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B1_coeff_86 :
Polynomial.coeff remainder5Coefficient1 86 = -(61698337866845503226247017123087820 * 10 ^ 70 + 3054080186671080782657207316726242154890583627835404800911447109140355)