A first correction with a quadratic large-vertex remainder

Keep the uniform-simplex assumptions, the fixed-degree-limit constant \(C_M\), and the leading term \(B_M\) from The vertex leading constant at large vertex count. The following expansion concerns \(C_M\) as the vertex count grows; it asserts no joint \(M,D\) limit and no finite-sample risk approximation.

Theorem 50 (First correction and an explicit second-order remainder)

Put \(n=M-2\), \(L=\log2\), and

\[\beta=\frac{28L^2-18L+1}{8(2L-1)^2}.\]

For every integer \(M\geq258\),

(97)\[\left|\frac{C_M}{B_M}-1-\frac\beta n\right| \leq\frac{84}{n^2}.\]

The coefficient satisfies \(13/8<\beta<53/32\). Consequently \(84/n^2\) also bounds the relative error against the corrected leading term \(B_M(1+\beta/n)\). The earlier radius \(6/n\) concerns approximation by \(B_M\) alone; the centers are different.

Proof. The correction is derived before numerical evaluation. Use the exact normalization already established in A sharper elementary large-vertex guarantee:

\[C_M/B_M=\sqrt{1+1/n}\,I_n/G_n,\qquad I_n=\int_0^\pi f(x)^nA(x)\,dx,\qquad G_n=\frac{\sqrt\pi}{2\sqrt{\alpha n}},\]

where

\[\begin{split}h(x)&=4\cos^2(x/2)\log(2\cos(x/2))+x\sin x,\\ f(x)&=h(x)/(4L),\quad A(x)=\sec^2(x/2),\quad \alpha=\frac{2L-1}{8L}.\end{split}\]

Define \(a_4=(4L-3)/(192L)\) and \(\lambda=a_4-\alpha^2/2<0\). The first two terms of the positive logarithm series give \(L>2/3+2/81=56/81>29/42\). Together with \(L<7/10\) from the refined chapter, this implies \(2/29<\alpha<1/14\).

Sixth-order control on the fixed local interval. For \(0\leq x\leq1\), write \(c=\cos x\) and \(\ell=\log(2\cos(x/2))\). Twice differentiating the previously proved fourth derivative gives the exact identity

\[h^{(6)}(x)=2c-x\sin x-2c\ell+2\sin x\tan(x/2) -\frac{c}{1+c}-\frac{c}{(1+c)^2} -\frac{2\sin^2x}{(1+c)^3}.\]

Here \(c\geq1/2\), \(0<\ell<7/10\), and \(0\leq\tan(x/2)\leq4/7\). The absolute values of the seven terms sum to at most \(2+1+7/5+8/7+1/2+1/4+16/27<8\). Taylor’s theorem and evenness therefore give

\[|f(x)-1+\alpha x^2-a_4x^4|\leq x^6/240.\]

Retain the signed bounds proved in the refined chapter. With \(u=1-f(x)\) and \(d=7/832\), they are

\[\alpha x^2\leq u\leq x^2/13,\quad |u-\alpha x^2|\leq x^4/192,\quad -dx^4\leq\log f(x)+\alpha x^2\leq0.\]

Since \(u+\alpha x^2\leq(1/13+1/14)x^2\), expansion of \(\log(1-u)\) through its quadratic term yields

\[\begin{split}|\log f(x)+\alpha x^2-\lambda x^4| &\leq\left(\frac1{240}+\frac{27}{69888}+\frac1{6084}\right)x^6\\ &=\frac{64289}{13628160}x^6<\frac{x^6}{200}.\end{split}\]

The last summand bounds \(\sum_{k\geq3}u^k/k\leq u^3/(3(1-u))\). Taking the limit at zero in the signed fourth-order bound also gives \(|\lambda|\leq d\). For the amplitude, put \(t=x/2\). From \(t\leq\tan t\leq8t/7\) one obtains \(0\leq\tan t-t\leq64t^3/147\). Hence

\[0\leq A(x)-1-x^2/4 \leq(20/343)x^4<x^4/16,\qquad A\leq4/3,\quad A-1\leq x^2/3.\]

A Gaussian expansion with a quantified error. Set \(w=\log f+\alpha x^2\leq0\). For \(v\leq0\), \(|e^v-1-v|\leq v^2/2\). The preceding bounds imply

\[\left|f(x)^nA(x) -e^{-\alpha nx^2}(1+x^2/4+n\lambda x^4)\right| \leq e^{-\alpha nx^2}\left( \frac{nx^6}{150}+\frac{2d^2n^2x^8}{3} +\frac{x^4}{16}+\frac{dnx^6}{3}\right).\]

Extend this positive majorant to infinity. Using \(G_n^{-1}\int_0^\infty x^{2k}e^{-\alpha nx^2}dx =(2k-1)!!/(2\alpha n)^k\), its integral divided by \(G_n\) is bounded by \(K_0/n^2\), where

\[K_0=\frac1{80\alpha^3}+\frac{35d^2}{8\alpha^4} +\frac3{64\alpha^2}+\frac{5d}{8\alpha^3} <\frac{34415865391}{443023360}<80.\]

