Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
Download

Proofs of Lemma 4, 8 and 9 in the paper "On a simple quartic family of Thue equations over imaginary quadratic number fields" by Benjamin Earp-Lynch, Eva G. Goedhart, Ingrid Vukusic and Daniel P. Wisniewski.

22 views
unlisted
ubuntu2204
Kernel: SageMath 9.7

Proof of Lemma 4 (mostly computed "by hand')

# approximation of alpha

S.<s> = PowerSeriesRing(QQ,'s',10)
R.<x> = S[]

f = x^4 - (1/s) * x^3 - 6 * x^2 + (1/s) * x + 1
fprime = derivative(f,x)

x0 = 0
k = 3

for i in range(1,k+1):
    xnew = x0 - f(x0)/fprime(x0)
    x0 = xnew

alpha = x0
print("alpha =", alpha)
print("where s = t^(-1)")
alpha = -s + 5*s^3 - 46*s^5 + 509*s^7 - 6170*s^9 + 78994*s^11 + O(s^13) where s = t^(-1) 
# Rouche for alpha^(0)

print("alpha^(0) =", alpha)

bt = -s # approximation to alpha
print("used approximation:", bt)

# |z| = 5.01 |t|^-3
fixedconst = 5.01 
fixedexpo = -3 
print("|z| =", fixedconst, "* |t| ^", fixedexpo)

# compute upper bound for |h(0)|
h0 = f(bt)
expos = h0.exponents()
expinbound = - min(expos) # exponent of |t| in upper bound for |h(0)|
coeffs = h0.coefficients()
ubh0 = add([abs(coeffs[j] * 100^(-expos[j] - expinbound)) for j in range(0,len(coeffs))])
print("|h(0)| <= ", ubh0.n(), "* |t| ^", expinbound)

# compute lower bound for |h(z) - h(0)| 
T.<z> = S[]
print("h(z)- h(0) =",  f(bt + z) - f(bt))
mainterm = s^-1 * z # set manually after looking at h(z)- h(0)
print("main term:", mainterm)
expomainterm = -2 # set manually after looking at mainterm, exponent of |t| in mainterm
absmainterm = fixedconst # set manually after looking at mainterm
print("|main term| =", absmainterm, "* |t| ^", expomainterm)
print("Exponents of |t| in bounds match?", expinbound == expomainterm)
tobound = f(bt + z) - f(bt) - mainterm # want to bound this part from above
print("next: find upper bound for: |", tobound, "|")
expos = tobound.exponents() # exponents of z
coeffs = tobound.coefficients() # coefficients of z, z^, ...; in terms of powers of s
ub = 0
for i in range(0,len(expos)): # run through terms of shape (...) * z^(...)
    zexpo = expos[i] # exponent of z
    coefffromz = fixedconst^zexpo # constant that comes from z^(...)
    expofromz = fixedexpo * zexpo # exponent of |t| coming from the power of z
    subexpos = coeffs[i].exponents() # exponents of s
    subcoeffs = coeffs[i].coefficients() # coefficients of s
    for j in range(0,len(subexpos)): # run through expressions of shape (...) * s^(...)
        tempexpo = - subexpos[j] + expofromz - expinbound 
            # exponent of |t| in subexpression * z^(...) minus what we have in bound
        if tempexpo <= 0:
            tempbound = abs(subcoeffs[j]) * coefffromz * 100^tempexpo
            ub = ub + tempbound
        else: 
            print("!!! Can't bound from above because exponent of |t| is positive")
print("| ...| <=", ub, "* |t| ^", expinbound)
lowerbound = absmainterm - ub
print("|h(z)-h(0)| >= ", lowerbound, " * |t| ^", expinbound)
print("Bounds match?", ubh0 < lowerbound )
alpha^(0) = -s + 5*s^3 - 46*s^5 + 509*s^7 - 6170*s^9 + 78994*s^11 + O(s^13) used approximation: -s |z| = 5.01000000000000 * |t| ^ -3 |h(0)| <= 5.00010000000000 * |t| ^ -2 h(z)- h(0) = z^4 + (-s^-1 - 4*s)*z^3 + (-3 + 6*s^2)*z^2 + (s^-1 + 9*s - 4*s^3)*z main term: (s^-1)*z |main term| = 5.01000000000000 * |t| ^ -2 Exponents of |t| in bounds match? True next: find upper bound for: | z^4 + (-s^-1 - 4*s)*z^3 + (-3 + 6*s^2)*z^2 + (9*s - 4*s^3)*z | | ...| <= 0.00450995367940241 * |t| ^ -2 |h(z)-h(0)| >= 5.00549004632060 * |t| ^ -2 Bounds match? True 
# Rouche for alpha^(1)

alpha1 = (alpha-1)/(alpha+1)
print("alpha^(1) =", alpha1)

bt = -1 # approximation to alpha^(1)
print("used approximation:", bt)

# |z| = 2.16 |t|^-1
fixedconst = 2.16 
fixedexpo = -1
print("|z| =", fixedconst, "* |t| ^", fixedexpo)

# compute upper bound for |h(0)|
h0 = f(bt)
expos = h0.exponents()
expinbound = - min(expos) # exponent of |t| in upper bound for |h(0)|
coeffs = h0.coefficients()
ubh0 = add([abs(coeffs[j] * 100^(-expos[j] - expinbound)) for j in range(0,len(coeffs))])
print("|h(0)| <= ", ubh0.n(), "* |t| ^", expinbound)

# compute lower bound for |h(z) - h(0)| 
T.<z> = S[]
print("h(z)- h(0) =",  f(bt + z) - f(bt))
mainterm = - 2 * s^-1 * z # set manually after looking at h(z)- h(0)
print("main term:", mainterm)
expomainterm = 0 # set manually after looking at mainterm, exponent of |t| in mainterm
absmainterm = 2 * fixedconst # set manually after looking at mainterm
print("|main term| =", absmainterm, "* |t| ^", expomainterm)
print("Exponents of |t| in bounds match?", expinbound == expomainterm)
tobound = f(bt + z) - f(bt) - mainterm # want to bound this part from above
print("next: find upper bound for: |", tobound, "|")
expos = tobound.exponents() # exponents of z
coeffs = tobound.coefficients() # coefficients of z, z^, ...; in terms of powers of s
ub = 0
for i in range(0,len(expos)): # run through terms of shape (...) * z^(...)
    zexpo = expos[i] # exponent of z
    coefffromz = fixedconst^zexpo # constant that comes from z^(...)
    expofromz = fixedexpo * zexpo # exponent of |t| coming from the power of z
    subexpos = coeffs[i].exponents() # exponents of s
    subcoeffs = coeffs[i].coefficients() # coefficients of s
    for j in range(0,len(subexpos)): # run through expressions of shape (...) * s^(...)
        tempexpo = - subexpos[j] + expofromz - expinbound 
            # exponent of |t| in subexpression * z^(...) minus what we have in bound
        if tempexpo <= 0:
            tempbound = abs(subcoeffs[j]) * coefffromz * 100^tempexpo
            ub = ub + tempbound
        else: 
            print("!!! Can't bound from above because exponent of |t| is positive")
print("| ...| <=", ub, "* |t| ^", expinbound)
lowerbound = absmainterm - ub
print("|h(z)-h(0)| >= ", lowerbound, " * |t| ^", expinbound)
print("Bounds match?", ubh0 < lowerbound )
alpha^(1) = -1 - 2*s - 2*s^2 + 8*s^3 + 18*s^4 - 64*s^5 - 196*s^6 + 640*s^7 + 2346*s^8 - 7168*s^9 - 29724*s^10 + 86016*s^11 + 391220*s^12 + O(s^13) used approximation: -1 |z| = 2.16000000000000 * |t| ^ -1 |h(0)| <= 4.00000000000000 * |t| ^ 0 h(z)- h(0) = z^4 + (-s^-1 - 4)*z^3 + (3*s^-1)*z^2 + (-2*s^-1 + 8)*z main term: (-2*s^-1)*z |main term| = 4.32000000000000 * |t| ^ 0 Exponents of |t| in bounds match? True next: find upper bound for: | z^4 + (-s^-1 - 4)*z^3 + (3*s^-1)*z^2 + 8*z | | ...| <= 0.313816298062234 * |t| ^ 0 |h(z)-h(0)| >= 4.00618370193777 * |t| ^ 0 Bounds match? True 
# Rouche for alpha^(2)

alpha2 = -1/alpha
print("alpha^(2) =", alpha2)

bt = s^-1 # approximation to alpha^(2)
print("used approximation:", bt)

# |z| = 5.02 |t|^-1
fixedconst = 5.02 
fixedexpo = -1
print("|z| =", fixedconst, "* |t| ^", fixedexpo)

# compute upper bound for |h(0)|
h0 = f(bt)
expos = h0.exponents()
expinbound = - min(expos) # exponent of |t| in upper bound for |h(0)|
coeffs = h0.coefficients()
ubh0 = add([abs(coeffs[j] * 100^(-expos[j] - expinbound)) for j in range(0,len(coeffs))])
print("|h(0)| <= ", ubh0.n(), "* |t| ^", expinbound)

# compute lower bound for |h(z) - h(0)| 
T.<z> = S[]
print("h(z)- h(0) =",  f(bt + z) - f(bt))
mainterm = s^-3 * z # set manually after looking at h(z)- h(0)
print("main term:", mainterm)
expomainterm = 2 # set manually after looking at mainterm, exponent of |t| in mainterm
absmainterm = fixedconst # set manually after looking at mainterm
print("|main term| =", absmainterm, "* |t| ^", expomainterm)
print("Exponents of |t| in bounds match?", expinbound == expomainterm)
tobound = f(bt + z) - f(bt) - mainterm # want to bound this part from above
print("next: find upper bound for: |", tobound, "|")
expos = tobound.exponents() # exponents of z
coeffs = tobound.coefficients() # coefficients of z, z^, ...; in terms of powers of s
ub = 0
for i in range(0,len(expos)): # run through terms of shape (...) * z^(...)
    zexpo = expos[i] # exponent of z
    coefffromz = fixedconst^zexpo # constant that comes from z^(...)
    expofromz = fixedexpo * zexpo # exponent of |t| coming from the power of z
    subexpos = coeffs[i].exponents() # exponents of s
    subcoeffs = coeffs[i].coefficients() # coefficients of s
    for j in range(0,len(subexpos)): # run through expressions of shape (...) * s^(...)
        tempexpo = - subexpos[j] + expofromz - expinbound 
            # exponent of |t| in subexpression * z^(...) minus what we have in bound
        if tempexpo <= 0:
            tempbound = abs(subcoeffs[j]) * coefffromz * 100^tempexpo
            ub = ub + tempbound
        else: 
            print("!!! Can't bound from above because exponent of |t| is positive")
print("| ...| <=", ub, "* |t| ^", expinbound)
lowerbound = absmainterm - ub
print("|h(z)-h(0)| >= ", lowerbound, " * |t| ^", expinbound)
print("Bounds match?", ubh0 < lowerbound )
alpha^(2) = s^-1 + 5*s - 21*s^3 + 174*s^5 - 1789*s^7 + 20506*s^9 + O(s^11) used approximation: s^-1 |z| = 5.02000000000000 * |t| ^ -1 |h(0)| <= 5.00010000000000 * |t| ^ 2 h(z)- h(0) = z^4 + (3*s^-1)*z^3 + (3*s^-2 - 6)*z^2 + (s^-3 - 11*s^-1)*z main term: (s^-3)*z |main term| = 5.02000000000000 * |t| ^ 2 Exponents of |t| in bounds match? True next: find upper bound for: | z^4 + (3*s^-1)*z^3 + (3*s^-2 - 6)*z^2 + (-11*s^-1)*z | | ...| <= 0.0130874278393002 * |t| ^ 2 |h(z)-h(0)| >= 5.00691257216070 * |t| ^ 2 Bounds match? True 
# Rouche for alpha^(3)

alpha3 = -(alpha+1)/(alpha-1)
print("alpha^(3) =", alpha3)

bt = 1 # approximation to alpha^(3)
print("used approximation:", bt)

# |z| = 2.16 |t|^-1
fixedconst = 2.16 
fixedexpo = -1 
print("|z| =", fixedconst, "* |t| ^", fixedexpo)

# compute upper bound for |h(0)|
h0 = f(bt)
expos = h0.exponents()
expinbound = - min(expos) # exponent of |t| in upper bound for |h(0)|
coeffs = h0.coefficients()
ubh0 = add([abs(coeffs[j] * 100^(-expos[j] - expinbound)) for j in range(0,len(coeffs))])
print("|h(0)| <= ", ubh0.n(), "* |t| ^", expinbound)

# compute lower bound for |h(z) - h(0)| 
T.<z> = S[]
print("h(z)- h(0) =",  f(bt + z) - f(bt))
mainterm = -2 * s^-1 * z # set manually after looking at h(z)- h(0)
print("main term:", mainterm)
expomainterm = 0 # set manually after looking at mainterm, exponent of |t| in mainterm
absmainterm = 2 * fixedconst # set manually after looking at mainterm
print("|main term| =", absmainterm, "* |t| ^", expomainterm)
print("Exponents of |t| in bounds match?", expinbound == expomainterm)
tobound = f(bt + z) - f(bt) - mainterm # want to bound this part from above
print("next: find upper bound for: |", tobound, "|")
expos = tobound.exponents() # exponents of z
coeffs = tobound.coefficients() # coefficients of z, z^, ...; in terms of powers of s
ub = 0
for i in range(0,len(expos)): # run through terms of shape (...) * z^(...)
    zexpo = expos[i] # exponent of z
    coefffromz = fixedconst^zexpo # constant that comes from z^(...)
    expofromz = fixedexpo * zexpo # exponent of |t| coming from the power of z
    subexpos = coeffs[i].exponents() # exponents of s
    subcoeffs = coeffs[i].coefficients() # coefficients of s
    for j in range(0,len(subexpos)): # run through expressions of shape (...) * s^(...)
        tempexpo = - subexpos[j] + expofromz - expinbound 
            # exponent of |t| in subexpression * z^(...) minus what we have in bound
        if tempexpo <= 0:
            tempbound = abs(subcoeffs[j]) * coefffromz * 100^tempexpo
            ub = ub + tempbound
        else: 
            print("!!! Can't bound from above because exponent of |t| is positive")
print("| ...| <=", ub, "* |t| ^", expinbound)
lowerbound = absmainterm - ub
print("|h(z)-h(0)| >= ", lowerbound, " * |t| ^", expinbound)
print("Bounds match?", ubh0 < lowerbound )
alpha^(3) = 1 - 2*s + 2*s^2 + 8*s^3 - 18*s^4 - 64*s^5 + 196*s^6 + 640*s^7 - 2346*s^8 - 7168*s^9 + 29724*s^10 + 86016*s^11 - 391220*s^12 + O(s^13) used approximation: 1 |z| = 2.16000000000000 * |t| ^ -1 |h(0)| <= 4.00000000000000 * |t| ^ 0 h(z)- h(0) = z^4 + (-s^-1 + 4)*z^3 + (-3*s^-1)*z^2 + (-2*s^-1 - 8)*z main term: (-2*s^-1)*z |main term| = 4.32000000000000 * |t| ^ 0 Exponents of |t| in bounds match? True next: find upper bound for: | z^4 + (-s^-1 + 4)*z^3 + (-3*s^-1)*z^2 - 8*z | | ...| <= 0.313816298062234 * |t| ^ 0 |h(z)-h(0)| >= 4.00618370193777 * |t| ^ 0 Bounds match? True

Proof of Lemma 8

# approximation of alpha

S.<s> = PowerSeriesRing(QQ,'s',31)
R.<x> = S[]

f = x^4 - (1/s) * x^3 - 6 * x^2 + (1/s) * x + 1
fprime = derivative(f,x)

x0 = 0
k = 15

for i in range(1,k+1):
    xnew = x0 - f(x0)/fprime(x0)
    x0 = xnew

alpha = x0
print("alpha =", alpha)
print("where s = t^(-1)")
alpha = -s + 5*s^3 - 46*s^5 + 509*s^7 - 6170*s^9 + 78994*s^11 - 1048956*s^13 + 14297885*s^15 - 198756386*s^17 + 2805592454*s^19 - 40092539460*s^21 + 578731619634*s^23 - 8424489620932*s^25 + 123511225534724*s^27 - 1821914025180536*s^29 + 27018244217543517*s^31 - 402539671931650162*s^33 + O(s^34) where s = t^(-1) 
# Rouche for alpha^(0) better approximation

bt = alpha.truncate(30) # approximation to alpha
print("used approximation:", bt)

# |z| = 2.71 * 10^16 * |t|^-31
fixedconst = 2.71 * 10^16
fixedexpo = -31
print("|z| =", fixedconst, "* |t| ^", fixedexpo)

# compute upper bound for |h(0)|
h0 = f(bt)
expos = h0.exponents()
expinbound = - min(expos) # exponent of |t| in upper bound for |h(0)|
coeffs = h0.coefficients()
ubh0 = add([abs(coeffs[j] * 100^(-expos[j] - expinbound)) for j in range(0,len(coeffs))])
print("|h(0)| <= ", ubh0.n(), "* |t| ^", expinbound)

# compute lower bound for |h(z) - h(0)| 
T.<z> = S[]
print("h(z)- h(0) =",  f(bt + z) - f(bt))
mainterm = s^-1 * z # set manually after looking at h(z)- h(0)
print("main term:", mainterm)
expomainterm = -30 # set manually after looking at mainterm, exponent of |t| in mainterm
absmainterm = fixedconst # set manually after looking at mainterm
print("|main term| =", absmainterm, "* |t| ^", expomainterm)
print("Exponents of |t| in bounds match?", expinbound == expomainterm)
tobound = f(bt + z) - f(bt) - mainterm # want to bound this part from above
print("next: find upper bound for: |", tobound, "|")
expos = tobound.exponents() # exponents of z
coeffs = tobound.coefficients() # coefficients of z, z^, ...; in terms of powers of s
ub = 0
for i in range(0,len(expos)): # run through terms of shape (...) * z^(...)
    zexpo = expos[i] # exponent of z
    coefffromz = fixedconst^zexpo # constant that comes from z^(...)
    expofromz = fixedexpo * zexpo # exponent of |t| coming from the power of z
    subexpos = coeffs[i].exponents() # exponents of s
    subcoeffs = coeffs[i].coefficients() # coefficients of s
    for j in range(0,len(subexpos)): # run through expressions of shape (...) * s^(...)
        tempexpo = - subexpos[j] + expofromz - expinbound 
            # exponent of |t| in subexpression * z^(...) minus what we have in bound
        if tempexpo <= 0:
            tempbound = abs(subcoeffs[j]) * coefffromz * 100^tempexpo
            ub = ub + tempbound
        else: 
            print("!!! Can't bound from above because exponent of |t| is positive")
print("| ...| <=", ub, "* |t| ^", expinbound)
lowerbound = absmainterm - ub
print("|h(z)-h(0)| >= ", lowerbound, " * |t| ^", expinbound)
print("Bounds match?", ubh0 < lowerbound )
used approximation: -s + 5*s^3 - 46*s^5 + 509*s^7 - 6170*s^9 + 78994*s^11 - 1048956*s^13 + 14297885*s^15 - 198756386*s^17 + 2805592454*s^19 - 40092539460*s^21 + 578731619634*s^23 - 8424489620932*s^25 + 123511225534724*s^27 - 1821914025180536*s^29 |z| = 2.71000000000000e16 * |t| ^ -31 |h(0)| <= 2.70341965865559e16 * |t| ^ -30 h(z)- h(0) = z^4 + (-s^-1 - 4*s + 20*s^3 - 184*s^5 + 2036*s^7 - 24680*s^9 + 315976*s^11 - 4195824*s^13 + 57191540*s^15 - 795025544*s^17 + 11222369816*s^19 - 160370157840*s^21 + 2314926478536*s^23 - 33697958483728*s^25 + 494044902138896*s^27 - 7287656100722144*s^29)*z^3 + (-3 - 9*s^2 + 78*s^4 - 825*s^6 + 9642*s^8 - 119706*s^10 + 1547772*s^12 - 20606217*s^14 + 280466130*s^16 - 3883895166*s^18 + 54536954244*s^20 - 774598817034*s^22 + 11107495850724*s^24 - 160577122992660*s^26 + 2337685870950264*s^28 + 46815221639518062*s^30 - 379220818332252312*s^32 + 4155505008622222272*s^34 - 49114014883077573120*s^36 + 600164821452741341712*s^38 - 7457285192807355063744*s^40 + 93346427797979436462528*s^42 - 1169240002030140757423104*s^44 + 14566362431181398176791480*s^46 - 179267345367587501136759264*s^48 + 2160132290766775775488750656*s^50 - 25139019506550067299545839104*s^52 + 275714486542903163392433491680*s^54 - 2700322008827400032606843184768*s^56 + 19916224290897256595204359483776*s^58)*z^2 + (s^-1 + 9*s - 34*s^3 + 261*s^5 - 2526*s^7 + 27530*s^9 - 322692*s^11 + 3973677*s^13 - 50710534*s^15 + 664892958*s^17 - 8904743772*s^19 + 121315811234*s^21 - 1676204224044*s^23 + 23434638041268*s^25 - 330935697537032*s^27 + 4713857073589629*s^29 + 94459292029323672*s^31 - 951620475980714636*s^33 + 10471270091652590424*s^35 - 119338995231695385252*s^37 + 1376885290173781875432*s^39 - 15838115064363629905080*s^41 + 178927857776570087327088*s^43 - 1945035831650218022814664*s^45 + 19605650108216399533869480*s^47 - 167218269707107304235932856*s^49 + 792200878892618984327115568*s^51 + 11744712026154633824372805672*s^53 - 506651910281213899250904463248*s^55 + 12287684270875240741807018766576*s^57 - 251655511675987277954183819741664*s^59 + 2563142095751376298552472065773840*s^61 - 29155763878491818984761711878669792*s^63 + 339775831257723604008225747505578720*s^65 - 3985808324048204682500252994841300416*s^67 + 46658879210754554323480698649726577376*s^69 - 541586977206267589183360230447494330688*s^71 + 6195088350767341092216648253737907678656*s^73 - 69343680545304144657015315525076559095168*s^75 + 752598635250017950694146212271066236270720*s^77 - 7816355995325993044172245254458998267773696*s^79 + 76086633217511630268969324557960096130665216*s^81 - 669088130302295416864317622962358502819882496*s^83 + 4919754540386319257877528401591194612405275648*s^85 - 24190432242817991395605331600870045734775322624*s^87)*z main term: (s^-1)*z |main term| = 2.71000000000000e16 * |t| ^ -30 Exponents of |t| in bounds match? True next: find upper bound for: | z^4 + (-s^-1 - 4*s + 20*s^3 - 184*s^5 + 2036*s^7 - 24680*s^9 + 315976*s^11 - 4195824*s^13 + 57191540*s^15 - 795025544*s^17 + 11222369816*s^19 - 160370157840*s^21 + 2314926478536*s^23 - 33697958483728*s^25 + 494044902138896*s^27 - 7287656100722144*s^29)*z^3 + (-3 - 9*s^2 + 78*s^4 - 825*s^6 + 9642*s^8 - 119706*s^10 + 1547772*s^12 - 20606217*s^14 + 280466130*s^16 - 3883895166*s^18 + 54536954244*s^20 - 774598817034*s^22 + 11107495850724*s^24 - 160577122992660*s^26 + 2337685870950264*s^28 + 46815221639518062*s^30 - 379220818332252312*s^32 + 4155505008622222272*s^34 - 49114014883077573120*s^36 + 600164821452741341712*s^38 - 7457285192807355063744*s^40 + 93346427797979436462528*s^42 - 1169240002030140757423104*s^44 + 14566362431181398176791480*s^46 - 179267345367587501136759264*s^48 + 2160132290766775775488750656*s^50 - 25139019506550067299545839104*s^52 + 275714486542903163392433491680*s^54 - 2700322008827400032606843184768*s^56 + 19916224290897256595204359483776*s^58)*z^2 + (9*s - 34*s^3 + 261*s^5 - 2526*s^7 + 27530*s^9 - 322692*s^11 + 3973677*s^13 - 50710534*s^15 + 664892958*s^17 - 8904743772*s^19 + 121315811234*s^21 - 1676204224044*s^23 + 23434638041268*s^25 - 330935697537032*s^27 + 4713857073589629*s^29 + 94459292029323672*s^31 - 951620475980714636*s^33 + 10471270091652590424*s^35 - 119338995231695385252*s^37 + 1376885290173781875432*s^39 - 15838115064363629905080*s^41 + 178927857776570087327088*s^43 - 1945035831650218022814664*s^45 + 19605650108216399533869480*s^47 - 167218269707107304235932856*s^49 + 792200878892618984327115568*s^51 + 11744712026154633824372805672*s^53 - 506651910281213899250904463248*s^55 + 12287684270875240741807018766576*s^57 - 251655511675987277954183819741664*s^59 + 2563142095751376298552472065773840*s^61 - 29155763878491818984761711878669792*s^63 + 339775831257723604008225747505578720*s^65 - 3985808324048204682500252994841300416*s^67 + 46658879210754554323480698649726577376*s^69 - 541586977206267589183360230447494330688*s^71 + 6195088350767341092216648253737907678656*s^73 - 69343680545304144657015315525076559095168*s^75 + 752598635250017950694146212271066236270720*s^77 - 7816355995325993044172245254458998267773696*s^79 + 76086633217511630268969324557960096130665216*s^81 - 669088130302295416864317622962358502819882496*s^83 + 4919754540386319257877528401591194612405275648*s^85 - 24190432242817991395605331600870045734775322624*s^87)*z | | ...| <= 2.43992210799529e13 * |t| ^ -30 |h(z)-h(0)| >= 2.70756007789200e16 * |t| ^ -30 Bounds match? True

Proof of Lemma 9

# Rouche for alpha^(3) better approximation

alpha3 = -(alpha+1)/(alpha-1)
print("alpha^(3) =", alpha3)
print("where s = t^(-1)")

bt = alpha3.truncate(30) # approximation to alpha^(3)
print("used approximation:", bt)

# |z| = 9.84 * 10^15 * |t|^-30
fixedconst = 9.84 * 10^15
fixedexpo = -30
print("|z| =", fixedconst, "* |t| ^", fixedexpo)

# compute upper bound for |h(0)|
h0 = f(bt)
expos = h0.exponents()
expinbound = - min(expos) # exponent of |t| in upper bound for |h(0)|
coeffs = h0.coefficients()
ubh0 = add([abs(coeffs[j] * 100^(-expos[j] - expinbound)) for j in range(0,len(coeffs))])
print("|h(0)| <= ", ubh0.n(), "* |t| ^", expinbound)

# compute lower bound for |h(z) - h(0)| 
T.<z> = S[]
print("h(z)- h(0) =",  f(bt + z) - f(bt))
mainterm = -2 * s^-1 * z # set manually after looking at h(z)- h(0)
print("main term:", mainterm)
expomainterm = -29 # set manually after looking at mainterm, exponent of |t| in mainterm
absmainterm = 2 * fixedconst # set manually after looking at mainterm
print("|main term| =", absmainterm, "* |t| ^", expomainterm)
print("Exponents of |t| in bounds match?", expinbound == expomainterm)
tobound = f(bt + z) - f(bt) - mainterm # want to bound this part from above
print("next: find upper bound for: |", tobound, "|")
expos = tobound.exponents() # exponents of z
coeffs = tobound.coefficients() # coefficients of z, z^, ...; in terms of powers of s
ub = 0
for i in range(0,len(expos)): # run through terms of shape (...) * z^(...)
    zexpo = expos[i] # exponent of z
    coefffromz = fixedconst^zexpo # constant that comes from z^(...)
    expofromz = fixedexpo * zexpo # exponent of |t| coming from the power of z
    subexpos = coeffs[i].exponents() # exponents of s
    subcoeffs = coeffs[i].coefficients() # coefficients of s
    for j in range(0,len(subexpos)): # run through expressions of shape (...) * s^(...)
        tempexpo = - subexpos[j] + expofromz - expinbound 
            # exponent of |t| in subexpression * z^(...) minus what we have in bound
        if tempexpo <= 0:
            tempbound = abs(subcoeffs[j]) * coefffromz * 100^tempexpo
            ub = ub + tempbound
        else: 
            print("!!! Can't bound from above because exponent of |t| is positive")
print("| ...| <=", ub, "* |t| ^", expinbound)
lowerbound = absmainterm - ub
print("|h(z)-h(0)| >= ", lowerbound, " * |t| ^", expinbound)
print("Bounds match?", ubh0 < lowerbound )
alpha^(3) = 1 - 2*s + 2*s^2 + 8*s^3 - 18*s^4 - 64*s^5 + 196*s^6 + 640*s^7 - 2346*s^8 - 7168*s^9 + 29724*s^10 + 86016*s^11 - 391220*s^12 - 1081344*s^13 + 5291656*s^14 + 14057472*s^15 - 73061274*s^16 - 187432960*s^17 + 1025056044*s^18 + 2549088256*s^19 - 14567881052*s^20 - 35223764992*s^21 + 209232806328*s^22 + 493132709888*s^23 - 3031747059460*s^24 - 6979724509184*s^25 + 44259233299736*s^26 + 99710350131200*s^27 - 650285662207656*s^28 - 1435829041889280*s^29 + 9607853638811920*s^30 + 20819521107394560*s^31 - 142649856887260538*s^32 - 303720072625520640*s^33 + O(s^34) where s = t^(-1) used approximation: 1 - 2*s + 2*s^2 + 8*s^3 - 18*s^4 - 64*s^5 + 196*s^6 + 640*s^7 - 2346*s^8 - 7168*s^9 + 29724*s^10 + 86016*s^11 - 391220*s^12 - 1081344*s^13 + 5291656*s^14 + 14057472*s^15 - 73061274*s^16 - 187432960*s^17 + 1025056044*s^18 + 2549088256*s^19 - 14567881052*s^20 - 35223764992*s^21 + 209232806328*s^22 + 493132709888*s^23 - 3031747059460*s^24 - 6979724509184*s^25 + 44259233299736*s^26 + 99710350131200*s^27 - 650285662207656*s^28 - 1435829041889280*s^29 |z| = 9.84000000000000e15 * |t| ^ -30 |h(0)| <= 1.92618243597539e16 * |t| ^ -29 h(z)- h(0) = z^4 + (-s^-1 + 4 - 8*s + 8*s^2 + 32*s^3 - 72*s^4 - 256*s^5 + 784*s^6 + 2560*s^7 - 9384*s^8 - 28672*s^9 + 118896*s^10 + 344064*s^11 - 1564880*s^12 - 4325376*s^13 + 21166624*s^14 + 56229888*s^15 - 292245096*s^16 - 749731840*s^17 + 4100224176*s^18 + 10196353024*s^19 - 58271524208*s^20 - 140895059968*s^21 + 836931225312*s^22 + 1972530839552*s^23 - 12126988237840*s^24 - 27918898036736*s^25 + 177036933198944*s^26 + 398841400524800*s^27 - 2601142648830624*s^28 - 5743316167557120*s^29)*z^3 + (-3*s^-1 + 6 - 30*s + 24*s^2 + 102*s^3 - 192*s^4 - 732*s^5 + 1920*s^6 + 6750*s^7 - 21504*s^8 - 70884*s^9 + 258048*s^10 + 806460*s^11 - 3244032*s^12 - 9688632*s^13 + 42172416*s^14 + 121080462*s^15 - 562298880*s^16 - 1559104020*s^17 + 7647264768*s^18 + 20552525364*s^19 - 105671294976*s^20 - 276097234440*s^21 + 1479398129664*s^22 + 3767130775884*s^23 - 20939173527552*s^24 - 52072869662184*s^25 + 299131050393600*s^26 + 727801921368120*s^27 - 4307487125667840*s^28 + 18554205028033728*s^29 + 9622882978624320*s^30 - 301091723381554944*s^31 + 158557866139985976*s^32 + 3086632838261114880*s^33 - 2587152272276096160*s^34 - 34868935655451144192*s^35 + 35806907104191362688*s^36 + 411326280569343344640*s^37 - 476489402071520028288*s^38 - 4962262439358925504512*s^39 + 6228468935899293460800*s^40 + 60538648861883290877952*s^41 - 80287040044731179238912*s^42 - 741078667757805722664960*s^43 + 1018789807501473238268160*s^44 + 9041600850961926954418176*s^45 - 12659389912388960245310592*s^46 - 109157125494456316015411200*s^47 + 152584242387396912601822176*s^48 + 1292059287907700061964861440*s^49 - 1753678528952040695635025280*s^50 - 14787761842504369678533525504*s^51 + 18563237632253806963751030016*s^52 + 159659866787663530462908776448*s^53 - 165460520625671145391729335552*s^54 - 1540666843290464264918516367360*s^55 + 819224456893191613271507654016*s^56 + 11204388471863456292311043932160*s^57 + 12369630225196126685710673510400*s^58)*z^2 + (-2*s^-1 + 4 - 24*s + 24*s^2 + 64*s^3 - 168*s^4 - 384*s^5 + 1520*s^6 + 3072*s^7 - 15720*s^8 - 28672*s^9 + 176592*s^10 + 294912*s^11 - 2098704*s^12 - 3244032*s^13 + 25982688*s^14 + 37486592*s^15 - 331812840*s^16 - 449839104*s^17 + 4341928720*s^18 + 5561647104*s^19 - 57942850992*s^20 - 70447529984*s^21 + 785844050208*s^22 + 910398849024*s^23 - 10803171436176*s^24 - 11965242015744*s^25 + 150231355522080*s^26 + 159536560209920*s^27 - 2109917792988960*s^28 + 55493378270037600*s^29 + 39511385851735296*s^30 - 499869911190790428*s^31 + 250875114902042064*s^32 + 4484078128602600816*s^33 - 4602335079912040224*s^34 - 45505338099420587328*s^35 + 65554383605464157920*s^36 + 485262050333324890944*s^37 - 889467387188357180736*s^38 - 5268779087551195835040*s^39 + 11882353049814266545248*s^40 + 57025557690176924456448*s^41 - 157600228439418237704384*s^42 - 602068881667195198763136*s^43 + 2079392747286588318860736*s^44 + 6002082255952385182928448*s^45 - 27280835405588945627594880*s^46 - 52687917284490116301789168*s^47 + 355297386164413371515306784*s^48 + 317915730947393354797332288*s^49 - 4580972423861985688086795072*s^50 + 1342487602899968377354038656*s^51 + 58239367346857813342773503424*s^52 - 100783341950767866469534731648*s^53 - 725733045118341143244071577216*s^54 + 2595269929955659043521931573568*s^55 + 8781024309731446728174971426880*s^56 - 53726753692240252026135311558144*s^57 - 101495143007530982812835764556928*s^58 + 734108113277447710728555146827776*s^59 + 992581819501521473412430029086848*s^60 - 8540365615968635962138023797440512*s^61 - 9645892536279717928214072887334400*s^62 + 98563545995164274069246149751177216*s^63 + 100867322484823638477578239781276544*s^64 - 1141440723446277627571992021121105920*s^65 - 1090866174267816632461632118539430656*s^66 + 13182490026714199496859652770575155200*s^67 + 12020409789314360022720531294583633152*s^68 - 150916078362267906265549775107463839744*s^69 - 133928354816434611696745269037871040000*s^70 + 1702009327124527886058531544763423784960*s^71 + 1501358254788644493401881607241338036480*s^72 - 18770717053356248021102011110904150622208*s^73 - 16863583823713319669617170529258166370816*s^74 + 200480201426579814012983457045908153171968*s^75 + 188897533791520016310932320242009541538304*s^76 - 2044508776872816767526786004493249883930624*s^77 - 2095756374497058311512050007450686365980672*s^78 + 19460006916891709655042471464034766182940672*s^79 + 22760671840024170604673514077342047987473408*s^80 - 165834654102918094899443748771593535826690048*s^81 - 236476658826986927887415911957120099578083328*s^82 + 1153795179179048205926499807633121808712990720*s^83 + 2229378751019159885652426056576557202229467136*s^84 - 4819292855561994349122264441925984819567656960*s^85 - 16087586364511000511393116294448527006551244800*s^86 - 11840449543178688921813917525980348843819008000*s^87)*z main term: (-2*s^-1)*z |main term| = 1.96800000000000e16 * |t| ^ -29 Exponents of |t| in bounds match? True next: find upper bound for: | z^4 + (-s^-1 + 4 - 8*s + 8*s^2 + 32*s^3 - 72*s^4 - 256*s^5 + 784*s^6 + 2560*s^7 - 9384*s^8 - 28672*s^9 + 118896*s^10 + 344064*s^11 - 1564880*s^12 - 4325376*s^13 + 21166624*s^14 + 56229888*s^15 - 292245096*s^16 - 749731840*s^17 + 4100224176*s^18 + 10196353024*s^19 - 58271524208*s^20 - 140895059968*s^21 + 836931225312*s^22 + 1972530839552*s^23 - 12126988237840*s^24 - 27918898036736*s^25 + 177036933198944*s^26 + 398841400524800*s^27 - 2601142648830624*s^28 - 5743316167557120*s^29)*z^3 + (-3*s^-1 + 6 - 30*s + 24*s^2 + 102*s^3 - 192*s^4 - 732*s^5 + 1920*s^6 + 6750*s^7 - 21504*s^8 - 70884*s^9 + 258048*s^10 + 806460*s^11 - 3244032*s^12 - 9688632*s^13 + 42172416*s^14 + 121080462*s^15 - 562298880*s^16 - 1559104020*s^17 + 7647264768*s^18 + 20552525364*s^19 - 105671294976*s^20 - 276097234440*s^21 + 1479398129664*s^22 + 3767130775884*s^23 - 20939173527552*s^24 - 52072869662184*s^25 + 299131050393600*s^26 + 727801921368120*s^27 - 4307487125667840*s^28 + 18554205028033728*s^29 + 9622882978624320*s^30 - 301091723381554944*s^31 + 158557866139985976*s^32 + 3086632838261114880*s^33 - 2587152272276096160*s^34 - 34868935655451144192*s^35 + 35806907104191362688*s^36 + 411326280569343344640*s^37 - 476489402071520028288*s^38 - 4962262439358925504512*s^39 + 6228468935899293460800*s^40 + 60538648861883290877952*s^41 - 80287040044731179238912*s^42 - 741078667757805722664960*s^43 + 1018789807501473238268160*s^44 + 9041600850961926954418176*s^45 - 12659389912388960245310592*s^46 - 109157125494456316015411200*s^47 + 152584242387396912601822176*s^48 + 1292059287907700061964861440*s^49 - 1753678528952040695635025280*s^50 - 14787761842504369678533525504*s^51 + 18563237632253806963751030016*s^52 + 159659866787663530462908776448*s^53 - 165460520625671145391729335552*s^54 - 1540666843290464264918516367360*s^55 + 819224456893191613271507654016*s^56 + 11204388471863456292311043932160*s^57 + 12369630225196126685710673510400*s^58)*z^2 + (4 - 24*s + 24*s^2 + 64*s^3 - 168*s^4 - 384*s^5 + 1520*s^6 + 3072*s^7 - 15720*s^8 - 28672*s^9 + 176592*s^10 + 294912*s^11 - 2098704*s^12 - 3244032*s^13 + 25982688*s^14 + 37486592*s^15 - 331812840*s^16 - 449839104*s^17 + 4341928720*s^18 + 5561647104*s^19 - 57942850992*s^20 - 70447529984*s^21 + 785844050208*s^22 + 910398849024*s^23 - 10803171436176*s^24 - 11965242015744*s^25 + 150231355522080*s^26 + 159536560209920*s^27 - 2109917792988960*s^28 + 55493378270037600*s^29 + 39511385851735296*s^30 - 499869911190790428*s^31 + 250875114902042064*s^32 + 4484078128602600816*s^33 - 4602335079912040224*s^34 - 45505338099420587328*s^35 + 65554383605464157920*s^36 + 485262050333324890944*s^37 - 889467387188357180736*s^38 - 5268779087551195835040*s^39 + 11882353049814266545248*s^40 + 57025557690176924456448*s^41 - 157600228439418237704384*s^42 - 602068881667195198763136*s^43 + 2079392747286588318860736*s^44 + 6002082255952385182928448*s^45 - 27280835405588945627594880*s^46 - 52687917284490116301789168*s^47 + 355297386164413371515306784*s^48 + 317915730947393354797332288*s^49 - 4580972423861985688086795072*s^50 + 1342487602899968377354038656*s^51 + 58239367346857813342773503424*s^52 - 100783341950767866469534731648*s^53 - 725733045118341143244071577216*s^54 + 2595269929955659043521931573568*s^55 + 8781024309731446728174971426880*s^56 - 53726753692240252026135311558144*s^57 - 101495143007530982812835764556928*s^58 + 734108113277447710728555146827776*s^59 + 992581819501521473412430029086848*s^60 - 8540365615968635962138023797440512*s^61 - 9645892536279717928214072887334400*s^62 + 98563545995164274069246149751177216*s^63 + 100867322484823638477578239781276544*s^64 - 1141440723446277627571992021121105920*s^65 - 1090866174267816632461632118539430656*s^66 + 13182490026714199496859652770575155200*s^67 + 12020409789314360022720531294583633152*s^68 - 150916078362267906265549775107463839744*s^69 - 133928354816434611696745269037871040000*s^70 + 1702009327124527886058531544763423784960*s^71 + 1501358254788644493401881607241338036480*s^72 - 18770717053356248021102011110904150622208*s^73 - 16863583823713319669617170529258166370816*s^74 + 200480201426579814012983457045908153171968*s^75 + 188897533791520016310932320242009541538304*s^76 - 2044508776872816767526786004493249883930624*s^77 - 2095756374497058311512050007450686365980672*s^78 + 19460006916891709655042471464034766182940672*s^79 + 22760671840024170604673514077342047987473408*s^80 - 165834654102918094899443748771593535826690048*s^81 - 236476658826986927887415911957120099578083328*s^82 + 1153795179179048205926499807633121808712990720*s^83 + 2229378751019159885652426056576557202229467136*s^84 - 4819292855561994349122264441925984819567656960*s^85 - 16087586364511000511393116294448527006551244800*s^86 - 11840449543178688921813917525980348843819008000*s^87)*z | | ...| <= 4.17458626843309e14 * |t| ^ -29 |h(z)-h(0)| >= 1.92625413731567e16 * |t| ^ -29 Bounds match? True