Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupExceptional

Recurrence 5 lookup certificate: exceptional coefficient lookup #

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.recurrence5Exceptional_coeff_0 :
Polynomial.coeff exceptional5 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_1 :
Polynomial.coeff exceptional5 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_2 :
Polynomial.coeff exceptional5 2 = 1 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_3 :
Polynomial.coeff exceptional5 3 = -33 / 39988901703835833774702822118890342577443381752832020
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_4 :
Polynomial.coeff exceptional5 4 = -12857 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_5 :
Polynomial.coeff exceptional5 5 = -185833 / 99972254259589584436757055297225856443608454382080050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_6 :
Polynomial.coeff exceptional5 6 = -5596321 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_7 :
Polynomial.coeff exceptional5 7 = -43625367 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_8 :
Polynomial.coeff exceptional5 8 = -83007371 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_9 :
Polynomial.coeff exceptional5 9 = 73079311 / 9997225425958958443675705529722585644360845438208005
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_10 :
Polynomial.coeff exceptional5 10 = 5846971117 / 99972254259589584436757055297225856443608454382080050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_11 :
Polynomial.coeff exceptional5 11 = 2375957204 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_12 :
Polynomial.coeff exceptional5 12 = -245447424547 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_13 :
Polynomial.coeff exceptional5 13 = -770033174521 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_14 :
Polynomial.coeff exceptional5 14 = 726141228332 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_15 :
Polynomial.coeff exceptional5 15 = 14370548777889 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_16 :
Polynomial.coeff exceptional5 16 = -2928518330931 / 19994450851917916887351411059445171288721690876416010
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_17 :
Polynomial.coeff exceptional5 17 = -165270662414299 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_18 :
Polynomial.coeff exceptional5 18 = 165172173113061 / 99972254259589584436757055297225856443608454382080050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_19 :
Polynomial.coeff exceptional5 19 = 1263901517563683 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_20 :
Polynomial.coeff exceptional5 20 = -182052086108446 / 9997225425958958443675705529722585644360845438208005
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_21 :
Polynomial.coeff exceptional5 21 = -4744288554171373 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_22 :
Polynomial.coeff exceptional5 22 = 7169936665586104 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_23 :
Polynomial.coeff exceptional5 23 = -17807823205029481 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_24 :
Polynomial.coeff exceptional5 24 = -109135034667591369 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_25 :
Polynomial.coeff exceptional5 25 = 140996562775716843 / 99972254259589584436757055297225856443608454382080050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_26 :
Polynomial.coeff exceptional5 26 = -154750981476043511 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_27 :
Polynomial.coeff exceptional5 27 = -619630231440505233 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_28 :
Polynomial.coeff exceptional5 28 = 1890962459384133543 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_29 :
Polynomial.coeff exceptional5 29 = -740911643794187042 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_30 :
Polynomial.coeff exceptional5 30 = 43187395200102413 / 2701952817826745525317758251276374498475904172488650
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_31 :
Polynomial.coeff exceptional5 31 = -641325284806649048 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_32 :
Polynomial.coeff exceptional5 32 = 1577124548959608153 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_33 :
Polynomial.coeff exceptional5 33 = -746018908790785361 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_34 :
Polynomial.coeff exceptional5 34 = 66612249239833749 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_35 :
Polynomial.coeff exceptional5 35 = -67117380579095351 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_36 :
Polynomial.coeff exceptional5 36 = 2209865215767196 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_37 :
Polynomial.coeff exceptional5 37 = 1314723494770327 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_38 :
Polynomial.coeff exceptional5 38 = -1164910419752001 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_39 :
Polynomial.coeff exceptional5 39 = 96410003919333 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_40 :
Polynomial.coeff exceptional5 40 = -17280322500519 / 39988901703835833774702822118890342577443381752832020
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_41 :
Polynomial.coeff exceptional5 41 = 14504235379297 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_42 :
Polynomial.coeff exceptional5 42 = -1882452416113 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_43 :
Polynomial.coeff exceptional5 43 = 47558583852 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_44 :
Polynomial.coeff exceptional5 44 = -7432928163 / 99972254259589584436757055297225856443608454382080050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_45 :
Polynomial.coeff exceptional5 45 = 220175003 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_46 :
Polynomial.coeff exceptional5 46 = -38109181 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_47 :
Polynomial.coeff exceptional5 47 = 1124157 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_48 :
Polynomial.coeff exceptional5 48 = -4871 / 49986127129794792218378527648612928221804227191040025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_49 :
Polynomial.coeff exceptional5 49 = 117 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_50 :
Polynomial.coeff exceptional5 50 = 1 / 199944508519179168873514110594451712887216908764160100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_coeff_high (n : ℕ) (h : 50 < n) :
Polynomial.coeff exceptional5 n = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Exceptional_natDegree_le :
Polynomial.natDegree exceptional5 ≤ 50