The last rational value substitutes \(\alpha=2/29\).

Both omitted tails are bounded separately. The old monotonicity and exact second moment \(I_2<12\), together with \(f(1)<15/16\) and \(G_n>3/\sqrt n\), give

\[G_n^{-1}\int_1^\pi f(x)^nA(x)dx \leq4\sqrt n e^{-(n-2)/16}\leq1/n^2\quad(n\geq256).\]

Indeed \(n^{5/2}e^{-(n-2)/16}\) decreases for \(n\geq40\), and at 256 the assertion follows from \(22L<77/5<254/16\) and \(4\,256^{5/2}=2^{22}\).

For the Gaussian polynomial put \(a=\alpha n>n/16\). Integration by parts bounds the tails of powers 0, 2 and 4 by \(e^{-a}/(2a)\) times, respectively, \(1\), \(1+1/(2a)\), and \(1+3/(2a)+3/(4a^2)\). Since \(d<1/100\), their sum with weights \(1,1/4,nd\) is bounded, for \(n\geq256\), by

\[1+\tfrac14(1+8/n)+nd(1+24/n+192/n^2) \leq149/100+n/100+98/(25n)<n/32.\]

Consequently the absolute Gaussian-polynomial tail divided by \(G_n\) is at most \(\sqrt n e^{-n/16}/12\leq1/n^2\). The same monotonicity proves the last bound from its value at 256; use \(e^{16}>2^{22}\). Combining both tails with the local integral proves

\[\left|I_n/G_n-1-b/n\right|\leq82/n^2,\qquad b=\frac1{8\alpha}+\frac{3\lambda}{4\alpha^2}.\]

Exact normalization and the first correction. Algebra gives \(\beta=b+1/2\) with the displayed formula. Its derivative as a function of \(L\) is \(-(10L-7)/(4(2L-1)^3)>0\) on \((2/3,7/10)\). Evaluation at the endpoints gives \(13/8<\beta<53/32\), so \(0<b<2\). Taylor’s theorem gives \(|\sqrt{1+1/n}-1-1/(2n)|\leq1/(8n^2)\). Thus, for \(n\geq256\),

\[\left|C_M/B_M-1-\beta/n\right| \leq\frac{83+1/8+(41+1/4)/n}{n^2}<\frac{84}{n^2}.\]

This includes the square-root normalization rather than absorbing it into an unspecified correction. Division by \(1+\beta/n>1\) proves the corrected relative-error assertion.

Certified evaluation and replay

The standard-library module tools.risk_research.vertex_large_dimension_second_order encloses \(\beta\) by exact rational evaluation at the endpoints of the existing logarithm-series enclosure. Monotonicity is used only on the proved interval \(2/3<L<7/10\). For every \(M\geq258\) it encloses \(C_M\) after removing \(M^2(M-1)!(2\log2)^{M-1}\). The uncertainty in the logarithm and leading normalization is separate from the analytic radius \(84/n^2\). For smaller \(M\) the new evaluator rejects the request; the earlier tool supplies its existing valid fallback.

For positive rational \(\varepsilon\), the threshold routine returns

\[\max\left(258,\ 2+\left\lceil\sqrt{84/\varepsilon}\right\rceil\right).\]

It guarantees the error relative to the exact corrected leading term at every larger integer vertex count. One percent is therefore guaranteed throughout the new theorem’s domain. Independently, \(|C_M/B_M-1|\leq53/(32n)+84/n^2<1/100\) already at \(n=256\), and the right side decreases thereafter; the uncorrected leading term also has a one-percent sufficient start of \(M=258\). These are sufficient starts, not minimal classifications.

$ .venv/bin/python -m tools.risk_research.vertex_large_dimension_second_order --vertices 258 --bits 47 --relative-target 1/1000 --output .research/skeleton-risk/second-order258.json
$ .venv/bin/python -m tools.risk_research.vertex_large_dimension_second_order --verify .research/skeleton-risk/second-order258.json

The new record schema stores the vertex count as a canonical decimal string, while precision and backend flags retain strict integer and boolean types. Rational fields use canonical decimal numerator and denominator strings, with local chunked conversion for very large integers. No old schema is changed. Verification accepts no generation overrides, restores recorded precision/target/optional flags, and rejects duplicate keys, extra fields, type changes, source edits and altered bounds. CRLF-to-LF fingerprints and raw source guards follow the existing tools.

Output is written atomically in a caller-controlled local directory. Generation rejects source/proof aliases before calculation and again at the canonical parent plus original leaf name before writing. An unrelated leaf symlink is replaced without changing its target. There is no sandbox guarantee against a separate process renaming or replacing that canonical directory itself.

Optional Arb restores the factorial/exponential scale. The optional --integral-check calls the original positive integral without using the new expansion, restores working precision, and rounds saved balls outward. Finite integral holdouts and rational-series normalization checks are implementation evidence; the proof above supplies the infinite tail. No fitted coefficient, production sampling API, mandatory dependency, third correction, or growing-degree limit is introduced.