The Main Bound Computations (L≥27+(1/50))

Here we assemble bounds on the relevant pieces and combine them to accomplish the bound in the Main Theorem.

Definitions

<<IntervalTools`

{Lmin,Lmax}={27+1/50,∞};
Linterval=Interval[{Lmin,Lmax}];
η[L_]=(18/(10+9L));
c[L_]=1+(391/(683+74L));
r[L_]=(149/140)+(769/(512+30L));
(Subscript[σ, 1])[L_]=c[L]+((((c[L]-1/2))^2)/(r[L]));
δ[L_]=2c[L]-(Subscript[σ, 1])[L]-(1/2);
(Subscript[θ, -η])[L_]=ArcCos[((-η[L]-c[L])/(r[L]))];
(Subscript[θ, 1+η])[L_]=ArcCos[((1+η[L]-c[L])/(r[L]))];
(Subscript[θ, 1-c])[L_]=ArcCos[((1-2c[L])/(r[L]))];

Reduce[D[η[L],L]≤0&&L≥27,L,Reals]
Reduce[D[c[L],L]≤0&&L≥27,L,Reals]
Reduce[D[r[L],L]≤0&&L≥27,L,Reals]
Reduce[D[(Subscript[σ, 1])[L],L]≤0&&L≥27,L,Reals]
Reduce[D[δ[L],L]≤0&&L≥27,L,Reals]
Reduce[D[(Subscript[θ, -η])[L],L]≥0&&L≥27,L,Reals]
Reduce[D[(Subscript[θ, 1+η])[L],L]≤ 0&&L≥27,L,Reals]
Reduce[D[(Subscript[θ, 1-c])[L],L]≥0&&L≥27,L,Reals]

Thus, the following interval enclosures are justified.  Actually, η, c,  r only contain one occurrence of L, and so are automatically sharp.

η[Lint_Interval]:=Block[{L},MonotoneEnclosure[η[L],L,Lint]];
c[Lint_Interval]:=Block[{L},MonotoneEnclosure[c[L],L,Lint]];
r[Lint_Interval]:=Block[{L},MonotoneEnclosure[r[L],L,Lint]];
(Subscript[σ, 1])[Lint_Interval]:=Block[{L},MonotoneEnclosure[(Subscript[σ, 1])[L],L,Lint]];
δ[Lint_Interval]:=Block[{L},MonotoneEnclosure[δ[L],L,Lint]];
(Subscript[θ, -η])[Lint_Interval]:=Block[{L},MonotoneEnclosure[(Subscript[θ, -η])[L],L,Lint]];
(Subscript[θ, 1+η])[Lint_Interval]:=Block[{L},MonotoneEnclosure[(Subscript[θ, 1+η])[L],L,Lint]];
(Subscript[θ, 1-c])[Lint_Interval]:=Block[{L},MonotoneEnclosure[(Subscript[θ, 1-c])[L],L,Lint]];

Additionally we will frequently encounter log((r/(c-1/2))), which is monotone decreasing:

Reduce[D[Log[((r[L])/(c[L]-1/2))],L]≤0&&L≥27,L,Reals]

logrc[L_]=Log[((r[L])/(c[L]-1/2))];
logrc[Lint_Interval]:=Block[{L},MonotoneEnclosure[Log[((r[L])/(c[L]-1/2))],L,Lint]]

Er[a_,d_,T_]=((4 (4+3 π))/(45 ((((((17+2 a))^2)+4 (T^2)))^(3/2))))-((4 T)/(3 ((((17+2 a))^2)+4 (T^2))))+((8+6 π)/(45 ((((((17+2 a-2 d))^2)+4 (T^2)))^(3/2))))+((2 T)/(3 ((((17+2 a-2 d))^2)+4 (T^2))))+((8+6 π)/(45 ((((((17+2 a+2 d))^2)+4 (T^2)))^(3/2))))+((2 T)/(3 ((((17+2 a+2 d))^2)+4 (T^2))))+2 ArcTan[((1+2 a)/(2 T))]+2 ArcTan[((5+2 a)/(2 T))]+2 ArcTan[((9+2 a)/(2 T))]+2 ArcTan[((13+2 a)/(2 T))]-(1/2) (15+2 a) ArcTan[((17+2 a)/(2 T))]-ArcTan[((1+2 a-2 d)/(2 T))]-ArcTan[((5+2 a-2 d)/(2 T))]-ArcTan[((9+2 a-2 d)/(2 T))]-ArcTan[((13+2 a-2 d)/(2 T))]+(1/4) (15+2 a-2 d) ArcTan[((17+2 a-2 d)/(2 T))]-ArcTan[((1+2 a+2 d)/(2 T))]-ArcTan[((5+2 a+2 d)/(2 T))]-ArcTan[((9+2 a+2 d)/(2 T))]-ArcTan[((13+2 a+2 d)/(2 T))]+(1/4) (15+2 a+2 d) ArcTan[((17+2 a+2 d)/(2 T))]+(1/2) T Log[1+((((17+2 a))^2)/(4 (T^2)))]-(1/4) T Log[1+((((17+2 a-2 d))^2)/(4 (T^2)))]-(1/4) T Log[1+((((17+2 a+2 d))^2)/(4 (T^2)))];

Bounds on the pieces

Domains for L,η,c,r,(Subscript[σ, 1]),δ

ηinterval=η[Linterval]
cinterval=c[Linterval]
rinterval=r[Linterval]
N[{ηinterval,cinterval,rinterval},3]

σ1interval=(Subscript[σ, 1])[Linterval]
δinterval=δ[Linterval]
N[{σ1interval,δinterval},3]

Inequalities: -(1/2)≤c[L]-r[L]≤1-c[L]≤-η[L]<0<1<1+η[L]<c[L]<(Subscript[σ, 1])[L]<c[L]+r[L]

-(1/2)<c[L]-r[L]<1-c[L]<-η[L]<0<1<1+η[L]<c[L]<(Subscript[σ, 1])[L]<c[L]+r[L]

N[Reduce[-(1/2)<c[L]-r[L]<1-c[L]<-η[L]<0<1<1+η[L]<c[L]<(Subscript[σ, 1])[L]<c[L]+r[L],L],30]
Reduce[-(1/2)<c[L]-r[L]<1-c[L]<-η[L]<0<1<1+η[L]<c[L]<(Subscript[σ, 1])[L]<c[L]+r[L]&&L≥(1351/50),L]

Bound: |g(a,T)|≤((2-a)/(50T))

In another file.

Bound: ((Subscript[E, δ])/π)≤(((640+216a)d-112-39a)/(1536(3T+3a-1)))+(1/(2^10))

In another file.

Bound 1: |g(a,T)|+((Subscript[E, δ])/π)≤(1/(2^10))+((1/14)/(T-1/5))

bound[1]=(1/(2^10))+((1/14)/(T-1/5));

Clear[f];
f[a_,d_,T_]=bound[1]-(((2-a)/(50T))+(((640+216a)d-112-39a)/(1536(3T+3a-1)))+(1/(2^10)));
(* for each a, the function f is monotone in d, and rational in T *)
f[a_,dint_Interval,Tint_Interval]:=IntervalHull[f[a,Min[dint],Tint],f[a,Max[dint],Tint]];
f[a_,d_,Tint_Interval]:=Module[{T,tmin=Min[Tint],tmax=Max[Tint],min,max},
min=First[Minimize[{f[a,d,T],tmin≤T≤tmax},T,Reals]];
max=First[Maximize[{f[a,d,T],tmin≤T≤tmax},T,Reals]];
Interval[{min,max}]];

δinterval

f[0,δinterval,Interval[{5/7,∞}]]
f[1,δinterval,Interval[{5/7,∞}]]

The warning messages are just acknowledging that the extreme values are happening as T->∞.

Bound 2:	 (2/π)Log[Zeta[(Subscript[σ, 1])]]-((Log[Zeta[2c]])/(Log[(r/(c-1/2))]))≤((80807+17909 L+178 (L^2))/(4 (164296+9637 L+128 (L^2))))

bound[2]=((80807+17909 L+178 (L^2))/(4 (164296+9637 L+128 (L^2))));

Clear[f];
f[L_]=bound[2]-((2/π)Log[Zeta[(Subscript[σ, 1])[L]]]-((Log[Zeta[2 c[L]]])/(Log[((r[L])/(c[L]-1/2))])));

Reduce[D[bound[2]]==0&&L≥27,L,Reals]

f[Lint_Interval]:=Module[{rat,L},
rat=MonotoneEnclosure[((80807+17909 L+178 (L^2))/(4 (164296+9637 L+128 (L^2)))),L,Lint];
rat-((2/π)Log[Zeta[(Subscript[σ, 1])[Lint]]]-((Log[Zeta[2 c[Lint]]])/(logrc[Lint])))];

N[f[Interval[{(2^15),∞}]],30]

Timing[{t0,t1,t2}=ProveNonNegative[f,f,{Linterval},MaxDepth->20];]
Length/@{t0,t1,t2}

Bound 3:	((1/π)/(Log[r/ (c-1/2) ]))(Subscript[κ, 1]) L≤(238413/(2^20))L+((80396+135589 L+798 (L^2))/(16 (38735+3105 L+32 (L^2))))

(Subscript[κ, 1])[L_]=((Subscript[θ, -η])[L]-(Subscript[θ, 1+η])[L])*((1+η[L]-c[L])/2)-(π-(Subscript[θ, -η])[L])(c[L]-(1/2))+((r[L](Sin[(Subscript[θ, -η])[L]]+Sin[(Subscript[θ, 1+η])[L]]))/2);

bound[3]=(238413/(2^20))L+((80396+135589 L+798 (L^2))/(16 (38735+3105 L+32 (L^2))));

This is done in another notebook.

Bound 4: 	((Log[Zeta[c]])/(2Log[(r/(c-1/2))]))((3/2)+(1/(2(Subscript[J, 1])))+(1/(Subscript[J, 2]))+((Subscript[θ, 1+η])/π)+(1-(1/(Subscript[J, 2])))((Subscript[θ, 1-c])/π)-((Subscript[θ, -η])/π))≤((149201-214796 L-1135 (L^2))/(496726+75117 L+512 (L^2)))+((1365 )/(2^10))Log[1+L]+(L/(2^20))

bound[4]=((149201-214796 L-1135 (L^2))/(496726+75117 L+512 (L^2)))+((1365 )/(2^10))Log[1+L]+(L/(2^20));

Clear[f];
f[L_]=Block[{J1=64,J2=24},

bound[4]-((Log[Zeta[c[L]]])/(2logrc[L]))((3/2)+(1/(2J1))+(1/J2)+(((Subscript[θ, 1+η])[L])/π)+(1-(1/J2))(((Subscript[θ, 1-c])[L])/π)-(((Subscript[θ, -η])[L])/π))]

Plot[f[L],{L,27.02,100},PlotRange->All]

logzetapluslog[1]=0;
logzetapluslog[s_]=Log[Zeta[s]]+Log[s-1];
logzetapluslog[sint_Interval]:=Block[{s},MonotoneEnclosure[logzetapluslog[s],s,sint]];

logoverlog[s_,x_]=((Log[s+x])/(Log[1+x]));
logoverlog[s_,xint_Interval]:=Block[{x},MonotoneEnclosure[logoverlog[s,x],x,xint]];

FullSimplify[f[L]==(L/(2^20))+((149201-214796 L-1135 (L^2))/(496726+75117 L+512 (L^2)))-((((595/384)-(((Subscript[θ, -η])[L])/π)+(((Subscript[θ, 1+η])[L])/π)+((23 (Subscript[θ, 1-c])[L])/(24 π))) )/(2 logrc[L]))(logzetapluslog[1+(391/(683+74 L))])+(((((595/384)-(((Subscript[θ, -η])[L])/π)+(((Subscript[θ, 1+η])[L])/π)+((23 (Subscript[θ, 1-c])[L])/(24 π))) )/(2 logrc[L]))((Log[(391/(683+74 L))])/(Log[1+L]))+(1365/1024))Log[1+L],Assumptions->L≥27+1/50]
FullSimplify[((Log[(391/(683+74 L))])/(Log[1+L]))==((-Log[(74/391)])/(Log[1+L]))-logoverlog[(683/74),L],Assumptions->L≥27+1/50]

Reduce[D[(L/1048576)+((149201-214796 L-1135 (L^2))/(496726+75117 L+512 (L^2))),L]≤0&&L≥Lmin,L,Reals]
Reduce[D[((Log[(391/(683+74 L))])/(Log[1+L])),L]≤0&&L≥(1351/50),L,Reals]

f[Lint_Interval]:=Module[{L,firstterms,coeff},
firstterms=PiecewiseMonotoneEnclosure[-(1135/512)+(L/1048576)+((640174922-24717757 L)/(512 (496726+75117 L+512 (L^2)))),L,{(NumericalApproximation[Root, (RowDefault["99.6", FEExpressionsNumericalApproximationElider]), Root[-123629264286806812-1342469492888260 #1+25924597975145 ((#1)^2)+76919808 ((#1)^3)+262144 ((#1)^4)&,2], ])},Lint];

coeff=((595/384)-(((Subscript[θ, -η])[Lint])/π)+(((Subscript[θ, 1+η])[Lint])/π)+((23 (Subscript[θ, 1-c])[Lint])/(24 π)))/(2logrc[Lint]);
firstterms-coeff(logzetapluslog[1+(391/(683+74 Lint))])+(coeff(((-Log[(74/391)])/(Log[1+Lint]))-logoverlog[(683/74),Lint])+(1365/1024))Log[1+Lint]];

Plot[f[L],{L,270.02,270.04}]
f[Interval[{270+1/50,270+2/50}]]//N

Timing[{fails,undec,proven}=ProveNonNegative[f,f,{Linterval},MaxDepth->20];]
{fails,undec,Length[proven]}

Bound 5: 	((Log[Zeta[1+η]])/(2Log[(r/(c-1/2))]))(-((Subscript[θ, 1+η])/π)+((Subscript[θ, 1-c])/π)+((Subscript[θ, -η])/π)-(1/2))≤((79045-118430 L-182 (L^2))/(599789+91562 L+512 (L^2)))+((529 )/(2^10))Log[1+L]+(L/(2^22))

bound[5]=((79045-118430 L-182 (L^2))/(599789+91562 L+512 (L^2)))+((529 )/(2^10))Log[1+L]+(L/(2^22));

Clear[f];
f[L_]=bound[5]-((Log[Zeta[1+η[L]]])/(2logrc[L]))(-(((Subscript[θ, 1+η])[L])/π)+(((Subscript[θ, 1-c])[L])/π)+(((Subscript[θ, -η])[L])/π)-(1/2))

Plot[f[L],{L,27.02,40},PlotRange->All]

logzetapluslog[0]=0;
logzetapluslog[s_]=Log[Zeta[s]]+Log[s-1];
logzetapluslog[sint_Interval]:=Block[{s},MonotoneEnclosure[logzetapluslog[s],s,sint]];

logoverlog[s_,x_]=((Log[s+x])/(Log[1+x]));
logoverlog[s_,xint_Interval]:=Block[{x},MonotoneEnclosure[logoverlog[s,x],x,xint]];

FullSimplify[f[L]==(L/4194304)+((79045-118430 L-182 (L^2))/(599789+91562 L+512 (L^2)))-(((-(((Subscript[θ, 1+η])[L])/π)+(((Subscript[θ, 1-c])[L])/π)+(((Subscript[θ, -η])[L])/π)-(1/2)) )/(2 logrc[L]))(logzetapluslog[1+η[L]])+((((-(((Subscript[θ, 1+η])[L])/π)+(((Subscript[θ, 1-c])[L])/π)+(((Subscript[θ, -η])[L])/π)-(1/2)) )/(2 logrc[L]))((Log[η[L]])/(Log[1+L]))+(529/1024))Log[1+L],Assumptions->L≥27+1/50]
FullSimplify[((Log[(18/(10+9 L))])/(Log[1+L]))==((-Log[1/2])/(Log[1+L]))-logoverlog[(10/9),L],Assumptions->L≥27+1/50]

Reduce[D[(L/4194304)+((79045-118430 L-182 (L^2))/(599789+91562 L+512 (L^2))),L]≤0&&L≥Lmin,L,Reals]

f[Lint_Interval]:=Module[{L,firstterms,coeff},
firstterms=
PiecewiseMonotoneEnclosure[(L/4194304)+((79045-118430 L-182 (L^2))/(599789+91562 L+512 (L^2))),L,{(NumericalApproximation[Root, (RowDefault["45.7", FEExpressionsNumericalApproximationElider]), Root[-328290035468781719-1255099708427068 #1+184440413178084 ((#1)^2)+93759488 ((#1)^3)+262144 ((#1)^4)&,2], ])},Lint];
coeff=(((-(((Subscript[θ, 1+η])[Lint])/π)+(((Subscript[θ, 1-c])[Lint])/π)+(((Subscript[θ, -η])[Lint])/π)-(1/2)) )/(2 logrc[Lint]));
firstterms-coeff(logzetapluslog[1+η[Lint]])+(coeff(((-Log[1/2])/(Log[1+Lint]))-logoverlog[(10/9),Lint])+(529/1024))Log[1+Lint]];

Plot[f[L],{L,27.02,27.04}]
f[Interval[{27+1/50,27+2/50}]]//N

N[f[Interval[{(2^22),∞}]],30]

Timing[{fails,undec,proven}=ProveNonNegative[f,f,{Linterval},MaxDepth->25];]
{fails,undec,Length[proven]}

Bound 6: (Subscript[κ, 2])=(π/(4(Subscript[J, 1])))(Log[Zeta[c+r]]+2Sum[Log[Zeta[c+r Cos[((π j)/(2(Subscript[J, 1])))]]],{j,1,(Subscript[J, 1])-1}])
	(((Subscript[κ, 2])/π)/(Log[r/(c-1/2)]))≤(635/1024)-((9 (25384532+113745 L))/(64 (7149852+150141 L+512 (L^2))))

bound[6]=(635/1024)-((9 (25384532+113745 L))/(64 (7149852+150141 L+512 (L^2))));

Clear[f];
f[L_]=bound[6]-Block[{J1=64},((1/π)/(logrc[L]))(π/(4J1))(Log[Zeta[c[L]+r[L]]]+2Sum[Log[Zeta[c[L]+r[L] Cos[((π j)/(2J1))]]],{j,1,J1-1}])];

Reduce[D[bound[6],L]≥0&&L≥27]

f[Lint_Interval]:=Module[{L,rat,J1=64},
rat=MonotoneEnclosure[(635/1024)-((9 (25384532+113745 L))/(64 (7149852+150141 L+512 (L^2)))),L,Lint];
rat-((1/π)/(logrc[Lint]))(π/(4J1))(Log[Zeta[c[Lint]+r[Lint]]]+2Sum[Log[Zeta[c[Lint]+r[Lint] Cos[((π j)/(2J1))]]],{j,1,J1-1}])];

N[f[Interval[{(2^16),∞}]],30]

N[f[Interval[{27+1/50,28}]],30]

Timing[Length/@ProveNonNegative[f,f,{Linterval},MaxDepth->20]]

Bound 7: (Subscript[κ, 3])=((π-(Subscript[θ, 1-c]))/(2(Subscript[J, 2])))(Log[Zeta[1-c+r]]+2Sum[Log[Zeta[1-c-r Cos[(Subscript[θ, 1-c])+(π-(Subscript[θ, 1-c]))(j/(Subscript[J, 2]))]]], {j, 1, (Subscript[J, 2])-1}])
	(((Subscript[κ, 3])/π)/(Log[r/(c-1/2)]))≤(491/1024)-((33179656+3346893 L)/(512 (208616+21113 L+512 (L^2))))

bound[7]=(491/1024)-((33179656+3346893 L)/(512 (208616+21113 L+512 (L^2))));

Clear[f];
f[L_]=(491/1024)-((33179656+3346893 L)/(512 (208616+21113 L+512 (L^2))))-Block[{J2=24},((1/π)/(logrc[L]))((π-(Subscript[θ, 1-c])[L])/(2J2))(Log[Zeta[1-c[L]+r[L]]]+2Sum[Log[Zeta[1-c[L]-r[L] Cos[(Subscript[θ, 1-c])[L](1-(j/J2))+((π j)/J2)]]], {j, 1, J2-1}])];

Reduce[D[bound[7],L]≥ 0&&L≥27]
Reduce[D[1-c[L]+r[L],L]≤0&&L≥27]

f[Lint_]:=Module[{L,rat,J2,rmcp1,insidezeta},
J2=24;
rat=MonotoneEnclosure[(491/1024)-((33179656+3346893 L)/(512 (208616+21113 L+512 (L^2)))),L,Lint];
rmcp1=Log[Zeta[MonotoneEnclosure[1-c[L]+r[L],L,Lint]]];
insidezeta[j_]:=IntervalIntersection[Interval[{Min[c[Lint]],∞}],1-c[Lint]-r[Lint]* Cos[(Subscript[θ, 1-c])[Lint]*(1-(j/J2))+((π j)/J2)]];
rat-((1/π)/(logrc[Lint]))((π-(Subscript[θ, 1-c])[Lint])/(2J2))(rmcp1+2Sum[Log[Zeta[insidezeta[j]]], {j, 1, J2-1}])];

N[f[Interval[{27+1/50,27+1/50+1/100}]],30]
N[f[Interval[{(2^20),∞}]],30]

Timing[Length/@ProveNonNegative[f,f,{Linterval},MaxDepth->25]]

Bound 8: 	(((Subscript[κ, 7])/π)/(Log[r/(c-1/2)]))≤((18281-1411 L-50 (L^2))/(800695+63962 L+512 (L^2)))

bound[8]=((18281-1411 L-50 (L^2))/(800695+63962 L+512 (L^2)));

The quantity (Subscript[κ, 7]) is defined by

Clear[K7];

K7[c_,r_,η_]=(1/4)Block[{σ=c+r Cos[θ],t=r Sin[θ]},Integrate[(1+η-σ)(2t-4+(7/19)((((1+σ))^2)+(((t-2))^2))),{θ,ArcCos[((1+η-c)/r)],ArcCos[((-η-c)/r)]}]]

Some nontrivial rearranging work, which we did by hand, gives

(Subscript[κ, 7])[c_,r_,η_]:=Block[{α1=(Sqrt[(-1+c+r-η) (1-c+r+η)]),α2=(Sqrt[-(c-r+η) (c+r+η)])},(1/76) (α1(-48+14 c+14 (c^2)+7 (r^2)-7 η-7 c η)+α2(55-7 c-14 (c^2)-7 (r^2)+21 η+21 c η)+5 (((1+2 η))^2)+(41-55 c+7 (c^2)+7 (c^3)+14 c (r^2)+41 η-14 c η-7 (c^2) η-7 (r^2) η) (ArcTan[((-1+c-η)/(α1))]- ArcTan[((c+η)/(α2))]))]

Mathematica is unable to ascertain if the two expressions are equivalent, but they are.

(* Should Simplify to just 0 *)FullSimplify[K7[c,r,η]-(Subscript[κ, 7])[c,r,η],Assumptions->((-1)/2)<c-r<1-c<-η<0<1<1+η<c<c+r]

(* Just as a reality check, compute the difference for 10 random numbers to 100000 digits. Should all be 0. *)
$MaxExtraPrecision=100000;
MinMax[Table[Block[{k=RandomInteger[{28,10000}]},
N[K7[c[k],r[k],η[k]]-(Subscript[κ, 7])[c[k],r[k],η[k]],20]],{10}]]
$MaxExtraPrecision=50;

Now we turn to developing an interval enclosure for (Subscript[κ, 7]).

(* the alphas are monotone decreasing*)
Reduce[L≥27&&D[(-1+c[L]+r[L]-η[L]) (1-c[L]+r[L]+η[L]),L]≤0,L,Reals]
Reduce[L≥27&&D[-(c[L]-r[L]+η[L]) (c[L]+r[L]+η[L]),L]≤0,L,Reals]

(* the alpha coefficients are monotone, one decreasing and one increasing *)
Reduce[L≥27&&D[(-48+14 c[L]+14 ((c[L])^2)+7 ((r[L])^2)-7 η[L]-7 c[L] η[L]),L]≤0,L,Reals]
Reduce[L≥27&&D[(55-7 c[L]-14 ((c[L])^2)-7 ((r[L])^2)+21 η[L]+21 c[L] η[L]),L]≥0,L,Reals]

(*the arctan coefficient is monotone decreasing *)
Reduce[L≥27&&D[(41-55 c[L]+7 ((c[L])^2)+7 ((c[L])^3)+14 c[L] ((r[L])^2)+41 η[L]-14 c[L] η[L]-7 ((c[L])^2) η[L]-7 ((r[L])^2) η[L]),L]≤0,L,Reals]

kappa7[L_]=(Subscript[κ, 7])[c[L],r[L],η[L]];
kappa7[Lint_Interval]:=Module[{a1c,a2c,arctanc,L,α1,α2},
α1=Sqrt[MonotoneEnclosure[(-1+c[L]+r[L]-η[L]) (1-c[L]+r[L]+η[L]),L,Lint]];
α2=Sqrt[MonotoneEnclosure[-(c[L]-r[L]+η[L]) (c[L]+r[L]+η[L]),L,Lint]];
a1c=MonotoneEnclosure[(-48+14 c[L]+14 ((c[L])^2)+7 ((r[L])^2)-7 η[L]-7 c[L] η[L]),L,Lint];
a2c=MonotoneEnclosure[(55-7 c[L]-14 ((c[L])^2)-7 ((r[L])^2)+21 η[L]+21 c[L] η[L]),L,Lint];
arctanc=MonotoneEnclosure[(41-55 c[L]+7 ((c[L])^2)+7 ((c[L])^3)+14 c[L] ((r[L])^2)+41 η[L]-14 c[L] η[L]-7 ((c[L])^2) η[L]-7 ((r[L])^2) η[L]),L,Lint];

(1/76) (α1*a1c+α2*a2c+5 (((1+2 η[Lint]))^2)+arctanc (ArcTan[((-1+c[Lint]-η[Lint])/(α1))]- ArcTan[((c[Lint]+η[Lint])/(α2))]))]

Plot[kappa7[L],{L,27.02,28}]
N[kappa7[Interval[{27+1/50,28}]],20]

Reduce[L≥27&&D[bound[8],L]≤0,L,Reals]

Clear[f];
f[L_]=bound[8]-((kappa7[L]/π)/(logrc[L]));
f[Lint_Interval]:=Module[{L},MonotoneEnclosure[((18281-1411 L-50 (L^2))/(800695+63962 L+512 (L^2))),L,Lint]-((kappa7[Lint]/π)/(logrc[Lint]))];

N[f[Interval[{(2^15),∞}]],30]

Timing[Length/@ProveNonNegative[f,f,{Linterval},MaxDepth->20]]

Bound 9: 	(((Subscript[κ, 8])/π)/(Log[r/(c-1/2)]))≤((-961048-15293 L-42 (L^2))/(3255348+113665 L+512 (L^2)))

bound[9]=((-961048-15293 L-42 (L^2))/(3255348+113665 L+512 (L^2)));

For the current values of c,r, we have (Subscript[θ, -1/2])=π. The quantity (Subscript[κ, 8]) is defined by

K8=(1/4)Block[{σ=c+r Cos[θ],t=r Sin[θ]},Integrate[(1-2σ)(2t-4+(7/19)((((1+σ))^2)+(((t-2))^2))),{θ,ArcCos[((-η-c)/r)],π}]]

Some easy rearranging work gives

(Subscript[κ, 8])[c_,r_,η_]:=Block[{α2=(Sqrt[-(c-r+η) (c+r+η)])},(1/76) ((c^2) (10-21 π)-41 π-14 (c^3) π+10 (r^2)-7 π (r^2)+c (-10+96 π-20 r-28 π (r^2))+10 (r-η (1+η))+2 (-48+7 (r^2)+7 c (2+2 c-η)-7 η) α2+(41+7 (r^2)+c (-96+7 c (3+2 c)+28 (r^2))) ArcCos[-((c+η)/r)])]

Mathematica is able to ascertain if the two expressions are equivalent, and they are.

Reduce[K8==(Subscript[κ, 8])[c,r,η]&&((-1)/2)<c-r<1-c<-η<0<1<1+η<c<c+r]

Now we turn to developing an interval enclosure for (Subscript[κ, 8]).

(* the α2 is monotone decreasing, and so is its coefficient *)
Reduce[L≥27&&D[-(c[L]-r[L]+η[L]) (c[L]+r[L]+η[L]),L]≤0,L,Reals]
Reduce[L≥27&&D[2 (-48+7 ((r[L])^2)+7 c[L] (2+2 c[L]-η[L])-7 η[L]),L]≤0,L,Reals]

(* the big terms are monotone increasing*)
Reduce[L≥27&&D[((c[L])^2) (10-21 π)-41 π-14 ((c[L])^3) π+10 ((r[L])^2)-7 π ((r[L])^2)+c[L] (-10+96 π-20 r[L]-28 π ((r[L])^2))+10 (r[L]-η[L] (1+η[L])),L]≥0,L,Reals]

(*the arccos coefficient is monotone decreasing *)
Reduce[L≥27&&D[(41+7 ((r[L])^2)+c[L] (-96+7 c[L] (3+2 c[L])+28 ((r[L])^2))),L]≤0,L,Reals]
(* the arccos term is monotone *)
Reduce[L≥27&&D[-((c[L]+η[L])/(r[L])),L]≤0,L,Reals]

kappa8[L_]=(Subscript[κ, 8])[c[L],r[L],η[L]];
kappa8[Lint_Interval]:=Module[{a2c,arccosc,arccos,L,bigs,α2},
α2=Sqrt[MonotoneEnclosure[-(c[L]-r[L]+η[L]) (c[L]+r[L]+η[L]),L,Lint]];
a2c=MonotoneEnclosure[2 (-48+7 ((r[L])^2)+7 c[L] (2+2 c[L]-η[L])-7 η[L]),L,Lint];
arccos=ArcCos[MonotoneEnclosure[-((c[L]+η[L])/(r[L])),L,Lint]];
arccosc=MonotoneEnclosure[(41+7 ((r[L])^2)+c[L] (-96+7 c[L] (3+2 c[L])+28 ((r[L])^2))),L,Lint];
bigs=MonotoneEnclosure[((c[L])^2) (10-21 π)-41 π-14 ((c[L])^3) π+10 ((r[L])^2)-7 π ((r[L])^2)+c[L] (-10+96 π-20 r[L]-28 π ((r[L])^2))+10 (r[L]-η[L] (1+η[L])),L,Lint];

(1/76) (bigs+a2c*α2+arccosc*arccos)]

Plot[kappa8[L],{L,270.02,280}]
N[kappa8[Interval[{270+1/50,280}]],20]

Reduce[L≥27&&D[bound[9],L]≥0,L,Reals]

Clear[f];
f[L_]=bound[9]-((kappa8[L]/π)/(logrc[L]));
f[Lint_Interval]:=Module[{L},MonotoneEnclosure[((-961048-15293 L-42 (L^2))/(3255348+113665 L+512 (L^2))),L,Lint]-((kappa8[Lint]/π)/(logrc[Lint]))];

N[f[Interval[{(2^16),∞}]],30]

Timing[Length/@ProveNonNegative[f,f,{Linterval},MaxDepth->20]]

Assembling the final bound

sharp[L_,T_]=Sum[bound[k],{k,1,7}]+(1/(T+2))(bound[8]+bound[9])

First we wrestle with the terms involving T.

Clear[f];
f[L_,T_]=(1/(14 (-(1/5)+T)))+((((18281-1411 L-50 (L^2))/(800695+63962 L+512 (L^2)))+((-961048-15293 L-42 (L^2))/(3255348+113665 L+512 (L^2))))/(2+T));

Reduce[D[((18281-1411 L-50 (L^2))/(800695+63962 L+512 (L^2)))+((-961048-15293 L-42 (L^2))/(3255348+113665 L+512 (L^2))),L]≥0&&L≥27]

That is, f is monotone increasing in L.  It is not monotone in T, but no matter.

f[Lint_Interval,Tint_Interval]:=Module[{Lmin,Lmax,Aint},
Aint=MonotoneEnclosure[((18281-1411 L-50 (L^2))/(800695+63962 L+512 (L^2)))+((-961048-15293 L-42 (L^2))/(3255348+113665 L+512 (L^2))),L,Lint];
((1/14)/(Tint-1/5))+(Aint/(2+Tint))]

f[Linterval,Interval[{5/7,∞}]]

Maximize[{Limit[f[L,T],L->Infinity],T≥5/7},T,Reals]

tobeprovennonneg[L_,T_]:=(75/1024)-f[L,T];

AbsoluteTiming[ProveNonNegative[tobeprovennonneg,tobeprovennonneg,{Linterval,Interval[{5/7,∞}]}]]

sharp2[L_]=(1127/1024)+((953657 L)/4194304)+((80807+17909 L+178 (L^2))/(4 (164296+9637 L+128 (L^2))))-((33179656+3346893 L)/(512 (208616+21113 L+512 (L^2))))+((149201-214796 L-1135 (L^2))/(496726+75117 L+512 (L^2)))+((79045-118430 L-182 (L^2))/(599789+91562 L+512 (L^2)))-((9 (25384532+113745 L))/(64 (7149852+150141 L+512 (L^2))))+((80396+135589 L+798 (L^2))/(16 (38735+3105 L+32 (L^2))))+(75/1024)+(947/512) Log[1+L]

N[((953657 )/4194304),20]

Plot[0.22737L+2Log[1+L]-1/2-sharp2[L],{L,27,(20^3)},PlotRange->All,AxesOrigin->{27.02,0},PlotLegends->"Expressions"]

toprovenonneg[L_]=(22737/100000)L+2Log[1+L]-1/2-sharp2[L]

Notice that all of the denominators are positive L>0. The rational part of toprovenonneg[L] has only one critical value for L≥27+(1/50), near L=20000. We use that knowledge to speed up the interval enclosure below, but don’t need to do so.

Reduce[L≥Lmin&&D[-(857/512)-((80807+17909 L+178 (L^2))/(4 (164296+9637 L+128 (L^2))))+((33179656+3346893 L)/(512 (208616+21113 L+512 (L^2))))-((149201-214796 L-1135 (L^2))/(496726+75117 L+512 (L^2)))-((79045-118430 L-182 (L^2))/(599789+91562 L+512 (L^2)))+((9 (25384532+113745 L))/(64 (7149852+150141 L+512 (L^2))))-((80396+135589 L+798 (L^2))/(16 (38735+3105 L+32 (L^2)))),L]≤0]

toprovenonneg[Lint_Interval]:=Module[{L,expr,exprint},
expr=-(857/512)-((80807+17909 L+178 (L^2))/(4 (164296+9637 L+128 (L^2))))+((33179656+3346893 L)/(512 (208616+21113 L+512 (L^2))))-((149201-214796 L-1135 (L^2))/(496726+75117 L+512 (L^2)))-((79045-118430 L-182 (L^2))/(599789+91562 L+512 (L^2)))+((9 (25384532+113745 L))/(64 (7149852+150141 L+512 (L^2))))-((80396+135589 L+798 (L^2))/(16 (38735+3105 L+32 (L^2))));
exprint=MonotoneEnclosure[expr,L,Lint];
exprint+((5939 Lint)/13107200000)+(77/512) Log[1+Lint]];

N[toprovenonneg[Interval[{(2^12),∞}]],30]

AbsoluteTiming[ProveNonNegative[toprovenonneg,toprovenonneg,{Linterval},MaxDepth->25]]