Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar4MainPart0.Coefficients151To191

Recurrence 2 lookup certificate: Scalar4Main coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_151 :
Polynomial.coeff recurrence2Scalar4Main 151 = (24174648076990437804769601221060907118107 * 10 ^ 70 + 5141028058389917132214490164717154943608204489349834082625831853884368) * 10 ^ 70 + 5567350627375411318202279411971639306133333453742017656865691695352472
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_152 :
Polynomial.coeff recurrence2Scalar4Main 152 = -((84668028530269297165211641640197689799593 * 10 ^ 70 + 5551602532586496221857909638866742783751297289984724741081018521433847) * 10 ^ 70 + 9730097032118042623833195023277904551550529644916399479032387547039901)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_153 :
Polynomial.coeff recurrence2Scalar4Main 153 = -((495307400426669427765964668448825103116 * 10 ^ 70 + 9893299126148358125963598753335041298490291110368554901364606993680440) * 10 ^ 70 + 1934238512336285604055633139201728841451501966808321476760137766285507)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_154 :
Polynomial.coeff recurrence2Scalar4Main 154 = (1122551132307368457358699617034672532549858 * 10 ^ 70 + 6712641670716419898918324902910462208816596772244982467804026490875506) * 10 ^ 70 + 4350280774422421458775005445449742119507537549018249023590624793382192
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_155 :
Polynomial.coeff recurrence2Scalar4Main 155 = -((4371594050057872579568870026924380945362071 * 10 ^ 70 + 9833869971792964929591750674313034623670656678240757789353091108350972) * 10 ^ 70 + 17346830316509548219346387369607206329238953911720133489944504373254)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_156 :
Polynomial.coeff recurrence2Scalar4Main 156 = (3107644577804568733223870572835367316416889 * 10 ^ 70 + 9338363694825545653515995292953279517481285781462364005437618173759203) * 10 ^ 70 + 4273619454595891722134830305293334256719164146599428075663590225158144
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_157 :
Polynomial.coeff recurrence2Scalar4Main 157 = (40212595492414630420888274903673077253380877 * 10 ^ 70 + 7191761045235621828006951302332922735741761221397577952364761364816798) * 10 ^ 70 + 8737221420458901642830089370044764890780458504119964887869814699926144
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_158 :
Polynomial.coeff recurrence2Scalar4Main 158 = -((189540430445527651830659357804633628448547913 * 10 ^ 70 + 9302777533885002222468619163399135813511786179094812992382324483527360) * 10 ^ 70 + 4158778797098851055080828668476175075388283055159228294148087886053909)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_159 :
Polynomial.coeff recurrence2Scalar4Main 159 = (265519806671155147535558081781370419684879312 * 10 ^ 70 + 4288013060998136775391685580792107450356384582611868822979638137995035) * 10 ^ 70 + 5942354955971419206823058961302641357923219372844637565225698449998414
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_160 :
Polynomial.coeff recurrence2Scalar4Main 160 = (1078767519003143979163300823326425536187550171 * 10 ^ 70 + 1257560312452916615684187139830858914411242762480007089984894775358800) * 10 ^ 70 + 7952991786647058280858253720266848607121469014412725692983758592586691
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_161 :
Polynomial.coeff recurrence2Scalar4Main 161 = -((6855119820988591383358514042368419041329804143 * 10 ^ 70 + 7958134255240021249741035366353043323459640726405641323721297474682474) * 10 ^ 70 + 4652913611669949239551407053459776001848442414993016469905936509267968)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_162 :
Polynomial.coeff recurrence2Scalar4Main 162 = (14052329129088213520104095430892009284541068502 * 10 ^ 70 + 8928235238470862234172845651737733737439207006809257087750649786946082) * 10 ^ 70 + 9684891599512961492915061379268161726248485174623643174383489387574028
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_163 :
Polynomial.coeff recurrence2Scalar4Main 163 = (18744113880128633335110765138693597200203509324 * 10 ^ 70 + 9842406142320950814363928862378169873600726213560045686978828884990057) * 10 ^ 70 + 2136007069986285231850702504213297628329026526443391343271411355454163
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_164 :
Polynomial.coeff recurrence2Scalar4Main 164 = -((210487391731724416583883875445595732299218252481 * 10 ^ 70 + 4907852384245118131604084001817079412175082031013756965781867795453411) * 10 ^ 70 + 9294060968680858572801166702457444757512474597893600658407928389142691)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_165 :
Polynomial.coeff recurrence2Scalar4Main 165 = (581750153501658545268955855806677768636766949274 * 10 ^ 70 + 4850066391896081012913090876011290877217093748381149224497747881591650) * 10 ^ 70 + 2912815408746200566798043046780885367246018029574209217464769866278926
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_166 :
Polynomial.coeff recurrence2Scalar4Main 166 = -((54209499978525458504951506899820640951831272785 * 10 ^ 70 + 7199549586829224792270239193838351044665712397046068305658809775174420) * 10 ^ 70 + 1469629929212201928256754243196061157084068054686450247220391000015530)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_167 :
Polynomial.coeff recurrence2Scalar4Main 167 = -((5452437032088520311178977310252315174406273839815 * 10 ^ 70 + 319796114531508866434647154092147005034079819427505708290713280127559) * 10 ^ 70 + 2587201483080227177173833485743816148984537187694947238579296528509871)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_168 :
Polynomial.coeff recurrence2Scalar4Main 168 = (20509843676340741307283758066754067213044717381222 * 10 ^ 70 + 7684885464489706208427218166603236858579041844122890008132868067212988) * 10 ^ 70 + 9119396506607370070224167355874546783415885097536731400132856875647853
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_169 :
Polynomial.coeff recurrence2Scalar4Main 169 = -((23752867770371934459423984674543262332730209289913 * 10 ^ 70 + 6519493197199943466782659219248409004819149831371983271289788112347785) * 10 ^ 70 + 2569841464553686635251159648917365485560854654428727338083913898671081)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_170 :
Polynomial.coeff recurrence2Scalar4Main 170 = -((104440440760961860185571508643891853840840436475889 * 10 ^ 70 + 5047951192568133454363628513850676876226025186705203052901210408383347) * 10 ^ 70 + 8028819039285809625044318099616486009201036871179814903960444600829300)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_171 :
Polynomial.coeff recurrence2Scalar4Main 171 = (608177495983141179425431176621050395091055628699862 * 10 ^ 70 + 2207809359577802960040335943220694981194179697007776134409692995365445) * 10 ^ 70 + 7314445395899321560348420929039851305489821536589931479053744288385857
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_172 :
Polynomial.coeff recurrence2Scalar4Main 172 = -((1320338999149375505840735887730937989963755286324320 * 10 ^ 70 + 1001541382695298561903996480418941142740097896354989533278894862798018) * 10 ^ 70 + 9035061091256608922149618857800510300719704524970916768880226238326283)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_173 :
Polynomial.coeff recurrence2Scalar4Main 173 = -((502597989965711821280639783453863304021951265797682 * 10 ^ 70 + 2876000204660625280389775341591084120069630707437713091181808021312428) * 10 ^ 70 + 5587740823845843016309904629168943641474240834320522506183510625184806)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_174 :
Polynomial.coeff recurrence2Scalar4Main 174 = (13535320084849810984045516460862121914858422316752838 * 10 ^ 70 + 3598780277562313752782556614873027003041227031100517802531267879802479) * 10 ^ 70 + 243336554697266270641668433697867018276547430473883369257141226491931
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_175 :
Polynomial.coeff recurrence2Scalar4Main 175 = -((46718512592209480402466185183104913813083663976260656 * 10 ^ 70 + 7790293431067199786279833948946764240826408098783990746366666125248188) * 10 ^ 70 + 1605612290490378877222543313208998398993534068709999377459585505587446)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_176 :
Polynomial.coeff recurrence2Scalar4Main 176 = (61512438706801456027024740447268901130481649797278722 * 10 ^ 70 + 4541517568535904246640032748702753824603127730396355662148785070816429) * 10 ^ 70 + 9123921389499462492831127433350648174785548181488245629469597883321544
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_177 :
Polynomial.coeff recurrence2Scalar4Main 177 = (156950772323936489377023760317558381948586055703051319 * 10 ^ 70 + 9818935613633406249376502364811123665246906376662350469958778805562943) * 10 ^ 70 + 1139694781290398665593452852569038123107040739358238341070181567359454
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_178 :
Polynomial.coeff recurrence2Scalar4Main 178 = -((1097551334046301716295332455290514346057281084888567540 * 10 ^ 70 + 947704012831311259720273130571972559330802778291928111572537185336971) * 10 ^ 70 + 4836735199428977443353836543467921543830498378044241819382653772350825)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_179 :
Polynomial.coeff recurrence2Scalar4Main 179 = (2895704407882056872105671746321250888265199497238006090 * 10 ^ 70 + 2379203239310739598650245764193784236908763586975102518020060182967384) * 10 ^ 70 + 6278048215019754879072061647076625775813514645253372877945381834474937
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_180 :
Polynomial.coeff recurrence2Scalar4Main 180 = -((2315754562280762373557511872803581896849448909861462389 * 10 ^ 70 + 2611541250415768384466762052634049011159404642891975318186455816613345) * 10 ^ 70 + 180082044854944821553810315747897154067259029324566195618174053395865)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_181 :
Polynomial.coeff recurrence2Scalar4Main 181 = -((13640521026892293716924233947827475620322679461564597375 * 10 ^ 70 + 2801188897063265800816968084469510123332727488019634513433744691016061) * 10 ^ 70 + 509917775699962840914867073176347605040994264969375883963557835955135)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_182 :
Polynomial.coeff recurrence2Scalar4Main 182 = (69304009252860808794408334775401097065683229608167291996 * 10 ^ 70 + 2150193077835946771442098934526145758707084201147614985638170424248845) * 10 ^ 70 + 8177329328115598404325717239522867580180083180798443780738796503451130
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_183 :
Polynomial.coeff recurrence2Scalar4Main 183 = -((160916449893783403245660560798679482442800632186575174234 * 10 ^ 70 + 7185404705210998075000783816661107290359464210677667828229694427252332) * 10 ^ 70 + 8044392712015030472084560730142479732966464139830960034935013572074529)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_184 :
Polynomial.coeff recurrence2Scalar4Main 184 = (101948923573644956289239277029312845852718351095666359935 * 10 ^ 70 + 1285210041344060632691482907153965972346501537344053308838477185731077) * 10 ^ 70 + 3655406945680693930177974239093383908284378117513439896720676886771214
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_185 :
Polynomial.coeff recurrence2Scalar4Main 185 = (773490434954409666115680366455211187084592553141132269093 * 10 ^ 70 + 140390783260469708511450200914881463103354693685890834286870191835513) * 10 ^ 70 + 490188834810151021260571044575538151699006726236853789536737886545022
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_186 :
Polynomial.coeff recurrence2Scalar4Main 186 = -((3662885241568676665214666490984469427562719788201960794176 * 10 ^ 70 + 5549864158992604587086658780162356368366814481751423230316969508131873) * 10 ^ 70 + 1647320273726573100940886542899874727940632444290903516656125749737670)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_187 :
Polynomial.coeff recurrence2Scalar4Main 187 = (8550030963865126837526849010925838976554099087844615435456 * 10 ^ 70 + 3919825149665236311574093628517522954205046431158341254445841182863436) * 10 ^ 70 + 9718952556701174033500416460560104276582612143377754106634987768280774
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_188 :
Polynomial.coeff recurrence2Scalar4Main 188 = -((7502334676632039393343639408111910043211506573286294999053 * 10 ^ 70 + 2065109084891940562381538181061066695430675647753014145174773344132620) * 10 ^ 70 + 6964470633263979494050587015383060825953573343093991977296509523050826)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_189 :
Polynomial.coeff recurrence2Scalar4Main 189 = -((28848261526714106782202898309154895102589415277275964807128 * 10 ^ 70 + 8364260273606338816319916723207844240303703900042129835440461054024173) * 10 ^ 70 + 2003404378263905340868393746212014089875652506817854475275397905915533)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_190 :
Polynomial.coeff recurrence2Scalar4Main 190 = (159485308094492191713214018235598965821197669071012168747346 * 10 ^ 70 + 7264291250968530090215526404032332193849550907698168504532094654418886) * 10 ^ 70 + 4701966771802052636903164197364879645224459474270726386239828519200089
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_191 :
Polynomial.coeff recurrence2Scalar4Main 191 = -((421622619443554404952825120285842520177865483427739329730380 * 10 ^ 70 + 5741446247329966037066515117682701297411768016234843388463962334413071) * 10 ^ 70 + 3123204516085534065253514536284298566417207208081781260325549378507066)