Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupB3A3Part1.Coefficients310To346

Recurrence 4 lookup certificate: B3A3 coefficient convolution #

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.recurrence4B3A3_coeff_310 :
Polynomial.coeff recurrence4B3A3 310 = -((8166480 * 10 ^ 70 + 4516128630941084092026038293921867358597725756502809968831736967717075) * 10 ^ 70 + 4731005718893817726240438652887687669656223872090880244989485340837155)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_311 :
Polynomial.coeff recurrence4B3A3 311 = (2240525 * 10 ^ 70 + 7319983109516943300211275286599326035583257707231574689025573686082111) * 10 ^ 70 + 5531075211959961993981934276861003389641100779360679615485994031671588
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_312 :
Polynomial.coeff recurrence4B3A3 312 = -((204917 * 10 ^ 70 + 1575050785750216940847369985174997454992682047584624786846303443483607) * 10 ^ 70 + 9377978343683187331852870929566717617122621471207609307990657011496828)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_313 :
Polynomial.coeff recurrence4B3A3 313 = (10483 * 10 ^ 70 + 7820410902268148236355586711144779101218616435556789334143137897892501) * 10 ^ 70 + 6822287957715437834107381556663713053298314183593036543625623942641397
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_314 :
Polynomial.coeff recurrence4B3A3 314 = -((181 * 10 ^ 70 + 2605010098219197355862098587864923965283923247190377093799334246328145) * 10 ^ 70 + 7119609377758410930907137667225818025278603897737437886426133059241660)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_315 :
Polynomial.coeff recurrence4B3A3 315 = -((15 * 10 ^ 70 + 5868348938052610382906352076753718391412462847420577304753287069869472) * 10 ^ 70 + 1061901066252889297710900147119053176262338268438388678094558412155443)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_316 :
Polynomial.coeff recurrence4B3A3 316 = (1 * 10 ^ 70 + 2779243995993513209732663323458124153942772012078435867293862970963691) * 10 ^ 70 + 1560115160698592202667808273033700188817974808969859729551656043732753
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_317 :
Polynomial.coeff recurrence4B3A3 317 = -(317330627654217927513646629430620937703208792437694326518896027399846 * 10 ^ 70 + 9868700659074632124382432469520586231209879900295293101573498500118295)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_318 :
Polynomial.coeff recurrence4B3A3 318 = -(5574553762225364730270374481381245788282690118943645090392666321990 * 10 ^ 70 + 7794682829727789728385253064951361319405222288094216713262714990363745)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_319 :
Polynomial.coeff recurrence4B3A3 319 = 427882495424271404063921190374980547599717348877874646432677364713 * 10 ^ 70 + 3119813578208334202928951345175719111125560673885800834092899411753063
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_320 :
Polynomial.coeff recurrence4B3A3 320 = -(1575810441584659592235991083819609706001859068070067095944294764 * 10 ^ 70 + 2953865673918564850217387618083219159923562502361350165782077902846610)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_321 :
Polynomial.coeff recurrence4B3A3 321 = -(200106119016883849057575081102329832389066520130639342489022975 * 10 ^ 70 + 7864490674812043303084662457604831334339873255969893206445481492537674)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_322 :
Polynomial.coeff recurrence4B3A3 322 = -(293060071971965252058838075360775851430710243919083327073279 * 10 ^ 70 + 6466946528580022743568151013463476807329541090362690515206142629563358)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_323 :
Polynomial.coeff recurrence4B3A3 323 = 31473773542116605867524346515895291259965244236146774152210 * 10 ^ 70 + 7874119695026904505095476950133747934522273952136799899035332231691661
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_324 :
Polynomial.coeff recurrence4B3A3 324 = 238537492799216512239845012553089252287045226110124150211 * 10 ^ 70 + 5620871676227918393337011569108152922340903929037746156523409630203829
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_325 :
Polynomial.coeff recurrence4B3A3 325 = -(251473147568101933861687218486926663765461805101743617 * 10 ^ 70 + 5026804860613764078902133680383832400630310154240861041237973554919330)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_326 :
Polynomial.coeff recurrence4B3A3 326 = -(7943795490208979660731966067078416402396322330642522 * 10 ^ 70 + 7784406139579207214086300612147736024950539908803681327363331435677257)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_327 :
Polynomial.coeff recurrence4B3A3 327 = -(19572123682627594333355280293530555853560363889726 * 10 ^ 70 + 4888996514519526668529162249216550890541986681254422960000180313659206)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_328 :
Polynomial.coeff recurrence4B3A3 328 = 49044383273069594192215275324609207071273977446 * 10 ^ 70 + 6921118333425870886547895626665093204877151782959119700063431593177349
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_329 :
Polynomial.coeff recurrence4B3A3 329 = 218709142101810839237031500354437963693586138 * 10 ^ 70 + 4579222343651986271261463427304159119087993809946306673236354068529789
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_330 :
Polynomial.coeff recurrence4B3A3 330 = -(60004249742314093267578794505736980946052 * 10 ^ 70 + 1105745174715541101482667058952703227816928851904477850765610849585478)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_331 :
Polynomial.coeff recurrence4B3A3 331 = -(840638672159945688743309984756051385286 * 10 ^ 70 + 8388367790896634248341095998622976500818219655659074550094455143574590)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_332 :
Polynomial.coeff recurrence4B3A3 332 = -(165659312141218293867449781303076216 * 10 ^ 70 + 2046031640619215027073065749503410593348133922449287338762814837606655)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_333 :
Polynomial.coeff recurrence4B3A3 333 = 1212001109888034307098170814910321 * 10 ^ 70 + 7912392627639626502438776679015621806331289963656344347858379244799983
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_334 :
Polynomial.coeff recurrence4B3A3 334 = 328860541003318769874109782885 * 10 ^ 70 + 8053413055461951673209807210728983565833526526049463871258386162152279
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_335 :
Polynomial.coeff recurrence4B3A3 335 = -(369500153938215449772847787 * 10 ^ 70 + 9351561765160702305709875762529361571665332434167421323643597521176251)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_336 :
Polynomial.coeff recurrence4B3A3 336 = -(66536024543333453476876 * 10 ^ 70 + 5450429728863595495519312035827577652856927836333371756100495037165913)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_337 :
Polynomial.coeff recurrence4B3A3 337 = 12158166416674343972 * 10 ^ 70 + 9002068886828204118173479283073346698071546516559989376961435496564061
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_338 :
Polynomial.coeff recurrence4B3A3 338 = 982969062409953 * 10 ^ 70 + 7034253323484021467754744900538373403774585602812795169936281113722707
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_339 :
Polynomial.coeff recurrence4B3A3 339 = -(28695655203 * 10 ^ 70 + 2055258521498779536182837052564263457142942940090194521729540794731061)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_340 :
Polynomial.coeff recurrence4B3A3 340 = -(754026 * 10 ^ 70 + 8708015096502294711013361743276974093548983857075751147043306978783578)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_341 :
Polynomial.coeff recurrence4B3A3 341 = 2 * 10 ^ 70 + 9956417577900696938560386782097165574218696177621852968589296437430283
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_342 :
Polynomial.coeff recurrence4B3A3 342 = 166200577260865696213783152421897361960008116830691993548602083809
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_343 :
Polynomial.coeff recurrence4B3A3 343 = -65964408095844150986211479570731191572132853184750281546146
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_344 :
Polynomial.coeff recurrence4B3A3 344 = -37067519174062366567404384624756845455296850857098735
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_345 :
Polynomial.coeff recurrence4B3A3 345 = 784397845382310995461708061609246340245151660
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_346 :
Polynomial.coeff recurrence4B3A3 346 = 8446737236647738989518319492449559300