Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupExceptionalProductPart1.Coefficients343To378

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_343 :
Polynomial.coeff recurrence5ExceptionalProduct 343 = (7582197290111909381421328635098845963352371611160117738703541828 * 10 ^ 70 + 6907906357427714071197671715511613701509049365022500756935774269678917) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_344 :
Polynomial.coeff recurrence5ExceptionalProduct 344 = -(204205471249649880589362071227466510801474048124190862534765133 * 10 ^ 70 + 1214445241703841171216559952246328720592412323141466655899031588967741) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_345 :
Polynomial.coeff recurrence5ExceptionalProduct 345 = (263986427114562881725370650821534679870772001494187681528089 * 10 ^ 70 + 643371081266209383411487476831421382534295175200062730509433214088807) / 184517613112223973198325
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_346 :
Polynomial.coeff recurrence5ExceptionalProduct 346 = -(328299462392443913875649644621377250626084740072553840119038 * 10 ^ 70 + 4381716177737281577040414181880120007604519034103140050505273018630717) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_347 :
Polynomial.coeff recurrence5ExceptionalProduct 347 = (59758307906542643461522475534133869497259335204930321055493 * 10 ^ 70 + 1612783805163677549924174115823711471540863791155652701738383583303907) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_348 :
Polynomial.coeff recurrence5ExceptionalProduct 348 = -(1852041798144544892675068888538525203065723081664136968679 * 10 ^ 70 + 787265236530834336405142003247072133060771134392645439794312508701617) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_349 :
Polynomial.coeff recurrence5ExceptionalProduct 349 = (4770453453130049493920931285106307513318115038479649467 * 10 ^ 70 + 4342773381594348765284520222616660769644955163230977844538107244951551) / 2730860674060914803335210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_350 :
Polynomial.coeff recurrence5ExceptionalProduct 350 = -(246449568717182431709627267134405216370557522334994649 * 10 ^ 70 + 956193205692904025940368159732633808240646682160582315189048009985096) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_351 :
Polynomial.coeff recurrence5ExceptionalProduct 351 = (154076707605336035765544053340397841535334260159000 * 10 ^ 70 + 3451854878848101881027282249442928607919081960790974929590662607490185) / 273086067406091480333521
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_352 :
Polynomial.coeff recurrence5ExceptionalProduct 352 = -(160640596721525440088820926188065499964091469356298 * 10 ^ 70 + 2813270221386080972976792583163528749725152269763427077516870092506643) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_353 :
Polynomial.coeff recurrence5ExceptionalProduct 353 = (672541224962670143011351225785205791314141198606 * 10 ^ 70 + 9952148279553709844753590276071902122097753089927235095860400957690873) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_354 :
Polynomial.coeff recurrence5ExceptionalProduct 354 = (1958292914456142551211501868297012317931495480 * 10 ^ 70 + 853267306125519930803125713636748346425396765604159790681038369402706) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_355 :
Polynomial.coeff recurrence5ExceptionalProduct 355 = -(128757643071223541211091554584829113598702958 * 10 ^ 70 + 5614637967822324082033224814087347936190008497707704306954267332611911) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_356 :
Polynomial.coeff recurrence5ExceptionalProduct 356 = (384045207830181277296159096709757468287017 * 10 ^ 70 + 6417605444654982014987874756594626657064742313225915330628233757657247) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_357 :
Polynomial.coeff recurrence5ExceptionalProduct 357 = (2236030982006977252179387511306034942023 * 10 ^ 70 + 6838214960620279235281797548633451027283051827392119307765313145421483) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_358 :
Polynomial.coeff recurrence5ExceptionalProduct 358 = -(29541263647844232707574902367062086816 * 10 ^ 70 + 5546038946731655814531092634002474420411242670628710015211981704470403) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_359 :
Polynomial.coeff recurrence5ExceptionalProduct 359 = -(43925810107717830038716976337951609 * 10 ^ 70 + 6899822804117434950661463361981616001761662693565664107124684615193633) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_360 :
Polynomial.coeff recurrence5ExceptionalProduct 360 = (331587602193031627477641773192578 * 10 ^ 70 + 1051119937696162650083424619671654194920172115416116312094921167529157) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_361 :
Polynomial.coeff recurrence5ExceptionalProduct 361 = -(542832619886123277997316862386 * 10 ^ 70 + 3486315025451789991769706136700413102855827703392408673113167444258621) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_362 :
Polynomial.coeff recurrence5ExceptionalProduct 362 = -(1466851697128710092172271778 * 10 ^ 70 + 5223520641403365346343268337730178674438261623388757573924235461825013) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_363 :
Polynomial.coeff recurrence5ExceptionalProduct 363 = (13681334102978870378166860 * 10 ^ 70 + 6454660127463254878534387438790119304499451105132869966714655722118229) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_364 :
Polynomial.coeff recurrence5ExceptionalProduct 364 = (860284965020279453707 * 10 ^ 70 + 2915074759728688126659646062692188420556522486308922748966871048618931) / 2730860674060914803335210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_365 :
Polynomial.coeff recurrence5ExceptionalProduct 365 = -(13589867853889713505 * 10 ^ 70 + 2227573640694823246104737658977084746086565172515998047286661021450007) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_366 :
Polynomial.coeff recurrence5ExceptionalProduct 366 = (101231014933921148 * 10 ^ 70 + 8763047239082891627559475266675388284788393817917374950301013834721501) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_367 :
Polynomial.coeff recurrence5ExceptionalProduct 367 = -(17788973154982 * 10 ^ 70 + 4257989170013289402629550167417187320934475852853250051161883520662753) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_368 :
Polynomial.coeff recurrence5ExceptionalProduct 368 = (13017865323 * 10 ^ 70 + 1681734961776809568008417042199244613127943107965238348350197896180287) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_369 :
Polynomial.coeff recurrence5ExceptionalProduct 369 = -(2465235 * 10 ^ 70 + 5323208847078780429496406443222801428345773441090479151627933895638107) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_370 :
Polynomial.coeff recurrence5ExceptionalProduct 370 = (118 * 10 ^ 70 + 700282994780651352612433478058520405535331938697583239871074270908174) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_371 :
Polynomial.coeff recurrence5ExceptionalProduct 371 = -21504891122472802553208266381028656288787472711548297392529514222757 / 2730860674060914803335210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_372 :
Polynomial.coeff recurrence5ExceptionalProduct 372 = 224013240194473025830142321787928855379984989101925825663648982 / 1365430337030457401667605
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_373 :
Polynomial.coeff recurrence5ExceptionalProduct 373 = -377985129306735110447359789354935170640294104296055234979 / 273086067406091480333521
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_374 :
Polynomial.coeff recurrence5ExceptionalProduct 374 = 126172775470916960259126666597957781024616544005586033 / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_375 :
Polynomial.coeff recurrence5ExceptionalProduct 375 = -126517018144915947155277336042476635597329697857 / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_376 :
Polynomial.coeff recurrence5ExceptionalProduct 376 = 41618300119571719020429822932379579198849 / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_377 :
Polynomial.coeff recurrence5ExceptionalProduct 377 = -195586437252026034978 / 2612881873555
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_378 :
Polynomial.coeff recurrence5ExceptionalProduct 378 = 1