Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupExceptionalProductPart0.Coefficients0To73

Recurrence 5 lookup certificate: ExceptionalProduct coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_0 :
Polynomial.coeff recurrence5ExceptionalProduct 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_1 :
Polynomial.coeff recurrence5ExceptionalProduct 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_2 :
Polynomial.coeff recurrence5ExceptionalProduct 2 = 68008294656 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_3 :
Polynomial.coeff recurrence5ExceptionalProduct 3 = -319773505615488 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_4 :
Polynomial.coeff recurrence5ExceptionalProduct 4 = 666861526892758896 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_5 :
Polynomial.coeff recurrence5ExceptionalProduct 5 = -757660479951474023544 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_6 :
Polynomial.coeff recurrence5ExceptionalProduct 6 = 100811442218396807528901 / 1365430337030457401667605
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_7 :
Polynomial.coeff recurrence5ExceptionalProduct 7 = -216764707546917918400108899 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_8 :
Polynomial.coeff recurrence5ExceptionalProduct 8 = 95495346064655177619134458092 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_9 :
Polynomial.coeff recurrence5ExceptionalProduct 9 = -44281906534390794592551550682547 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_10 :
Polynomial.coeff recurrence5ExceptionalProduct 10 = 10967929619401068925101522942152989 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_11 :
Polynomial.coeff recurrence5ExceptionalProduct 11 = 2484947366860568066558377249168286173 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_12 :
Polynomial.coeff recurrence5ExceptionalProduct 12 = -672157926834138083152541117755014737377 / 1365430337030457401667605
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_13 :
Polynomial.coeff recurrence5ExceptionalProduct 13 = 1701587270010574181692603308869611655525787 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_14 :
Polynomial.coeff recurrence5ExceptionalProduct 14 = -720713764665413256306774644524750039413889581 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_15 :
Polynomial.coeff recurrence5ExceptionalProduct 15 = 286188480808271394191025734265558907735908882327 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_16 :
Polynomial.coeff recurrence5ExceptionalProduct 16 = -341216970672754366711484605520784548273527198290283 / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_17 :
Polynomial.coeff recurrence5ExceptionalProduct 17 = 7537520771005310288606618176512833522864829455375737 / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_18 :
Polynomial.coeff recurrence5ExceptionalProduct 18 = 2483405824670484450387683378206564621668576571238922763 / 2730860674060914803335210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_19 :
Polynomial.coeff recurrence5ExceptionalProduct 19 = -3515672202850547814231659251805578922042140555019610392487 / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_20 :
Polynomial.coeff recurrence5ExceptionalProduct 20 = 3210486136458743345145907760361455634881980096743705840497163 / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_21 :
Polynomial.coeff recurrence5ExceptionalProduct 21 = -1639444519904797583700262616242561051511534422058942516951669919 / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_22 :
Polynomial.coeff recurrence5ExceptionalProduct 22 = 312995508141412692485729371046931428396176100830209661062210852227 / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_23 :
Polynomial.coeff recurrence5ExceptionalProduct 23 = -11194376494643205154179431406668642659061147481165621813589021262238 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_24 :
Polynomial.coeff recurrence5ExceptionalProduct 24 = 1115915329431096721051854246172964277120855960574732934811205212133424 / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_25 :
Polynomial.coeff recurrence5ExceptionalProduct 25 = -(10 * 10 ^ 70 + 253958156800182111401985643880535363610882812548305461669946749750601) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_26 :
Polynomial.coeff recurrence5ExceptionalProduct 26 = -(1377 * 10 ^ 70 + 6461180711763626525935582704926844123309087307259002391943237101222757) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_27 :
Polynomial.coeff recurrence5ExceptionalProduct 27 = (199956 * 10 ^ 70 + 7468455429016150215996631497748164575415039542879812428660855057132629) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_28 :
Polynomial.coeff recurrence5ExceptionalProduct 28 = -(111239340 * 10 ^ 70 + 2724111859608073617068967008488595121797207772595282251662855136038593) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_29 :
Polynomial.coeff recurrence5ExceptionalProduct 29 = (10467897569 * 10 ^ 70 + 7701827627767381167257469079954599847167972019220805010949792072903083) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_30 :
Polynomial.coeff recurrence5ExceptionalProduct 30 = -(642326081315 * 10 ^ 70 + 3466475752910898145658657408991106403523206553631334052634323188262039) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_31 :
Polynomial.coeff recurrence5ExceptionalProduct 31 = (2639400027316 * 10 ^ 70 + 7676175966813188446325926210127874842579925460685929715215899261493829) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_32 :
Polynomial.coeff recurrence5ExceptionalProduct 32 = (3340833767518486 * 10 ^ 70 + 5437737741824380825697072841981873716471788345619632405473844930745987) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_33 :
Polynomial.coeff recurrence5ExceptionalProduct 33 = -(551827683050119992 * 10 ^ 70 + 4698680028085395255688626250620851770885284221246339540279782733702313) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_34 :
Polynomial.coeff recurrence5ExceptionalProduct 34 = (27833519513960707822 * 10 ^ 70 + 8654136362060708346420733750456686124529574428785688027732450526885283) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_35 :
Polynomial.coeff recurrence5ExceptionalProduct 35 = -(4366133600967097174014 * 10 ^ 70 + 7128861775850674459970086430816269759864053526515129849483833911779157) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_36 :
Polynomial.coeff recurrence5ExceptionalProduct 36 = (71333511044627941720496 * 10 ^ 70 + 1947709151868042484908510537306559959274851128857308010292130829266414) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_37 :
Polynomial.coeff recurrence5ExceptionalProduct 37 = -(16013559129984398637472399 * 10 ^ 70 + 8929107772752755678600455487667935591175073012431501853788703992973657) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_38 :
Polynomial.coeff recurrence5ExceptionalProduct 38 = (196000200866387251113176623 * 10 ^ 70 + 4931384419600674242565239964209417182940338835550197825311638425675692) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_39 :
Polynomial.coeff recurrence5ExceptionalProduct 39 = -(33769795227773828675172256735 * 10 ^ 70 + 6837020672256996176558672001749555851875748472758654645076324022830403) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_40 :
Polynomial.coeff recurrence5ExceptionalProduct 40 = (642366237811179911980600625305 * 10 ^ 70 + 3477852655371701491769275785687879025118362437691477066801866685318011) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_41 :
Polynomial.coeff recurrence5ExceptionalProduct 41 = -(43167848574387109436835485848926 * 10 ^ 70 + 2839382503493463112281176310155993646389791048733549566847624383717567) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_42 :
Polynomial.coeff recurrence5ExceptionalProduct 42 = (1275251918254256437592350418002992 * 10 ^ 70 + 3887220407759836487082039831201038920065498346296271944708714097709529) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_43 :
Polynomial.coeff recurrence5ExceptionalProduct 43 = -(3274143182062757387199855382390438 * 10 ^ 70 + 5544455019681879339543347524041891978008550102796076227228502838858441) / 2730860674060914803335210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_44 :
Polynomial.coeff recurrence5ExceptionalProduct 44 = (712072388066374045990035371837780594 * 10 ^ 70 + 4414847116755858549309743101467302611342919798564518778161859418446317) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_45 :
Polynomial.coeff recurrence5ExceptionalProduct 45 = -(12311961000299184924502760495591891762 * 10 ^ 70 + 4660590671804475563069220923937059112722315142290727806334174042274289) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_46 :
Polynomial.coeff recurrence5ExceptionalProduct 46 = (67326242419069438721812608529109506894 * 10 ^ 70 + 168201205314636618731271963221122157067665970785342262719283045770467) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_47 :
Polynomial.coeff recurrence5ExceptionalProduct 47 = (688984313580539274241097730204344028803 * 10 ^ 70 + 6596833593337978486697369511255643848446956848339164197209915976013993) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_48 :
Polynomial.coeff recurrence5ExceptionalProduct 48 = -(87189841479161244182432998438696482400002 * 10 ^ 70 + 4178522696175498584191159850741557770987316217568835258346529484215717) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_49 :
Polynomial.coeff recurrence5ExceptionalProduct 49 = (1439052114363604111266891803251637115695304 * 10 ^ 70 + 1134218146536914211655013059543581813035740158874658368260464400580759) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_50 :
Polynomial.coeff recurrence5ExceptionalProduct 50 = -(66337881643071834499947585918076605277262248 * 10 ^ 70 + 6996676748543308614581867338343161535794134481519370718304214831627473) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_51 :
Polynomial.coeff recurrence5ExceptionalProduct 51 = (236123742568945300279956624657620538838107356 * 10 ^ 70 + 8000950671263247984282327827647739809402046579313465027246668609436363) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_52 :
Polynomial.coeff recurrence5ExceptionalProduct 52 = -(3151674734441543116853239968977448643904651280 * 10 ^ 70 + 4844562933130133417346755618121299188902776692530264942577425320343163) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_53 :
Polynomial.coeff recurrence5ExceptionalProduct 53 = (30178572147810206332405553410014788974166500820 * 10 ^ 70 + 2317405335247710505388401593955862227463162117024434831903576556476428) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_54 :
Polynomial.coeff recurrence5ExceptionalProduct 54 = (477728874072814469611577410184956808023060082368 * 10 ^ 70 + 5804068664598089361866267107780500251306620500592201993846595308690563) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_55 :
Polynomial.coeff recurrence5ExceptionalProduct 55 = -(15030148142482545563836355958725197898600368813632 * 10 ^ 70 + 3672366637158744267588178509440760169281323733380101026759056116611513) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_56 :
Polynomial.coeff recurrence5ExceptionalProduct 56 = (719785021663688856057343293571593349762431441083292 * 10 ^ 70 + 4775521950558910469834561657711589158698286522979969849729421382979363) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_57 :
Polynomial.coeff recurrence5ExceptionalProduct 57 = -(1246128356304360061703609575122444317287267153490411 * 10 ^ 70 + 1913663663745150329807913999977392033503237008920873673125122472957019) / 1365430337030457401667605
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_58 :
Polynomial.coeff recurrence5ExceptionalProduct 58 = (342185171704930423738779575542383938356084482649010104 * 10 ^ 70 + 5195364968932544271861471709281124081358453160401304244362264221142149) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_59 :
Polynomial.coeff recurrence5ExceptionalProduct 59 = -(3726951221326008625728762687324449253680086287347386572 * 10 ^ 70 + 5363819824453014016858982797073503437489645199472250774295349823238989) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_60 :
Polynomial.coeff recurrence5ExceptionalProduct 60 = (14726043727350114600620118414143776831635360103916011853 * 10 ^ 70 + 3938264456847774885805683451645962364487029592078616476878917411923373) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_61 :
Polynomial.coeff recurrence5ExceptionalProduct 61 = -(94456238927833850775454944354911622070808671644738104848 * 10 ^ 70 + 6367018838453974741908699794790233288112704710186100148769817392901079) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_62 :
Polynomial.coeff recurrence5ExceptionalProduct 62 = -(92857454132625853770328827704137241694512253451338159087 * 10 ^ 70 + 6398032669243347607298608379701521169021634206182896401416588800077383) / 1365430337030457401667605
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_63 :
Polynomial.coeff recurrence5ExceptionalProduct 63 = (9048773948280954230738232019709743059968373220711940754450 * 10 ^ 70 + 8564566053921289129858455341314405129006964011266534288979680720950003) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_64 :
Polynomial.coeff recurrence5ExceptionalProduct 64 = -(148916960806431178392379307983204069177036628845507600118873 * 10 ^ 70 + 4571857441127299009163312798195667640046623820614094343096628935762233) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_65 :
Polynomial.coeff recurrence5ExceptionalProduct 65 = (5428543190162069163850485584498760862554345228846639717828330 * 10 ^ 70 + 3678929676553524193255465147058749138797751692124156658607170472593383) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_66 :
Polynomial.coeff recurrence5ExceptionalProduct 66 = -(816653856665545146027637429221563825631887341637647482295377 * 10 ^ 70 + 487680631222793532687674677833490814465699200408747864686420460000403) / 738070452448895892793300
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_67 :
Polynomial.coeff recurrence5ExceptionalProduct 67 = -(16647655709820557812710397978409700064551081413431242577399185 * 10 ^ 70 + 5879778343120535098383276644742241811459918725060061927103340562563911) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_68 :
Polynomial.coeff recurrence5ExceptionalProduct 68 = (818045639452742509487822340910899837505300518709108958951621439 * 10 ^ 70 + 4291752318718456703764792129029547087098656154847934843855333983065449) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_69 :
Polynomial.coeff recurrence5ExceptionalProduct 69 = -(23324860856202143915675919647631884231064736424535689655363650832 * 10 ^ 70 + 4135386943792353792236030414983132849962581090597294944337774232097619) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_70 :
Polynomial.coeff recurrence5ExceptionalProduct 70 = (414643162383539002624812033051553975840929313993006361820263925270 * 10 ^ 70 + 4605200627427092425653361141724811825775064019147155141290456007133979) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_71 :
Polynomial.coeff recurrence5ExceptionalProduct 71 = -(2225971920530168787351535430173208295912080747969959060401937227949 * 10 ^ 70 + 9544375581753079106222545365247425855597903632874365827584388457131477) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_72 :
Polynomial.coeff recurrence5ExceptionalProduct 72 = -(30780824081329347751806893320766653085278971058542512273047380911 * 10 ^ 70 + 7460609746523755121141415924082749688487709589711882788863529399533299) / 1365430337030457401667605
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_73 :
Polynomial.coeff recurrence5ExceptionalProduct 73 = (172329760941705495006504953951705551625582184750271152906692320942603 * 10 ^ 70 + 665928152601537507387250179283900814481096266513183717659297627646511) / 27308606740609148033352100