feat(p28): harden exact proof equations
This commit is contained in:
Codex
parent
437b439c6c
commit
492c8ab871
18 changed files with 3123 additions and 394 deletions
|
|
@ -1,73 +1,99 @@
|
||||||
# Problem 2.8 — Exact Hypergeometric Tail Closure
|
# Problem 2.8 — Exact Hypergeometric Tail Closure
|
||||||
|
|
||||||
**Status:** PROVED
|
**Status:** exact proof, adversarially audited
|
||||||
**Date:** July 2026
|
**Date:** July 2026
|
||||||
|
|
||||||
For every official column \(j=1,2,3,4\), the authoritative recurrence
|
For every official column \(j=1,2,3,4\), the authoritative recurrence
|
||||||
satisfies
|
satisfies the official orientation
|
||||||
|
|
||||||
\[
|
|
||||||
\lim_{N\to\infty}\frac{P_{N,j}}{Q_{N,j}}
|
|
||||||
=\frac{\sqrt{10005}}{\pi}.
|
|
||||||
\]
|
|
||||||
|
|
||||||
Equivalently, in the orientation requested by Ramanujan Challenge
|
|
||||||
Problem 2.8,
|
|
||||||
|
|
||||||
\[
|
\[
|
||||||
\boxed{\displaystyle
|
\boxed{\displaystyle
|
||||||
|
\lim_{N\to\infty}\frac{P_{N,j}}{Q_{N,j}}
|
||||||
|
=\frac{\sqrt{10005}}{\pi}}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Its reciprocal consequence is
|
||||||
|
|
||||||
|
\[
|
||||||
\lim_{N\to\infty}\frac{Q_{N,j}}{P_{N,j}}
|
\lim_{N\to\infty}\frac{Q_{N,j}}{P_{N,j}}
|
||||||
=\frac{\pi}{\sqrt{10005}}}.
|
=\frac{\pi}{\sqrt{10005}}.
|
||||||
\]
|
\]
|
||||||
|
|
||||||
## Exact closure
|
## Exact closure
|
||||||
|
|
||||||
The proof closes the former connection-functional gap through:
|
The proof closes the former connection-functional gap through:
|
||||||
|
|
||||||
1. an exact nonterminating \({}_4F_3\) tail with
|
1. the fully displayed rational deformation
|
||||||
|
\(M_N(x)=\mathcal M(2N+3,x)\);
|
||||||
|
2. a nonterminating \({}_4F_3\) tail with
|
||||||
\(M_Nk_{N+1}=k_N\);
|
\(M_Nk_{N+1}=k_N\);
|
||||||
2. a rank-one discrete-valuation argument giving the all-\(N\)
|
3. four denominator-cleared Ore factorizations, with no division or
|
||||||
|
remainder command;
|
||||||
|
4. a rank-one discrete-valuation induction giving the all-\(N\)
|
||||||
Padé divisibility pattern;
|
Padé divisibility pattern;
|
||||||
3. an exact terminating adjoint \({}_4F_3\) formula for the denominator;
|
5. an exact terminating adjoint \({}_4F_3\), proved by a matrix-induced
|
||||||
4. positivity at \(z_0=-1/53360^3\) and a fixed-point Cauchy bound with
|
scalar step and base/generic/top coefficient induction;
|
||||||
|
6. positivity at \(z_0=-1/53360^3\) and a Cauchy bound with
|
||||||
\[
|
\[
|
||||||
\beta=
|
\beta=
|
||||||
\frac{3125}{1307443596565949700399927}
|
\frac{3125}{1307443596565949700399927}
|
||||||
<4\cdot10^{-19};
|
<4\cdot10^{-19};
|
||||||
\]
|
\]
|
||||||
5. the Chudnovsky CM value
|
7. the Chudnovsky CM value
|
||||||
\(\Phi(x_0)=\sqrt{10005}/\pi\);
|
\(\Phi(x_0)=\sqrt{10005}/\pi\);
|
||||||
6. an exact Rouché separation of the characteristic quartic, a positive
|
8. an explicit stable-graph contraction constructing the dominant
|
||||||
denominator lower bound, and the cyclic-frame argument transferring the
|
functional and proving eventual nonvanishing in all four columns.
|
||||||
first-column result to all four columns.
|
|
||||||
|
|
||||||
The proof is structural and does not infer equality from the earlier
|
The proof is structural and does not infer equality from the earlier
|
||||||
\(10^{-1052}\) numerical enclosure.
|
\(10^{-1052}\) numerical enclosure.
|
||||||
|
|
||||||
|
## Equation-only audit repairs
|
||||||
|
|
||||||
|
The repaired release removes:
|
||||||
|
|
||||||
|
- Ore `quo_rem` calls from the proof path;
|
||||||
|
- ODE-normalization uniqueness;
|
||||||
|
- Birkhoff–Poincaré delegation;
|
||||||
|
- irreducibility and polynomial-GCD decisions;
|
||||||
|
- a false negative-exponent norm inequality;
|
||||||
|
- implicit maximum-principle and denominator-nonvanishing hypotheses;
|
||||||
|
- reliance on stored PASS transcripts.
|
||||||
|
|
||||||
|
The mandatory standard-library checkers verify the full differential gauge,
|
||||||
|
base horizontal row, matrix-to-scalar bridge, terminating induction,
|
||||||
|
balanced limit, characteristic polynomial, root-separation inequalities, and
|
||||||
|
positive exterior-root eigenvector coordinates.
|
||||||
|
|
||||||
|
## Trust boundary
|
||||||
|
|
||||||
|
The classical Chudnovsky formula is the sole imported problem-specific
|
||||||
|
theorem and is cited precisely to a complete modular/CM derivation. Standard
|
||||||
|
foundational complex- and linear-analysis results are used with their
|
||||||
|
hypotheses displayed. The package therefore claims a self-contained
|
||||||
|
recurrence proof relative to that explicit theorem—not an axiom-free
|
||||||
|
reconstruction of all of complex analysis or CM theory.
|
||||||
|
|
||||||
## Authoritative artifacts
|
## Authoritative artifacts
|
||||||
|
|
||||||
- `docs/proofs/PROBLEM_28_PROOF.tex`
|
- `docs/proofs/PROBLEM_28_PROOF.tex`
|
||||||
- `docs/proofs/PROBLEM_28_PROOF.pdf`
|
- `docs/proofs/PROBLEM_28_PROOF.pdf`
|
||||||
- `experiments/ramanujan_28/submission/`
|
- `experiments/ramanujan_28/submission/solution.tex`
|
||||||
|
- `experiments/ramanujan_28/submission/solution.pdf`
|
||||||
|
- `experiments/ramanujan_28/submission/ADVERSARIAL_AUDIT.md`
|
||||||
|
- `experiments/ramanujan_28/submission/certificates/STANDALONE_EQUATION_CERTIFICATES.md`
|
||||||
- `experiments/ramanujan_28/submission/ramanujan_challenge_problem_2_8.zip`
|
- `experiments/ramanujan_28/submission/ramanujan_challenge_problem_2_8.zip`
|
||||||
|
|
||||||
The primary Wolfram Language certificate contains 22 exact symbolic checks
|
|
||||||
plus a consolidated PASS conclusion. Dependency-free Python checks verify
|
|
||||||
the rank-one algebra, the Rouché inequality, and the convergence constants.
|
|
||||||
Independent SageMath certificates provide secondary exact cross-checks.
|
|
||||||
|
|
||||||
## Release verification
|
## Release verification
|
||||||
|
|
||||||
- Independent adversarial proof audit: **PASS**
|
- Mandatory dependency-free equations: **PASS**
|
||||||
- Wolfram exact checks: **22/22 PASS**
|
- Fresh optional Wolfram cross-check: **22/22 PASS**
|
||||||
- Python exact checks: **PASS**
|
- Independent Ore/special-function audit: **PASS**
|
||||||
- LaTeX build: **PASS**, zero warnings
|
- Independent convergence/all-column audit: **PASS**
|
||||||
- PDF visual inspection: **PASS**, all 10 pages
|
- Independent logic/vacuity audit: **PASS**
|
||||||
- Clean ZIP extraction and PDF rebuild: **PASS**
|
- LaTeX build and warning scan: **PASS**
|
||||||
|
- PDF page-by-page inspection: **PASS**
|
||||||
|
- Clean ZIP extraction, checks, and PDF rebuild: **PASS**
|
||||||
|
- Clean Git-bundle clone and checks: **PASS**
|
||||||
|
|
||||||
SHA-256:
|
Final SHA-256 values are recorded in `Sha256.txt` beside the released
|
||||||
|
artifacts.
|
||||||
```text
|
|
||||||
PDF a70c50287b24d13bdb113bcdbf87011dcbd698fdd4a7566ede5a8b37aeb8c2b9
|
|
||||||
ZIP 60b9d60808af129a339064e72b2ad5bd8ff9bc933c3905cf8faf821316cab91d
|
|
||||||
```
|
|
||||||
|
|
|
||||||
Binary file not shown.
|
|
@ -58,15 +58,17 @@ Equivalently, \(Q_{N,j}/P_{N,j}\to\pi/\sqrt{10005}\).
|
||||||
|
|
||||||
The missing connection constant is fixed by an exact rank-three
|
The missing connection constant is fixed by an exact rank-three
|
||||||
hypergeometric tail. A nonterminating \(\F43\) Euler jet is carried
|
hypergeometric tail. A nonterminating \(\F43\) Euler jet is carried
|
||||||
backward by the authoritative matrix, while the first denominator is a
|
backward by the displayed matrix, while the first denominator is a
|
||||||
terminating adjoint \(\F43\). Their common differential gauge gives an
|
terminating adjoint \(\F43\). Four denominator-cleared Ore identities
|
||||||
all-\(N\) Pad\'e divisibility theorem. Positivity of the terminating
|
and three coefficient identities give an all-\(N\) Pad\'e divisibility
|
||||||
denominator at the negative CM point, together with a balanced-transfer
|
theorem. Positivity at the negative CM point, a Cauchy estimate, and an
|
||||||
Cauchy estimate, turns that formal divisibility into a direct fixed-point
|
explicit stable-graph contraction prove convergence for all four columns.
|
||||||
convergence proof. The symbolic contiguity and adjoint identities are
|
Every algebraic identity used below is reproduced by a dependency-free
|
||||||
included as reproducible Wolfram Language and SageMath certificates.
|
rational-polynomial checker. The classical Chudnovsky formula, cited
|
||||||
|
precisely in Section~2, is the sole imported theorem.
|
||||||
\end{abstract}
|
\end{abstract}
|
||||||
|
|
||||||
|
\enlargethispage{2\baselineskip}
|
||||||
\tableofcontents
|
\tableofcontents
|
||||||
|
|
||||||
\section{Statement and compact form of the seeds}
|
\section{Statement and compact form of the seeds}
|
||||||
|
|
@ -85,16 +87,49 @@ Let
|
||||||
\[
|
\[
|
||||||
G_N=M_0M_1\cdots M_{N-1},\qquad G_0=I_4,
|
G_N=M_0M_1\cdots M_{N-1},\qquad G_0=I_4,
|
||||||
\]
|
\]
|
||||||
where \(M_N=M(N,x)\) is the authoritative transfer matrix in the analytic
|
where the rational family is defined as follows. Put \(r=x^{-1}\),
|
||||||
deformation
|
\(\omega=u(3u-2)(3u+2)\), and
|
||||||
|
\begin{align*}
|
||||||
|
a_1={}&r(144u^5-288u^4+144u^3)
|
||||||
|
-99u^5+333u^4-229u^3-114u^2+40u+64,\\
|
||||||
|
a_2={}&r(432u^4-864u^3+432u^2)
|
||||||
|
-243u^4+909u^3-868u^2-80u+272,\\
|
||||||
|
a_3={}&r(432u^3-864u^2+432u)
|
||||||
|
-153u^3+648u^2-860u+360,\\
|
||||||
|
a_4={}&144r(u-1)^2,\\
|
||||||
|
b_1={}&-144ru^3+9u^4+63u^3+158u^2+168u+64,\\
|
||||||
|
b_2={}&216ru^2+36u^3-189u^2-316u-168,\\
|
||||||
|
b_3={}&108ru+54u^2-189u-158,\\
|
||||||
|
c_1={}&-288r^2u^3+
|
||||||
|
r(54u^4+378u^3+948u^2+1008u+384)\\
|
||||||
|
&\hspace{2.2em}+18u^5+45u^4-251u^3-1086u^2-1384u-576,\\
|
||||||
|
c_2={}&-432r^2u^2+
|
||||||
|
r(153u^4-657u^3+1292u^2+2064u+1072)\\
|
||||||
|
&\hspace{2.2em}-72u^4+702u^3-1069u^2-2508u-1512,\\
|
||||||
|
c_3={}&-216r^2u+
|
||||||
|
r(180u^3-891u^2+1450u+1116)\\
|
||||||
|
&\hspace{2.2em}-108u^3+864u^2-1385u-1422,\\
|
||||||
|
c_4={}&-4r^2+r(6u^2-33u+\tfrac{536}{9})
|
||||||
|
-4u^2+32u-63.
|
||||||
|
\end{align*}
|
||||||
|
Define
|
||||||
|
\begin{equation}\label{eq:deformed-matrix}
|
||||||
|
\mathcal M(u,x)=
|
||||||
|
\begin{pmatrix}
|
||||||
|
a_1/\omega&a_2/\omega&a_3/\omega&a_4/\omega\\
|
||||||
|
-u^3&-3u^2&-3u&-1\\
|
||||||
|
xb_1/144&-xb_2/72&-xb_3/36&
|
||||||
|
x(-2r-(2u-7))/2\\
|
||||||
|
x^2c_1/288&x^2c_2/144&x^2c_3/72&x^2c_4/4
|
||||||
|
\end{pmatrix},
|
||||||
|
\qquad M_N(x)=\mathcal M(2N+3,x).
|
||||||
|
\end{equation}
|
||||||
|
At \(x=x_0\), the only deformed challenge coefficient is restored by
|
||||||
\[
|
\[
|
||||||
236337691420383\ \longmapsto\ \frac{14/x-567}{9}.
|
236337691420383=\frac{14R-567}{9}.
|
||||||
\]
|
\]
|
||||||
At \(x=x_0\), this is the exact identity
|
Thus every use of Cauchy's theorem below concerns the explicitly displayed
|
||||||
\(236337691420383=(14R-567)/9\). Thus every later use of Cauchy's theorem
|
rational \(x\)-family, not an unspecified continuation.
|
||||||
concerns this explicitly defined rational \(x\)-family.
|
|
||||||
The complete entries of \(M(N,x)\) appear verbatim in the accompanying
|
|
||||||
CAS certificates.
|
|
||||||
|
|
||||||
Define four Pascal rows
|
Define four Pascal rows
|
||||||
\[
|
\[
|
||||||
|
|
@ -131,7 +166,19 @@ The two official initial rows have the exact form
|
||||||
H_0=Ab_0+Bb_1=(A+B,B,0,0).
|
H_0=Ab_0+Bb_1=(A+B,B,0,0).
|
||||||
\end{equation}
|
\end{equation}
|
||||||
At \(x=x_0\), these identities reproduce the official integer rows
|
At \(x=x_0\), these identities reproduce the official integer rows
|
||||||
entry by entry.
|
entry by entry:
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
A_0={}&(37169305760442252761441,\,
|
||||||
|
111507917281327441564208,\\
|
||||||
|
&\hspace{4.7em}111507917281327599720129,\,
|
||||||
|
37169305760442410917362),\\
|
||||||
|
A_1={}&(1167416361542639692320,\,
|
||||||
|
3502249084627896132160,\\
|
||||||
|
&\hspace{4.7em}3502249084627879697280,\,
|
||||||
|
1167416361542622723840).
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
For \(j=1,\ldots,4\), write
|
For \(j=1,\ldots,4\), write
|
||||||
\[
|
\[
|
||||||
|
|
@ -156,7 +203,10 @@ and define
|
||||||
\Phi(x)=\frac{Ay(z)+B\theta y(z)}{S}.
|
\Phi(x)=\frac{Ay(z)+B\theta y(z)}{S}.
|
||||||
\end{equation}
|
\end{equation}
|
||||||
|
|
||||||
The classical Chudnovsky identity is
|
We use one external theorem: the classical Chudnovsky identity. In the
|
||||||
|
normalization used here it is Theorem~0.1 of Milla's equation-by-equation
|
||||||
|
derivation \([2]\), whose modular and CM proof is completed in
|
||||||
|
Theorem~9.7 and Chapter~10:
|
||||||
\[
|
\[
|
||||||
\frac1\pi=
|
\frac1\pi=
|
||||||
\frac{12}{640320^{3/2}}
|
\frac{12}{640320^{3/2}}
|
||||||
|
|
@ -212,24 +262,89 @@ Its Euler jet is
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
The first row is verified coefficientwise from the ratio of consecutive
|
Put \(m=(u-1)/2=N+1\). For the \(r\)-th row of
|
||||||
\(\F43\) coefficients. For the other rows, let \(t=\delta_{N+1}\).
|
\(\mathcal M(u,x)\), define
|
||||||
|
\[
|
||||||
|
P_r(t)=\sum_{s=0}^3\mathcal M(u,x)_{r+1,s+1}t^s,\qquad
|
||||||
|
\mathcal TQ=(1-x)x\partial_xQ+(t+1)Q.
|
||||||
|
\]
|
||||||
The shifted tail satisfies
|
The shifted tail satisfies
|
||||||
\[
|
\[
|
||||||
\left[
|
L_+(t)F_{N+1}=0,
|
||||||
(1-x)t(t+u)^3+
|
|
||||||
x(t+n+1)(t+n+\tfrac76)(t+n+\tfrac32)(t+n+\tfrac{11}{6})
|
|
||||||
\right]F_{N+1}=0,
|
|
||||||
\]
|
\]
|
||||||
where \(u=2N+3\). Each of the remaining three row differences is divided
|
where
|
||||||
by this degree-four Ore polynomial; its remainder is identically zero in
|
\[
|
||||||
\(\Q(N,x)[t]\). The exact coefficient identity, the three Ore divisions,
|
L_+(t)=(1-x)t(t+u)^3+
|
||||||
and the normalization ratio are checked in
|
x(t+m+1)(t+m+\tfrac76)(t+m+\tfrac32)(t+m+\tfrac{11}{6}).
|
||||||
\texttt{p28\_full\_closure\_certificate.wl} and
|
\]
|
||||||
\texttt{p28\_kernel\_contiguity\_certificate.sage}.
|
There is no division step: direct expansion gives the following four
|
||||||
|
denominator-cleared polynomial identities:
|
||||||
|
\begin{align}
|
||||||
|
u(3u-2)(3u+2)x(\mathcal TP_0-P_1)
|
||||||
|
& =144(u-1)^2L_+,\label{eq:ore0}\\
|
||||||
|
\mathcal TP_1-P_2&=-L_+,\label{eq:ore1}\\
|
||||||
|
2(\mathcal TP_2-P_3)&=(-2+7x-2ux)L_+,\label{eq:ore2}\\
|
||||||
|
36(\mathcal TP_3+\ell_3P_3+\ell_2P_2+\ell_1P_1+\ell_0P_0)
|
||||||
|
&=q_3L_+,\label{eq:ore3}
|
||||||
|
\end{align}
|
||||||
|
with
|
||||||
|
\begin{align*}
|
||||||
|
\ell_0={}&(u-1)u(3u-2)(3u+2)x/144,\\
|
||||||
|
\ell_1={}&[-576+864u-432u^2+72u^3
|
||||||
|
+(580-872u+405u^2-36u^3)x]/72,\\
|
||||||
|
\ell_2={}&[432-432u+108u^2
|
||||||
|
+(-436+405u-54u^2)x]/36,\\
|
||||||
|
\ell_3={}&(-12+6u+11x-2ux)/2,\\
|
||||||
|
q_3={}&-36+(536-297u+54u^2)x
|
||||||
|
+(-567+288u-36u^2)x^2.
|
||||||
|
\end{align*}
|
||||||
|
|
||||||
|
For clarity, the coefficient calculation producing the first row is also
|
||||||
|
written without a special-function routine. Set
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
A(t)&=\frac{144(u-1)^2(t+u)^3}{u(3u-2)(3u+2)},&
|
||||||
|
B(t)&=P_0(t)-\frac{A(t)}x,\\
|
||||||
|
\varrho&=-\frac{(3u-2)(3u+2)}{144(u-1)^2u^2},\\
|
||||||
|
\chi_j&=
|
||||||
|
\frac{(m+j)(m+\frac16+j)(m+\frac12+j)(m+\frac56+j)}
|
||||||
|
{m(m+\frac16)(m+\frac12)(m+\frac56)}\\
|
||||||
|
&\quad{}\times
|
||||||
|
\left(\frac{2m(2m+1)}{(2m+j)(2m+j+1)}\right)^3,\\
|
||||||
|
\psi_j&=
|
||||||
|
\frac{(m+j)(m+\frac16+j)(m+\frac12+j)(m+\frac56+j)}
|
||||||
|
{(2m+j)^3(j+1)} .
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
The constant and generic coefficient equations are
|
||||||
|
\begin{equation}\label{eq:tail-coefficients}
|
||||||
|
\varrho[-A(0)]=1,\qquad
|
||||||
|
\varrho\left[-A(j)\chi_j+
|
||||||
|
\frac{(A(j-1)+B(j-1))\chi_{j-1}}{\psi_{j-1}}\right]=1
|
||||||
|
\quad(j\ge1).
|
||||||
|
\end{equation}
|
||||||
|
Clearing the displayed nonzero factors turns
|
||||||
|
\eqref{eq:ore0}--\eqref{eq:tail-coefficients} into polynomial
|
||||||
|
equalities with every coefficient zero. The independent script
|
||||||
|
\texttt{p28\_standalone\_equations.py} expands precisely these equalities
|
||||||
|
using only rational addition and multiplication. Equation
|
||||||
|
\eqref{eq:tail-coefficients} gives the first row of
|
||||||
|
\eqref{eq:tail-contiguity}; applying
|
||||||
|
\eqref{eq:ore0}--\eqref{eq:ore3} successively gives the other three
|
||||||
|
Euler-jet rows.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
For \(N=0\), the standard ascension identity gives
|
For \(N=0\), write \(y(z)=1+\sum_{k\ge1}c_kz^k\). The coefficient of
|
||||||
|
\(z\) is
|
||||||
|
\[
|
||||||
|
c_1=\frac{(1/6)(1/2)(5/6)}{1^3}=\frac5{72},
|
||||||
|
\]
|
||||||
|
and, after shifting \(k\mapsto k+1\), both sides below have initial
|
||||||
|
coefficient \(5/72\) and consecutive-coefficient ratio
|
||||||
|
\[
|
||||||
|
\frac{(k+\frac16)(k+\frac12)(k+\frac56)}{(k+1)^3}.
|
||||||
|
\]
|
||||||
|
Hence coefficient equality, rather than a named ascension rule, gives
|
||||||
\begin{equation}\label{eq:ascension}
|
\begin{equation}\label{eq:ascension}
|
||||||
F_0=y-1
|
F_0=y-1
|
||||||
=\frac5{72}z
|
=\frac5{72}z
|
||||||
|
|
@ -255,6 +370,14 @@ The transformed hypergeometric equation is
|
||||||
\begin{equation}\label{eq:transformed-ode}
|
\begin{equation}\label{eq:transformed-ode}
|
||||||
72\theta^3y+108x\theta^2y+46x\theta y+5xy=0.
|
72\theta^3y+108x\theta^2y+46x\theta y+5xy=0.
|
||||||
\end{equation}
|
\end{equation}
|
||||||
|
Indeed the coefficient ratio of \(y\) gives
|
||||||
|
\[
|
||||||
|
\left[\theta^3-
|
||||||
|
z(\theta+\tfrac16)(\theta+\tfrac12)(\theta+\tfrac56)\right]y=0.
|
||||||
|
\]
|
||||||
|
Substituting \(z=-x/(1-x)\), using
|
||||||
|
\(\theta=(1-x)x\partial_x\), and multiplying by \(72(1-x)\)
|
||||||
|
expands to \eqref{eq:transformed-ode}.
|
||||||
Using the displayed decomposition of \(C\), equations
|
Using the displayed decomposition of \(C\), equations
|
||||||
\eqref{eq:ascension}--\eqref{eq:transformed-ode} give
|
\eqref{eq:ascension}--\eqref{eq:transformed-ode} give
|
||||||
\[
|
\[
|
||||||
|
|
@ -309,6 +432,21 @@ Since \(z=-x+O(x^2)\),
|
||||||
\end{equation}
|
\end{equation}
|
||||||
The leading vector in \eqref{eq:tail-direction} is precisely the image
|
The leading vector in \eqref{eq:tail-direction} is precisely the image
|
||||||
direction in \eqref{eq:rank-one}.
|
direction in \eqref{eq:rank-one}.
|
||||||
|
The other expansion required below is equally direct. Since
|
||||||
|
\[
|
||||||
|
F_{N+1}=\kappa_{N+1}z^{N+2}(1+O(z)),\qquad
|
||||||
|
\delta_{N+1}=\theta-(N+2),
|
||||||
|
\]
|
||||||
|
the shifted derivatives kill the leading monomial, and therefore
|
||||||
|
\begin{equation}\label{eq:next-tail-direction}
|
||||||
|
k_{N+1}=x^{N+2}\widetilde\eta_N
|
||||||
|
\left(\e_1+xs_N+O(x^2)\right),
|
||||||
|
\qquad\widetilde\eta_N\ne0.
|
||||||
|
\end{equation}
|
||||||
|
Moreover, \eqref{eq:rank-one} gives
|
||||||
|
\[
|
||||||
|
J_N(0)\e_1=u^3(a_N,-1,-1,-1)^T\ne0.
|
||||||
|
\]
|
||||||
|
|
||||||
\begin{lemma}[DVR step, including the extra first-column zero]
|
\begin{lemma}[DVR step, including the extra first-column zero]
|
||||||
\label{lem:dvr}
|
\label{lem:dvr}
|
||||||
|
|
@ -378,7 +516,8 @@ Consequently the constant term in the first column of \(fC\) is
|
||||||
|
|
||||||
Apply Lemma~\ref{lem:dvr} inductively, using
|
Apply Lemma~\ref{lem:dvr} inductively, using
|
||||||
\eqref{eq:annihilation}, \eqref{eq:rank-one},
|
\eqref{eq:annihilation}, \eqref{eq:rank-one},
|
||||||
\eqref{eq:tail-direction}, and \(M_Nk_{N+1}=k_N\).
|
\eqref{eq:tail-direction}, \eqref{eq:next-tail-direction}, the displayed
|
||||||
|
nonzero first column of \(J_N(0)\), and \(M_Nk_{N+1}=k_N\).
|
||||||
The stronger last-row assertion follows from
|
The stronger last-row assertion follows from
|
||||||
\eqref{eq:row-relation}.
|
\eqref{eq:row-relation}.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
@ -421,39 +560,154 @@ can vanish.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
The proof is an exact differential-gauge calculation in
|
Write \(p_n=\widehat Q_{n-1}\) for \(n\ge1\). We use coefficient
|
||||||
\(\Q(n,z)\). The nonterminating tail
|
induction, because normalization at \(z=0\) alone
|
||||||
|
would not select a unique solution of the fourth-order equation. To expose
|
||||||
|
the matrix-to-scalar bridge, write
|
||||||
\[
|
\[
|
||||||
\F43\left(
|
\mathcal L_n(t)=t(t+2n-1)^3
|
||||||
\begin{matrix}n,n+\frac16,n+\frac12,n+\frac56\\
|
-z(t+n)(t+n+\tfrac16)(t+n+\tfrac12)(t+n+\tfrac56)
|
||||||
2n,2n,2n
|
=\sum_{j=0}^4c_jt^j
|
||||||
\end{matrix};z\right)
|
|
||||||
\]
|
\]
|
||||||
has a \(4\times4\) Euler companion system. Direct simplification gives
|
and define, for operator polynomials with coefficients on the left,
|
||||||
\[
|
\[
|
||||||
\mathcal C_n(z)\,[-zM(2n+1,-z/(1-z))]
|
\Theta Q=z\partial_zQ+tQ.
|
||||||
-\theta[-zM(2n+1,-z/(1-z))]
|
|
||||||
-[-zM(2n+1,-z/(1-z))]\mathcal C_{n+1}(z)=0.
|
|
||||||
\]
|
\]
|
||||||
The transformed seed \(-zC(-z/(1-z))\) is a horizontal adjoint row.
|
The four horizontal components are reconstructed from the first by
|
||||||
Eliminating its other three coordinates from the horizontal equation
|
|
||||||
produces exactly
|
|
||||||
\[
|
\[
|
||||||
\left[
|
\pi_0=1,\qquad
|
||||||
\theta(\theta-2n)^3
|
\pi_3=\frac{c_4}{c_0}t,\qquad
|
||||||
-z(\theta-n)(\theta-n-\tfrac16)
|
\pi_2=\frac{c_3}{c_4}\pi_3-\Theta\pi_3,\qquad
|
||||||
(\theta-n-\tfrac12)(\theta-n-\tfrac56)
|
\pi_1=\frac{c_2}{c_4}\pi_3-\Theta\pi_2.
|
||||||
\right]\widehat Q_N=0.
|
|
||||||
\]
|
\]
|
||||||
The analytic solution normalized at \(z=0\) is the terminating
|
The remaining horizontal equation is the direct factorization
|
||||||
\(\F43\) in \eqref{eq:qhat}.
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
\Theta\pi_1+1-\frac{c_1}{c_4}\pi_3
|
||||||
|
={}&-\frac{72}{n(2n+1)(6n+1)(6n+5)z}\bigl[
|
||||||
|
t(t-2n)^3\\
|
||||||
|
&\hspace{4em}
|
||||||
|
-z(t-n)(t-n-\tfrac16)
|
||||||
|
(t-n-\tfrac12)(t-n-\tfrac56)\bigr].
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
Let
|
||||||
|
\[
|
||||||
|
\mathcal C_n(z)=
|
||||||
|
\begin{pmatrix}
|
||||||
|
0&1&0&0\\
|
||||||
|
0&0&1&0\\
|
||||||
|
0&0&0&1\\
|
||||||
|
-c_0/c_4&-c_1/c_4&-c_2/c_4&-c_3/c_4
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
The propagation of the reconstructed row is the following sixteen-entry
|
||||||
|
identity:
|
||||||
|
\begin{equation}\label{eq:full-gauge}
|
||||||
|
\mathcal C_n[-z\mathcal M(2n+1,-z/(1-z))]
|
||||||
|
-\theta[-z\mathcal M(2n+1,-z/(1-z))]
|
||||||
|
-[-z\mathcal M(2n+1,-z/(1-z))]\mathcal C_{n+1}=0.
|
||||||
|
\end{equation}
|
||||||
|
Finally, direct contraction with the displayed matrix gives
|
||||||
|
\begin{equation}\label{eq:matrix-scalar-bridge}
|
||||||
|
\sum_{r=0}^3\pi_r(t)
|
||||||
|
\left[-z\mathcal M(2n+1,-z/(1-z))\right]_{r+1,1}
|
||||||
|
=d_0(t)+zd_1(t).
|
||||||
|
\end{equation}
|
||||||
|
These are identities in \(\Q(n,z)(t)\). The factors depending on the
|
||||||
|
integer \(n\) are nonzero for \(n\ge1\); no value is obtained by dividing
|
||||||
|
at \(z=0\), because the verifier cross-multiplies first and the reconstructed
|
||||||
|
base functions have removable limits there. The mandatory
|
||||||
|
sparse-polynomial verifier checks every
|
||||||
|
reconstruction equation, the closing factorization, and
|
||||||
|
\eqref{eq:full-gauge}--\eqref{eq:matrix-scalar-bridge} by cross
|
||||||
|
multiplication. For any reconstructed horizontal row these identities give
|
||||||
|
\begin{equation}\label{eq:terminating-step}
|
||||||
|
p_{n+1}
|
||||||
|
=\bigl(d_0(\theta)+zd_1(\theta)\bigr)p_n,
|
||||||
|
\end{equation}
|
||||||
|
where
|
||||||
|
\[
|
||||||
|
d_0(t)=
|
||||||
|
\frac{72(2n+1)^2(2n-t)^3}{n(6n+1)(6n+5)}
|
||||||
|
\]
|
||||||
|
and
|
||||||
|
\[
|
||||||
|
d_1(t)=-\frac{P(n,t)}{n(2n+1)(6n+1)(6n+5)}
|
||||||
|
\]
|
||||||
|
with
|
||||||
|
\begin{align*}
|
||||||
|
P(n,t)={}&-5n-76n^2+1404n^3+4360n^4+4320n^5+1440n^6\\
|
||||||
|
&+(5+127n-1760n^2-6536n^3-7632n^4-3024n^5)t\\
|
||||||
|
&+(-51+659n+3086n^2+4500n^3+2232n^4)t^2\\
|
||||||
|
&+(-72-432n-864n^2-576n^3)t^3.
|
||||||
|
\end{align*}
|
||||||
|
Thus \eqref{eq:terminating-step} is the scalar form of the displayed
|
||||||
|
matrix recurrence; no differential-equation uniqueness is used below.
|
||||||
|
|
||||||
For completeness, the CAS certificate does not rely only on this
|
Let
|
||||||
differential equation. It computes the actual one-step scalar operator
|
\[
|
||||||
and verifies its generic coefficient identity, its \(k=0\) normalization,
|
h_{n,k}=
|
||||||
and the separate top boundary \(k=n+1\). Every remainder simplifies
|
\frac{(-n)_k(-n-\frac16)_k(-n-\frac12)_k(-n-\frac56)_k}
|
||||||
identically to zero. This proves the statement for all \(n\), not merely
|
{(1-2n)_k^3k!}
|
||||||
for sampled values.
|
\quad(0\le k\le n),
|
||||||
|
\qquad
|
||||||
|
\nu_n=\frac{576n^2(2n+1)^2}{(6n+1)(6n+5)}.
|
||||||
|
\]
|
||||||
|
For \(n\ge1\), clearing the displayed nonzero denominators gives exactly
|
||||||
|
\begin{align}
|
||||||
|
d_0(0)&=\nu_n,\label{eq:term-constant}\\
|
||||||
|
d_0(k)+d_1(k-1)\frac{h_{n,k-1}}{h_{n,k}}
|
||||||
|
&=\nu_n\frac{h_{n+1,k}}{h_{n,k}}
|
||||||
|
\qquad(1\le k\le n),\label{eq:term-generic}\\
|
||||||
|
d_1(n)&=-\nu_n
|
||||||
|
\frac{(n+\frac76)(n+\frac32)(n+\frac{11}{6})}
|
||||||
|
{8(2n+1)^3}.\label{eq:term-top}
|
||||||
|
\end{align}
|
||||||
|
The base row is not assumed: from the first component of \(C\),
|
||||||
|
\[
|
||||||
|
q_0(x)=\frac{18}{x}+\frac{159}{4},\qquad
|
||||||
|
Q_0(x)=xq_0(x)=18+\frac{159}{4}x,
|
||||||
|
\]
|
||||||
|
and therefore
|
||||||
|
\[
|
||||||
|
p_1(z)=(1-z)Q_0\!\left(-\frac{z}{1-z}\right)
|
||||||
|
=18\left(1-\frac{77}{24}z\right).
|
||||||
|
\]
|
||||||
|
Direct application of the four displayed \(\pi_r\) operators gives the
|
||||||
|
four base identities
|
||||||
|
\begin{equation}\label{eq:base-horizontal-row}
|
||||||
|
-zC\!\left(-\frac{z}{1-z}\right)
|
||||||
|
=\left.(\pi_0(\theta)p_1,\pi_1(\theta)p_1,
|
||||||
|
\pi_2(\theta)p_1,\pi_3(\theta)p_1)\right|_{n=1}.
|
||||||
|
\end{equation}
|
||||||
|
The fourth base equation is also direct:
|
||||||
|
\[
|
||||||
|
\left[
|
||||||
|
\theta(\theta-2)^3
|
||||||
|
-z(\theta-1)(\theta-\tfrac76)
|
||||||
|
(\theta-\tfrac32)(\theta-\tfrac{11}{6})
|
||||||
|
\right]p_1=0.
|
||||||
|
\]
|
||||||
|
Equivalently, if \(H_1=-zC(-z/(1-z))\), then all four components of
|
||||||
|
\[
|
||||||
|
\theta H_1+H_1\mathcal C_1=0
|
||||||
|
\]
|
||||||
|
vanish. The mandatory verifier checks both forms independently.
|
||||||
|
Moreover,
|
||||||
|
\[
|
||||||
|
\deg((d_0(\theta)+zd_1(\theta))p_n)\le n+1.
|
||||||
|
\]
|
||||||
|
Equations \eqref{eq:term-constant}--\eqref{eq:term-top} therefore prove,
|
||||||
|
coefficient by coefficient, that the right side of
|
||||||
|
\eqref{eq:terminating-step} is
|
||||||
|
\(\alpha_{n+1}\sum_{k=0}^{n+1}h_{n+1,k}z^k\).
|
||||||
|
Starting from \eqref{eq:base-horizontal-row},
|
||||||
|
\eqref{eq:full-gauge} propagates the horizontal form at every step.
|
||||||
|
This proves \eqref{eq:qhat} and \eqref{eq:normalization} for the actual
|
||||||
|
row \(CG_N\), not merely for a scalar surrogate.
|
||||||
|
The mandatory standalone checker independently expands the cleared
|
||||||
|
identities and rejects any nonzero coefficient.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\begin{corollary}[Positivity at the CM point]\label{cor:positivity}
|
\begin{corollary}[Positivity at the CM point]\label{cor:positivity}
|
||||||
|
|
@ -515,10 +769,19 @@ and therefore
|
||||||
\le10^4\left(\frac um\right)^{i-1}
|
\le10^4\left(\frac um\right)^{i-1}
|
||||||
\left(\frac u{m+1}\right)^{3-j}.
|
\left(\frac u{m+1}\right)^{3-j}.
|
||||||
\]
|
\]
|
||||||
For \(m\ge1\), \(u/m\le5\) and \(u/(m+1)\le5/2\); summing four entries in
|
For \(m\ge1\), \(u/m\le5\) and \(u/(m+1)\le5/2\). Because the exponent
|
||||||
each row gives the deliberately loose uniform bound
|
\(3-j\) is negative when \(j=4\), we use the exact case split
|
||||||
\[
|
\[
|
||||||
\|\mathcal B_m\|_\infty\le4\cdot10^8,\qquad
|
\left(\frac{u}{m+1}\right)^{3-j}\le
|
||||||
|
\begin{cases}
|
||||||
|
(5/2)^{3-j}\le25/4,&j\le3,\\[1mm]
|
||||||
|
1/2,&j=4,
|
||||||
|
\end{cases}
|
||||||
|
\]
|
||||||
|
where the second line follows from \(u/(m+1)=2+1/(m+1)\ge2\).
|
||||||
|
Thus every entry is at most \(7{,}812{,}500\), and summing each row gives
|
||||||
|
\[
|
||||||
|
\|\mathcal B_m\|_\infty\le31{,}250{,}000<4\cdot10^8,\qquad
|
||||||
\|M_0\|_\infty<10^7.
|
\|M_0\|_\infty<10^7.
|
||||||
\]
|
\]
|
||||||
The balancing telescopes:
|
The balancing telescopes:
|
||||||
|
|
@ -531,6 +794,23 @@ It follows that, for \(N\ge1\),
|
||||||
\max_{|x|=1/4}|\mathcal R_{N,r}(x)|
|
\max_{|x|=1/4}|\mathcal R_{N,r}(x)|
|
||||||
\le6\cdot10^{10}(N!)^2(4\cdot10^8)^{N-1}(1/4)^n.
|
\le6\cdot10^{10}(N!)^2(4\cdot10^8)^{N-1}(1/4)^n.
|
||||||
\end{equation}
|
\end{equation}
|
||||||
|
We now verify the analytic hypothesis behind the next step. On
|
||||||
|
\(|x|\le1/4\),
|
||||||
|
\[
|
||||||
|
\left|-\frac{x}{1-x}\right|\le\frac13<1,
|
||||||
|
\]
|
||||||
|
so the series defining \(y\) and its first three Euler derivatives are
|
||||||
|
holomorphic on a neighborhood of the closed disk. Because \(f=O(x)\),
|
||||||
|
the simple pole of \(C\) cancels in \(fC\), so \(\mathcal E_0\) is
|
||||||
|
holomorphic there. Inspection of \eqref{eq:deformed-matrix} shows that
|
||||||
|
each \(M_m\) is holomorphic off \(x=0\) in this disk and has at most a
|
||||||
|
simple pole at \(0\). Hence
|
||||||
|
\(\mathcal R_{N,r}=x^n(\mathcal E_N)_{r,1}\), with \(n=N+1\), is
|
||||||
|
holomorphic on the disk after removing its possible singularity at zero.
|
||||||
|
Proposition~\ref{prop:divisibility} strengthens its order there to at
|
||||||
|
least \(2n\). Therefore
|
||||||
|
\(\mathcal R_{N,r}(x)/x^{2n}\) has a removable singularity at zero and
|
||||||
|
is holomorphic on a neighborhood of the closed disk.
|
||||||
Applying the maximum principle to
|
Applying the maximum principle to
|
||||||
\(\mathcal R_{N,r}(x)/x^{2n}\) gives
|
\(\mathcal R_{N,r}(x)/x^{2n}\) gives
|
||||||
\begin{equation}\label{eq:cauchy}
|
\begin{equation}\label{eq:cauchy}
|
||||||
|
|
@ -552,9 +832,9 @@ Combining this with \eqref{eq:cauchy}, we obtain
|
||||||
\begin{equation}\label{eq:geometric-error}
|
\begin{equation}\label{eq:geometric-error}
|
||||||
\left|\frac{E_{N,r}(x_0)}{q_N(x_0)}\right|
|
\left|\frac{E_{N,r}(x_0)}{q_N(x_0)}\right|
|
||||||
=\left|\frac{\mathcal R_{N,r}(x_0)}{Q_N(x_0)}\right|
|
=\left|\frac{\mathcal R_{N,r}(x_0)}{Q_N(x_0)}\right|
|
||||||
\le C(x_0)\,\beta(x_0)^N,
|
\le K_0\,\beta(x_0)^N,
|
||||||
\end{equation}
|
\end{equation}
|
||||||
where \(C(x_0)<\infty\) and
|
where \(K_0<\infty\) is independent of \(N\) and
|
||||||
\[
|
\[
|
||||||
\beta(x_0)=
|
\beta(x_0)=
|
||||||
\frac{4\cdot10^8}{29}
|
\frac{4\cdot10^8}{29}
|
||||||
|
|
@ -592,9 +872,22 @@ Equation \eqref{eq:CM-value} therefore proves
|
||||||
|
|
||||||
\section{The other three official columns}
|
\section{The other three official columns}
|
||||||
|
|
||||||
For completeness, we recall the exact finite-frame reduction already used
|
All matrices in this section are evaluated at \(x=x_0=1/R\).
|
||||||
to establish convergence of the recurrence. The balanced transfer tends
|
For \(m\ge1\), retain
|
||||||
to
|
\[
|
||||||
|
D_m=\diag(1,m,m^2,m^3),\qquad
|
||||||
|
\mathcal B_m=D_m^{-1}M_mD_{m+1}/(m+1)^2,
|
||||||
|
\]
|
||||||
|
and, for any row \(a\), put
|
||||||
|
\[
|
||||||
|
Z_m(a)=\frac{aG_mD_m}{(m!)^2}.
|
||||||
|
\]
|
||||||
|
Then the balancing gives the exact recurrence
|
||||||
|
\begin{equation}\label{eq:balanced-row-recurrence}
|
||||||
|
Z_{m+1}(a)=Z_m(a)\mathcal B_m.
|
||||||
|
\end{equation}
|
||||||
|
Substitution in the displayed matrix shows, entry by entry, that
|
||||||
|
\(\mathcal B_m-\mathcal S=O(m^{-1})\), where
|
||||||
\[
|
\[
|
||||||
\mathcal S=
|
\mathcal S=
|
||||||
\begin{pmatrix}
|
\begin{pmatrix}
|
||||||
|
|
@ -611,94 +904,255 @@ Q_R(t)={}&R^2t^4-(64R^3-56R^2-4)t^3\\
|
||||||
&+(48R^2-262R+220)t^2-(12R-8)t+1.
|
&+(48R^2-262R+220)t^2-(12R-8)t+1.
|
||||||
\end{aligned}
|
\end{aligned}
|
||||||
\]
|
\]
|
||||||
The quartic is irreducible. Its spectral separation is also exact: on
|
On \(|t|=1\), the cubic coefficient strictly dominates the sum of the
|
||||||
\(|t|=1\), the absolute value of its cubic coefficient exceeds the sum of
|
other four coefficient magnitudes, because
|
||||||
the other coefficient magnitudes, because
|
|
||||||
\[
|
\[
|
||||||
(64R^3-56R^2-4)-(49R^2-250R+213)
|
(64R^3-56R^2-4)-(49R^2-250R+213)
|
||||||
=64R^3-105R^2+250R-217>0.
|
=64R^3-105R^2+250R-217>0.
|
||||||
\]
|
\]
|
||||||
Rouch\'e's theorem therefore places exactly three roots in \(|t|<1\) and
|
To count the roots without an irreducibility or root-finder call, consider
|
||||||
the remaining root \(\rho\) in \(|t|>1\). Hence \(\rho\) is the unique
|
|
||||||
root of maximal modulus.
|
|
||||||
|
|
||||||
We next remove any possible nonvanishing assumption about the denominator.
|
|
||||||
The positivity estimate above and \(Q_N=x_0^nq_N\) give
|
|
||||||
\begin{equation}\label{eq:q-lower}
|
|
||||||
q_N(x_0)\ge
|
|
||||||
18\cdot29^N(N!)^2
|
|
||||||
\left(\frac{1-x_0}{x_0}\right)^{N+1}.
|
|
||||||
\end{equation}
|
|
||||||
The scalar recurrence obtained from the first cyclic coordinate is of
|
|
||||||
Poincar\'e type after the \((N!)^2\) balancing. The discrete
|
|
||||||
Birkhoff--Poincar\'e theorem \([4,\text{ Chapters 3 and 5}]\) applies because
|
|
||||||
the balanced coefficients are rational in \(N\), have full expansions in
|
|
||||||
\(N^{-1}\), and the limiting spectrum is simple. If the coefficient of the
|
|
||||||
\(\rho\)-mode in \(q_N\) were zero, the three-root separation just proved
|
|
||||||
would give, for some \(\tau<1\),
|
|
||||||
\[
|
\[
|
||||||
|q_N(x_0)|\le K_\tau (N!)^2\tau^N.
|
H_s(t)=-(64R^3-56R^2-4)t^3+
|
||||||
|
s\{R^2t^4+(48R^2-262R+220)t^2-(12R-8)t+1\}.
|
||||||
\]
|
\]
|
||||||
This contradicts \eqref{eq:q-lower}. Thus the dominant denominator
|
The strict inequality above gives \(H_s(t)\ne0\) for
|
||||||
coefficient is nonzero by a wholly exact argument.
|
\(|t|=1\), \(0\le s\le1\). Thus the winding number of
|
||||||
|
\(H_s(e^{i\vartheta})\) about zero cannot change with \(s\); at \(s=0\)
|
||||||
|
it is \(3\). Hence \(Q_R=H_1\) has three zeros in \(|t|<1\) and one,
|
||||||
|
counted with multiplicity, in \(|t|>1\). Moreover
|
||||||
|
\[
|
||||||
|
Q_R(1)=-(64R^3-105R^2+274R-233)<0,\qquad
|
||||||
|
\lim_{t\to+\infty}Q_R(t)=+\infty.
|
||||||
|
\]
|
||||||
|
Consequently the unique exterior zero is a simple real number
|
||||||
|
\(\rho>1\).
|
||||||
|
|
||||||
It remains to transfer the first-column result to the other columns. For
|
\begin{lemma}[Explicit dominant-product dichotomy]
|
||||||
\(r\ge1\), put
|
\label{lem:dominant-product}
|
||||||
|
Fix \(\tau\) with
|
||||||
|
\[
|
||||||
|
\max_{\lambda\ne\rho}|\lambda|<\tau<1,
|
||||||
|
\]
|
||||||
|
Then there exist a late index \(m_0\), a linear functional \(\Lambda\) on
|
||||||
|
rows, nonzero scalars \(L_m\) independent of the row, and a left
|
||||||
|
\(\rho\)-eigenvector \(w\) of \(\mathcal S\) such that the following
|
||||||
|
alternatives hold:
|
||||||
|
\begin{align}
|
||||||
|
\Lambda(a)=0&\quad\Longrightarrow\quad
|
||||||
|
\|Z_m(a)\|\le K_a\tau^{m-m_0},\label{eq:exceptional-decay}\\
|
||||||
|
\Lambda(a)\ne0&\quad\Longrightarrow\quad
|
||||||
|
Z_m(a)=\Lambda(a)L_m\bigl(w+o_a(1)\bigr).
|
||||||
|
\label{eq:dominant-asymptotic}
|
||||||
|
\end{align}
|
||||||
|
\end{lemma}
|
||||||
|
|
||||||
|
\begin{proof}
|
||||||
|
Choose an invertible \(P\) with
|
||||||
|
\[
|
||||||
|
P^{-1}\mathcal SP=
|
||||||
|
\begin{pmatrix}\rho&0\\0&A\end{pmatrix},
|
||||||
|
\qquad\operatorname{spr}(A)<1.
|
||||||
|
\]
|
||||||
|
Choose \(\operatorname{spr}(A)<\theta<\tau\). For stable rows define
|
||||||
|
\[
|
||||||
|
\|\beta\|_\theta=\sum_{k=0}^{\infty}
|
||||||
|
\theta^{-k}\|\beta A^k\|_0.
|
||||||
|
\]
|
||||||
|
The finite Jordan identity
|
||||||
|
\[
|
||||||
|
J_\lambda^k=\sum_{\ell=0}^{s-1}
|
||||||
|
\binom{k}{\ell}\lambda^{k-\ell}N^\ell
|
||||||
|
\]
|
||||||
|
gives, for \(\operatorname{spr}(A)<\eta<\theta\),
|
||||||
|
\(\|A^k\|_0\le Ck^2\eta^k\); hence the series converges and
|
||||||
|
\[
|
||||||
|
\|\beta A\|_\theta
|
||||||
|
=\theta\sum_{k=1}^{\infty}\theta^{-k}\|\beta A^k\|_0
|
||||||
|
\le\theta\|\beta\|_\theta.
|
||||||
|
\]
|
||||||
|
Use the dual norm for stable columns.
|
||||||
|
|
||||||
|
Write
|
||||||
|
\[
|
||||||
|
T_m=P^{-1}\mathcal B_mP=
|
||||||
|
\begin{pmatrix}a_m&b_m\\c_m&E_m\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
Then \(a_m\to\rho\), \(b_m,c_m\to0\), and \(E_m\to A\).
|
||||||
|
Choose
|
||||||
|
\[
|
||||||
|
\theta<d_*<\tau<1<a_*<\rho.
|
||||||
|
\]
|
||||||
|
For sufficiently large \(m_0\), a positive \(\epsilon\) makes, for
|
||||||
|
\(m\ge m_0\),
|
||||||
|
\begin{gather}
|
||||||
|
|a_m|\ge a_*,\quad\|E_m\|\le d_*,
|
||||||
|
\quad\|b_m\|,\|c_m\|\le\epsilon,\label{eq:block-bounds}\\
|
||||||
|
d_*+\epsilon<\tau,\quad a_*-\epsilon>1,\quad
|
||||||
|
d_*+\epsilon<a_*-\epsilon,\label{eq:block-separation}\\
|
||||||
|
q:=\frac{d_*}{a_*-\epsilon}
|
||||||
|
+\frac{(d_*+\epsilon)\epsilon}{(a_*-\epsilon)^2}<1.
|
||||||
|
\label{eq:graph-contraction-constant}
|
||||||
|
\end{gather}
|
||||||
|
For stable columns \(\|h\|\le1\), set
|
||||||
|
\[
|
||||||
|
\Psi_m(h)=\frac{E_mh-c_m}{a_m-b_mh}.
|
||||||
|
\]
|
||||||
|
Equations \eqref{eq:block-bounds}--\eqref{eq:block-separation} give
|
||||||
|
\[
|
||||||
|
\|\Psi_m(h)\|
|
||||||
|
\le\frac{d_*+\epsilon}{a_*-\epsilon}<1.
|
||||||
|
\]
|
||||||
|
For two such columns,
|
||||||
|
\[
|
||||||
|
\Psi_m(h)-\Psi_m(k)
|
||||||
|
=\frac{E_m(h-k)}{a_m-b_mh}
|
||||||
|
+\frac{(E_mk-c_m)b_m(h-k)}
|
||||||
|
{(a_m-b_mh)(a_m-b_mk)},
|
||||||
|
\]
|
||||||
|
so \eqref{eq:graph-contraction-constant} gives
|
||||||
|
\[
|
||||||
|
\|\Psi_m(h)-\Psi_m(k)\|\le q\|h-k\|.
|
||||||
|
\]
|
||||||
|
|
||||||
|
For \(M>m\), set \(h_M^{(M)}=0\) and recurse backward by
|
||||||
|
\(h_j^{(M)}=\Psi_j(h_{j+1}^{(M)})\). Then, for \(M'>M\),
|
||||||
|
\[
|
||||||
|
\|h_m^{(M')}-h_m^{(M)}\|\le2q^{M-m}.
|
||||||
|
\]
|
||||||
|
Thus \(h_m=\lim_{M\to\infty}h_m^{(M)}\) exists and satisfies
|
||||||
|
\begin{equation}\label{eq:graph-invariance}
|
||||||
|
h_ma_m+c_m=(h_mb_m+E_m)h_{m+1}.
|
||||||
|
\end{equation}
|
||||||
|
The defining recurrence gives the explicit bound
|
||||||
|
\[
|
||||||
|
\|h_m\|\le
|
||||||
|
\frac{\|E_m\|\|h_{m+1}\|+\|c_m\|}
|
||||||
|
{|a_m|-\|b_m\|}.
|
||||||
|
\]
|
||||||
|
Together with \(\|A\|_\theta/\rho<1\), this gives
|
||||||
|
\[
|
||||||
|
\limsup_{m\to\infty}\|h_m\|
|
||||||
|
\le\frac{\theta}{\rho}\limsup_{m\to\infty}\|h_m\|,
|
||||||
|
\qquad\text{hence}\qquad h_m\to0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Write
|
||||||
|
\[
|
||||||
|
U_m(a)=Z_m(a)P=(\alpha_m,\beta_m),\qquad
|
||||||
|
\xi_m=\alpha_m-\beta_mh_m,\qquad
|
||||||
|
d_m=a_m-b_mh_{m+1}.
|
||||||
|
\]
|
||||||
|
Using \eqref{eq:graph-invariance} in
|
||||||
|
\(U_{m+1}=U_mT_m\) gives the exact scalar equation
|
||||||
|
\[
|
||||||
|
\xi_{m+1}=d_m\xi_m.
|
||||||
|
\]
|
||||||
|
Define the composed seed functional and product
|
||||||
|
\[
|
||||||
|
\Lambda(a)=\alpha_{m_0}(a)-\beta_{m_0}(a)h_{m_0},\qquad
|
||||||
|
L_m=\prod_{\ell=m_0}^{m-1}d_\ell.
|
||||||
|
\]
|
||||||
|
Both are now explicit, \(\Lambda\) is linear, and
|
||||||
|
\(\xi_m=\Lambda(a)L_m\). Equations
|
||||||
|
\eqref{eq:block-bounds}--\eqref{eq:block-separation} ensure
|
||||||
|
\(d_m\ne0\).
|
||||||
|
|
||||||
|
If \(\Lambda(a)=0\), then \(\alpha_m=\beta_mh_m\) and
|
||||||
|
\[
|
||||||
|
\beta_{m+1}=\beta_m(E_m+h_mb_m),\qquad
|
||||||
|
\|\beta_{m+1}\|<(d_*+\epsilon)\|\beta_m\|
|
||||||
|
<\tau\|\beta_m\|,
|
||||||
|
\]
|
||||||
|
which proves \eqref{eq:exceptional-decay}.
|
||||||
|
|
||||||
|
If \(\Lambda(a)\ne0\), put \(r_m=\beta_m/\xi_m\). Exact substitution
|
||||||
|
gives
|
||||||
|
\[
|
||||||
|
r_{m+1}
|
||||||
|
=\frac{b_m+r_m(E_m+h_mb_m)}{d_m}.
|
||||||
|
\]
|
||||||
|
Here \(b_m/d_m\to0\) and
|
||||||
|
\((E_m+h_mb_m)/d_m\to A/\rho\), whose norm is below one.
|
||||||
|
Enlarge \(m_0\) once more, redefining \(\Lambda\) and \(L_m\) from this
|
||||||
|
new index, so that for some \(q_1<1\),
|
||||||
|
\[
|
||||||
|
\left\|\frac{E_m+h_mb_m}{d_m}\right\|\le q_1
|
||||||
|
\qquad(m\ge m_0).
|
||||||
|
\]
|
||||||
|
Then, for every \(m\ge m_0\),
|
||||||
|
\[
|
||||||
|
\|r_m\|\le q_1^{m-m_0}\|r_{m_0}\|
|
||||||
|
+\sum_{\ell=m_0}^{m-1}q_1^{m-1-\ell}
|
||||||
|
\left\|\frac{b_\ell}{d_\ell}\right\|\longrightarrow0.
|
||||||
|
\]
|
||||||
|
Since \(\alpha_m/\xi_m=1+r_mh_m\to1\),
|
||||||
|
\[
|
||||||
|
U_m(a)=\Lambda(a)L_m\bigl((1,0)+o_a(1)\bigr).
|
||||||
|
\]
|
||||||
|
Multiplying by \(P^{-1}\) proves
|
||||||
|
\eqref{eq:dominant-asymptotic} with
|
||||||
|
\[
|
||||||
|
w=(1,0)P^{-1},\qquad w\mathcal S=\rho w.
|
||||||
|
\]
|
||||||
|
\end{proof}
|
||||||
|
|
||||||
|
No GCD or irreducibility decision is needed to show that all four
|
||||||
|
coordinates of \(w\) are nonzero. Define the polynomial row \(w(t)\) by
|
||||||
\[
|
\[
|
||||||
\begin{aligned}
|
\begin{aligned}
|
||||||
F_r&=[\,\e_1,M_r\e_1,M_rM_{r+1}\e_1,
|
w_1(t)={}&Rt(Rt^2-7)+12R^2t^2+4t^2+44t+10,\\
|
||||||
M_rM_{r+1}M_{r+2}\e_1\,],\\
|
\frac{w_2(t)}2={}&R^2t((48R-27)t-28)
|
||||||
\gamma_{r,k}&=\prod_{\ell=1}^{k}(r+\ell)^2,\\
|
+(194R-108)t+40R-23,\\
|
||||||
C_r&=[\,\e_1,\mathcal B_r\e_1,
|
w_3(t)={}&R^2t((48R-17)t-8)
|
||||||
\mathcal B_r\mathcal B_{r+1}\e_1,
|
+(198R-68)t+71R-32,\\
|
||||||
\mathcal B_r\mathcal B_{r+1}\mathcal B_{r+2}\e_1\,].
|
w_4(t)={}&2R(8+(17+3R)t+4R^2t^2).
|
||||||
\end{aligned}
|
\end{aligned}
|
||||||
\]
|
\]
|
||||||
The balancing telescopes exactly:
|
Direct multiplication gives the exact polynomial identity
|
||||||
\[
|
\[
|
||||||
F_r=D(r)C_r\diag(\gamma_{r,0},\ldots,\gamma_{r,3}),
|
w(t)(tI-\mathcal S)=(Q_R(t),0,0,0).
|
||||||
\qquad
|
|
||||||
C_r\longrightarrow
|
|
||||||
C=[\,\e_1,\mathcal S\e_1,\mathcal S^2\e_1,\mathcal S^3\e_1\,].
|
|
||||||
\]
|
\]
|
||||||
The limiting cyclic frame is nonsingular:
|
At \(t=\rho\), this is a left \(\rho\)-eigenvector. The exterior
|
||||||
|
eigenspace is one-dimensional, so the vector in
|
||||||
|
Lemma~\ref{lem:dominant-product} may be rescaled to \(w(\rho)\), with the
|
||||||
|
inverse rescaling absorbed into \(L_m\). Since \(R>7\) and \(\rho>1\),
|
||||||
|
every displayed grouping is positive. Thus \(w_j(\rho)>0\) for
|
||||||
|
\(j=1,2,3,4\); below we abbreviate \(w_j=w_j(\rho)\).
|
||||||
|
|
||||||
|
Undoing the balancing in \eqref{eq:dominant-asymptotic} gives, whenever
|
||||||
|
\(\Lambda(a)\ne0\),
|
||||||
|
\begin{equation}\label{eq:all-column-asymptotic}
|
||||||
|
aG_m\e_j=(m!)^2m^{-(j-1)}
|
||||||
|
\Lambda(a)L_m\bigl(w_j+o_a(1)\bigr).
|
||||||
|
\end{equation}
|
||||||
|
It remains to verify that the two official rows are not exceptional.
|
||||||
|
The positivity estimate and \(Q_m=x_0^{m+1}q_m\) give
|
||||||
|
\begin{equation}\label{eq:q-lower}
|
||||||
|
\frac{q_m(x_0)}{(m!)^2}
|
||||||
|
\ge18(R-1)\,[29(R-1)]^m.
|
||||||
|
\end{equation}
|
||||||
|
If \(\Lambda(C)=0\), the first coordinate of
|
||||||
|
\eqref{eq:exceptional-decay} would contradict \eqref{eq:q-lower}.
|
||||||
|
Therefore
|
||||||
\[
|
\[
|
||||||
\det C
|
\Lambda(A_1)=S\Lambda(C)\ne0.
|
||||||
=-\frac{4(27R-11)(128R^2-149R-43)}{R^6}\ne0.
|
|
||||||
\]
|
\]
|
||||||
Thus \(F_r\) is invertible for all sufficiently large \(r\). If
|
If \(\Lambda(A_0)=0\), then
|
||||||
\(y_r(a)=aG_r\e_1\), exact inversion of this frame gives
|
\eqref{eq:exceptional-decay}, \eqref{eq:dominant-asymptotic}, and
|
||||||
|
\(|d_m|>1\) for large \(m\) would make the first-column quotient tend
|
||||||
|
to zero, contradicting \eqref{eq:first-column}. Hence
|
||||||
|
\(\Lambda(A_0)\ne0\) as well.
|
||||||
|
|
||||||
|
Because \(w_j>0\), equation \eqref{eq:all-column-asymptotic} first proves
|
||||||
|
that every \(Q_{m,j}\) is nonzero for all sufficiently large \(m\), and
|
||||||
|
only then permits division:
|
||||||
\[
|
\[
|
||||||
aG_r\e_j=r^{-(j-1)}
|
\lim_{m\to\infty}\frac{P_{m,j}}{Q_{m,j}}
|
||||||
\sum_{k=0}^{3}(C_r^{-1})_{k+1,j}
|
=\frac{\Lambda(A_0)}{\Lambda(A_1)}
|
||||||
\frac{y_{r+k}(a)}{\gamma_{r,k}}.
|
=\lim_{m\to\infty}\frac{P_{m,1}}{Q_{m,1}}
|
||||||
|
=\frac{\sqrt{10005}}{\pi}.
|
||||||
\]
|
\]
|
||||||
The same Birkhoff--Poincar\'e theorem supplies a linear dominant functional
|
We conclude:
|
||||||
\(\Lambda\) and an exponent \(\sigma\) such that, for fixed \(k\),
|
|
||||||
\[
|
|
||||||
\frac{y_{r+k}(a)}
|
|
||||||
{(r!)^2\rho^r r^\sigma\gamma_{r,k}}
|
|
||||||
\longrightarrow\Lambda(a)\rho^k.
|
|
||||||
\]
|
|
||||||
Consequently
|
|
||||||
\[
|
|
||||||
\frac{aG_r\e_j}
|
|
||||||
{(r!)^2\rho^r r^{\sigma-(j-1)}}
|
|
||||||
\longrightarrow\Lambda(a)\,\widetilde w_j,\qquad
|
|
||||||
\widetilde w=[1,\rho,\rho^2,\rho^3]C^{-1}.
|
|
||||||
\]
|
|
||||||
An explicit left eigenvector is obtained from the first row of
|
|
||||||
\(R^2\operatorname{adj}(tI-\mathcal S)\). Each of its four coordinate
|
|
||||||
polynomials is coprime to \(Q_R\); hence no coordinate vanishes at \(\rho\).
|
|
||||||
It is a nonzero multiple of \(\widetilde w\), so
|
|
||||||
\(\widetilde w_j\ne0\) for every \(j\). Applying the last limit to
|
|
||||||
\(a=A_0,A_1\), using the exact denominator nonvanishing above, gives
|
|
||||||
\[
|
|
||||||
\lim_{N\to\infty}\frac{P_{N,j}}{Q_{N,j}}
|
|
||||||
=\frac{\Lambda(A_0)}{\Lambda(A_1)}
|
|
||||||
\qquad(j=1,2,3,4).
|
|
||||||
\]
|
|
||||||
Equation \eqref{eq:first-column} evaluates this common ratio. We conclude:
|
|
||||||
|
|
||||||
\begin{theorem}[Ramanujan Challenge Problem 2.8]\label{thm:main}
|
\begin{theorem}[Ramanujan Challenge Problem 2.8]\label{thm:main}
|
||||||
For every official column \(j=1,2,3,4\),
|
For every official column \(j=1,2,3,4\),
|
||||||
|
|
@ -727,29 +1181,42 @@ The proof package contains the following certificates.
|
||||||
File & Exact obligation\\
|
File & Exact obligation\\
|
||||||
\midrule
|
\midrule
|
||||||
\path{p28_full_closure_certificate.wl}
|
\path{p28_full_closure_certificate.wl}
|
||||||
& Authoritative differential gauge; nonterminating tail contiguity;
|
& Optional independent Wolfram cross-check of the differential gauge and
|
||||||
terminating adjoint equation; coefficientwise \(n\)-contiguity;
|
hypergeometric closure.\\
|
||||||
normalization and top boundary; exact spectral and cyclic-frame closure.\\
|
\path{p28_standalone_equations.py}
|
||||||
|
& Mandatory dependency-free expansion of the four cleared Ore
|
||||||
|
factorizations, the tail coefficient equations, the terminating base,
|
||||||
|
generic, and top identities, ascension, and the \(\F32\) equation.\\
|
||||||
|
\path{p28_dominant_product_algebra.py}
|
||||||
|
& Mandatory dependency-free verification of
|
||||||
|
\(\mathcal B_m=\mathcal S+O(m^{-1})\), the characteristic polynomial,
|
||||||
|
the root-separation inequalities, the left-eigenvector identity, and
|
||||||
|
the four positive coordinate rewrites.\\
|
||||||
\path{p28_kernel_contiguity_certificate.sage}
|
\path{p28_kernel_contiguity_certificate.sage}
|
||||||
& Independent coefficient/Ore proof of \(M_Nk_{N+1}=k_N\).\\
|
& Optional independent Sage check of the four displayed
|
||||||
|
factorizations; it performs no Ore division.\\
|
||||||
\path{p28_lattice_hypotheses_certificate.sage}
|
\path{p28_lattice_hypotheses_certificate.sage}
|
||||||
& Rank-one factorization, tail direction, and transformed ODE identities.\\
|
& Optional exact cross-check of the rank-one factorization, tail
|
||||||
|
direction, and transformed ODE identities.\\
|
||||||
\path{p28_convergence_constants.py}
|
\path{p28_convergence_constants.py}
|
||||||
& Exact rational verification of the coefficient bounds,
|
& Exact rational verification of the coefficient bounds,
|
||||||
\(\alpha_{n+1}/\alpha_n\ge29n^2\), and \(\beta(x_0)<1\).\\
|
\(\alpha_{n+1}/\alpha_n\ge29n^2\), and \(\beta(x_0)<1\).\\
|
||||||
\path{all_four_columns_certificate.sage}
|
\path{all_four_columns_certificate.sage}
|
||||||
& Balanced limit, Rouch\'e separation, nonzero eigenvector coordinates,
|
& Optional Sage cross-check of the balanced limit and exterior-root
|
||||||
and invertible cyclic frame.\\
|
algebra; the analytic contraction is proved in Lemma~\ref{lem:dominant-product}.\\
|
||||||
\path{p28_parametric_pade_probe.py}
|
\path{p28_parametric_pade_probe.py}
|
||||||
& Dependency-free finite exact regression of the predicted valuations.\\
|
& Diagnostic finite exact regression of the predicted valuations; it is
|
||||||
|
not used as proof of an all-\(N\) statement.\\
|
||||||
\bottomrule
|
\bottomrule
|
||||||
\end{tabular}
|
\end{tabular}
|
||||||
\end{center}
|
\end{center}
|
||||||
|
|
||||||
The Wolfram certificate performs symbolic identities over
|
The two mandatory algebra checkers use only the standard library's
|
||||||
\(\Q(n,z)\); it uses no numerical samples. The Python constants check uses
|
\texttt{fractions.Fraction}, sparse coefficient dictionaries, and explicit
|
||||||
only the standard library's \texttt{fractions.Fraction}. The SageMath
|
addition, multiplication, differentiation, and determinant expansion.
|
||||||
files are independent exact cross-checks.
|
They invoke no division algorithm, factorizer, root finder, special-function
|
||||||
|
library, or numerical sample. Wolfram Language and SageMath are optional
|
||||||
|
independent cross-checks, not a trust requirement.
|
||||||
|
|
||||||
\section*{References}
|
\section*{References}
|
||||||
\addcontentsline{toc}{section}{References}
|
\addcontentsline{toc}{section}{References}
|
||||||
|
|
@ -758,6 +1225,10 @@ files are independent exact cross-checks.
|
||||||
\item D. V. Chudnovsky and G. V. Chudnovsky,
|
\item D. V. Chudnovsky and G. V. Chudnovsky,
|
||||||
``Approximations and complex multiplication according to Ramanujan,''
|
``Approximations and complex multiplication according to Ramanujan,''
|
||||||
in \emph{Ramanujan Revisited}, Academic Press, 1988, pp.~375--472.
|
in \emph{Ramanujan Revisited}, Academic Press, 1988, pp.~375--472.
|
||||||
|
\item L. Milla,
|
||||||
|
``A detailed proof of the Chudnovsky formula with means of basic
|
||||||
|
complex analysis,'' arXiv:1809.00533v6, 2021,
|
||||||
|
\href{https://arxiv.org/abs/1809.00533}{arXiv:1809.00533}.
|
||||||
\item J. L. Fields,
|
\item J. L. Fields,
|
||||||
``Rational approximations to generalized hypergeometric functions,''
|
``Rational approximations to generalized hypergeometric functions,''
|
||||||
\emph{Mathematics of Computation} \textbf{19} (1965), 606--624,
|
\emph{Mathematics of Computation} \textbf{19} (1965), 606--624,
|
||||||
|
|
@ -767,9 +1238,6 @@ files are independent exact cross-checks.
|
||||||
``Hermite--Pad\'e approximants of generalized hypergeometric
|
``Hermite--Pad\'e approximants of generalized hypergeometric
|
||||||
functions,'' \emph{Russian Acad. Sci. Sb. Math.}
|
functions,'' \emph{Russian Acad. Sci. Sb. Math.}
|
||||||
\textbf{83} (1995), 189--219.
|
\textbf{83} (1995), 189--219.
|
||||||
\item S. Bodine and D. A. Lutz,
|
|
||||||
\emph{Asymptotic Integration of Differential and Difference Equations},
|
|
||||||
Lecture Notes in Mathematics 2129, Springer, 2015, Chapters 3 and 5.
|
|
||||||
\item The Ramanujan Machine,
|
\item The Ramanujan Machine,
|
||||||
\href{https://www.ramanujanmachine.com/ramanujan-challenge/}
|
\href{https://www.ramanujanmachine.com/ramanujan-challenge/}
|
||||||
{Ramanujan Challenge}, Problem 2.8.
|
{Ramanujan Challenge}, Problem 2.8.
|
||||||
|
|
|
||||||
111
experiments/ramanujan_28/submission/ADVERSARIAL_AUDIT.md
Normal file
111
experiments/ramanujan_28/submission/ADVERSARIAL_AUDIT.md
Normal file
|
|
@ -0,0 +1,111 @@
|
||||||
|
# Adversarial Audit — Ramanujan Challenge Problem 2.8
|
||||||
|
|
||||||
|
## Verdict
|
||||||
|
|
||||||
|
The recurrence-specific proof path passes the repaired adversarial audit.
|
||||||
|
Every Ore, differential-gauge, terminating-induction, valuation, convergence,
|
||||||
|
and all-four-column obligation is now displayed as an equation and replayed
|
||||||
|
without a computer-algebra decision procedure.
|
||||||
|
|
||||||
|
The exact trust boundary is important:
|
||||||
|
|
||||||
|
- The proof imports the classical Chudnovsky formula as one explicitly named
|
||||||
|
theorem, with a precise citation to a complete modular/CM derivation.
|
||||||
|
- It also uses foundational results stated with their hypotheses: polynomial
|
||||||
|
continuity, the winding-number/argument-principle root count, the maximum
|
||||||
|
modulus principle, finite-dimensional Jordan decomposition, and completeness
|
||||||
|
of finite-dimensional normed spaces.
|
||||||
|
- It does **not** claim to be axiom-free or to reconstruct those foundational
|
||||||
|
theorems from set theory.
|
||||||
|
|
||||||
|
Relative to that explicit boundary, no recurrence-specific assumption,
|
||||||
|
vacuous implication, numerical-equality inference, or hidden CAS remainder
|
||||||
|
remains.
|
||||||
|
|
||||||
|
## Defects found and repaired
|
||||||
|
|
||||||
|
| Initial defect | Why it failed | Equation-level repair |
|
||||||
|
|---|---|---|
|
||||||
|
| The deformed transfer was under-defined | Only one substituted coefficient was shown; later notation changed the meaning of the first argument | Displayed all sixteen entries of \(\mathcal M(u,x)\), defined \(M_N(x)=\mathcal M(2N+3,x)\), and displayed both official seed rows |
|
||||||
|
| Three matrix terms lost a plus sign during the first repair | The manuscript matrix then differed from the certified matrix | Restored the three sums in \(c_1,c_2,c_3\); hostile replay caught this before release |
|
||||||
|
| Ore divisions used `quo_rem` | A zero remainder was trusted rather than exhibited | Replaced every division with four direct cleared factorizations \(D_r=q_rL_+\), including the fourth companion closure |
|
||||||
|
| “Standard ascension identity” and transformed ODE were named but not derived | The coefficient mechanism was hidden | Added initial coefficient and consecutive-ratio equations; expanded the \({}_3F_2\) Euler operator explicitly |
|
||||||
|
| ODE normalization was claimed to determine the terminating \({}_4F_3\) uniquely | False: the exponent \(2n\) supplies an additional analytic branch | Replaced uniqueness with base, generic, and top coefficient induction for the actual one-step operator |
|
||||||
|
| The scalar one-step operator was not tied to the challenge matrix | Hard-coded \(d_0,d_1\) could have described a surrogate | Added horizontal reconstruction, all sixteen differential-gauge equations, and the exact matrix contraction producing \(d_0+zd_1\) |
|
||||||
|
| Only the first base component was initially checked | The actual compact seed row was not yet known to be horizontal | Added all four base-row reconstruction equations, the base terminating-operator equation, and all four base adjoint residuals |
|
||||||
|
| Two DVR-lemma hypotheses were only implicit | The induction had not displayed the \(k_{N+1}\) leading direction or \(J_N(0)e_1\ne0\) | Added both expansions and cited them explicitly at the induction step |
|
||||||
|
| A transfer norm inequality used an upper bound with exponent \(-1\) | The inequality direction was invalid for column four | Split \(j\le3\) and \(j=4\), obtaining \(31{,}250{,}000<4\cdot10^8\) |
|
||||||
|
| The maximum-modulus step omitted holomorphy of the quotient | Formal divisibility only supplied a local removable germ | Proved holomorphy on \(|x|\le1/4\), identified the only possible pole, and removed it with the \(2n\)-valuation |
|
||||||
|
| Birkhoff–Poincaré was used as a black box for three columns | It hid the exceptional hyperplane, dominant functional, decay, and denominator nonvanishing | Replaced it with an explicit backward stable-graph contraction, transverse scalar recurrence, and projective convergence estimate |
|
||||||
|
| The stable-graph statement and final projective iteration had mismatched starting quantifiers | The displayed iterations did not literally follow from the stated index ranges | Made \(\tau\) precede the construction and enlarged/redefined \(m_0,\Lambda,L_m\) before the uniform \(q_1\)-iteration |
|
||||||
|
| Irreducibility and polynomial GCD calls were used for eigenvector nonvanishing | These were unnecessary native CAS decisions | Used the coefficient-dominance homotopy, \(Q_R(1)<0\), and four positive eigenvector rewrites at the unique exterior root |
|
||||||
|
| Division in columns \(2,3,4\) preceded an eventual-nonzero proof | The displayed quotients were not yet justified | Derived the all-column asymptotic first, proved every \(w_j>0\), then established eventual \(Q_{N,j}\ne0\) before division |
|
||||||
|
| The checker could succeed while Wolfram/Sage were absent | A stored transcript was being treated as proof evidence | Made standard-library rational-polynomial verifiers mandatory; Wolfram and Sage are now optional independent cross-checks |
|
||||||
|
| Metadata called \(Q/P\) the requested orientation | The official challenge asks for \(P/Q\) | Corrected every release document to state \(P/Q\to\sqrt{10005}/\pi\) as the official orientation |
|
||||||
|
|
||||||
|
## Mandatory replay
|
||||||
|
|
||||||
|
Run:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
./run_checks.sh
|
||||||
|
```
|
||||||
|
|
||||||
|
The mandatory path executes:
|
||||||
|
|
||||||
|
1. `p28_rank_ode_bound_verifier.py`
|
||||||
|
2. `p28_convergence_constants.py`
|
||||||
|
3. `p28_standalone_equations.py`
|
||||||
|
4. `p28_dominant_product_algebra.py`
|
||||||
|
|
||||||
|
The third verifier checks:
|
||||||
|
|
||||||
|
- four cleared tail factorizations;
|
||||||
|
- lowest and generic tail coefficients;
|
||||||
|
- horizontal reconstruction;
|
||||||
|
- the terminating-operator closure;
|
||||||
|
- all sixteen differential-gauge entries;
|
||||||
|
- the authoritative matrix-to-scalar contraction;
|
||||||
|
- the base polynomial and four base-row components;
|
||||||
|
- the base terminating equation and four base adjoint residuals;
|
||||||
|
- constant, generic, and top terminating induction;
|
||||||
|
- ascension and the \({}_3F_2\) Euler equation.
|
||||||
|
|
||||||
|
The fourth verifier checks:
|
||||||
|
|
||||||
|
- \(\mathcal B_m=\mathcal S+O(m^{-1})\) entry by entry;
|
||||||
|
- \(\det(tI-\mathcal S)=Q_R(t)/R^2\);
|
||||||
|
- the exact unit-circle coefficient inequality and exterior-root sign;
|
||||||
|
- \(w(t)(tI-\mathcal S)=(Q_R(t),0,0,0)\);
|
||||||
|
- all four positive exterior-root coordinate rewrites.
|
||||||
|
|
||||||
|
Both use `fractions.Fraction` and explicit coefficient dictionaries. Neither
|
||||||
|
uses polynomial division, factorization, a simplifier, Gröbner bases,
|
||||||
|
irreducibility, GCD, a root finder, a special-function package, sampling, or
|
||||||
|
a stored transcript.
|
||||||
|
|
||||||
|
## Forbidden-shortcut search
|
||||||
|
|
||||||
|
The mandatory runner rejects these constructs in the proof path:
|
||||||
|
|
||||||
|
- `quo_rem`
|
||||||
|
- `is_irreducible`
|
||||||
|
- polynomial `gcd`
|
||||||
|
- Birkhoff/Poincaré delegation
|
||||||
|
- “standard ascension”
|
||||||
|
- ODE-normalization uniqueness
|
||||||
|
|
||||||
|
No occurrence of `native_decide`, `axiom`, `sorry`, or `admit` was found.
|
||||||
|
|
||||||
|
## Independent hostile replays
|
||||||
|
|
||||||
|
Three independent reviews targeted:
|
||||||
|
|
||||||
|
- logical validity, indexing, vacuity, and denominator domains;
|
||||||
|
- Ore/special-function and matrix-to-scalar algebra;
|
||||||
|
- convergence, stable-product asymptotics, and all-column division.
|
||||||
|
|
||||||
|
The defects in the table above were discovered during those loops. The final
|
||||||
|
Ore, asymptotic, and logic/vacuity replays returned PASS after the repairs.
|
||||||
|
Release engineering then repeats the mandatory checks in a clean extraction,
|
||||||
|
rebuilds the PDF, and performs page-by-page visual inspection.
|
||||||
|
|
@ -10,17 +10,28 @@ This package proves, for each of the four official columns,
|
||||||
=\frac{\pi}{\sqrt{10005}}.
|
=\frac{\pi}{\sqrt{10005}}.
|
||||||
\]
|
\]
|
||||||
|
|
||||||
The second display is the orientation requested in Problem 2.8.
|
The first display is the orientation requested in Problem 2.8; the second
|
||||||
|
is its reciprocal consequence.
|
||||||
|
|
||||||
## Contents
|
## Contents
|
||||||
|
|
||||||
- `solution.pdf` — the complete proof.
|
- `solution.pdf` — the complete proof.
|
||||||
- `solution.tex` — its LaTeX source.
|
- `solution.tex` — its LaTeX source.
|
||||||
- `certificates/p28_full_closure_certificate.wl` — the primary,
|
- `certificates/p28_standalone_equations.py` — mandatory, dependency-free
|
||||||
self-contained exact symbolic certificate. It proves the authoritative
|
expansion of the four cleared Ore identities, tail coefficient equations,
|
||||||
differential gauge, both hypergeometric contiguity identities, the
|
terminating base/generic/top identities, ascension, and the
|
||||||
terminating denominator formula, CM-seed annihilation, and the singular
|
hypergeometric differential equation. It uses rational coefficient
|
||||||
lattice step. No numerical sampling is used.
|
dictionaries only: no division algorithm, simplifier, factorizer, special
|
||||||
|
function library, root finder, or sample values.
|
||||||
|
- `certificates/p28_dominant_product_algebra.py` — mandatory,
|
||||||
|
dependency-free verification of the balanced limit, characteristic
|
||||||
|
polynomial, root-separation inequalities, left-eigenvector identity, and
|
||||||
|
four positive-coordinate rewrites.
|
||||||
|
- `certificates/STANDALONE_EQUATION_CERTIFICATES.md` — the same Ore and
|
||||||
|
terminating identities in a human-readable, denominator-cleared equation
|
||||||
|
sheet.
|
||||||
|
- `certificates/p28_full_closure_certificate.wl` — optional independent
|
||||||
|
symbolic cross-check of the differential gauge and closure.
|
||||||
- `certificates/p28_full_closure_certificate.PASS.txt` — transcript of a
|
- `certificates/p28_full_closure_certificate.PASS.txt` — transcript of a
|
||||||
stateless Wolfram Language run (22 exact checks plus the consolidated
|
stateless Wolfram Language run (22 exact checks plus the consolidated
|
||||||
conclusion).
|
conclusion).
|
||||||
|
|
@ -33,6 +44,8 @@ The second display is the orientation requested in Problem 2.8.
|
||||||
SageMath cross-checks.
|
SageMath cross-checks.
|
||||||
- `certificates/p28_parametric_pade_probe.py` — finite exact regression,
|
- `certificates/p28_parametric_pade_probe.py` — finite exact regression,
|
||||||
included as a diagnostic only and not used as proof.
|
included as a diagnostic only and not used as proof.
|
||||||
|
- `ADVERSARIAL_AUDIT.md` — defect ledger, repairs, replay evidence, and
|
||||||
|
the exact trust boundary.
|
||||||
|
|
||||||
## Reproduction
|
## Reproduction
|
||||||
|
|
||||||
|
|
@ -42,19 +55,20 @@ From this directory, run:
|
||||||
./run_checks.sh
|
./run_checks.sh
|
||||||
```
|
```
|
||||||
|
|
||||||
The primary symbolic check can also be run directly:
|
The mandatory proof path is Python-standard-library only. The Wolfram
|
||||||
|
cross-check can also be run directly:
|
||||||
|
|
||||||
```sh
|
```sh
|
||||||
wolframscript -file certificates/p28_full_closure_certificate.wl
|
wolframscript -file certificates/p28_full_closure_certificate.wl
|
||||||
```
|
```
|
||||||
|
|
||||||
It should print 22 exact-check lines beginning with `PASS:`, followed by the
|
The Python checks use only the standard library:
|
||||||
consolidated certificate conclusion. The Python checks use only the standard
|
|
||||||
library:
|
|
||||||
|
|
||||||
```sh
|
```sh
|
||||||
python3 certificates/p28_rank_ode_bound_verifier.py
|
python3 certificates/p28_rank_ode_bound_verifier.py
|
||||||
python3 certificates/p28_convergence_constants.py
|
python3 certificates/p28_convergence_constants.py
|
||||||
|
python3 certificates/p28_standalone_equations.py
|
||||||
|
python3 certificates/p28_dominant_product_algebra.py
|
||||||
```
|
```
|
||||||
|
|
||||||
For the independent SageMath checks:
|
For the independent SageMath checks:
|
||||||
|
|
@ -70,3 +84,13 @@ To rebuild the manuscript:
|
||||||
```sh
|
```sh
|
||||||
latexmk -pdf solution.tex
|
latexmk -pdf solution.tex
|
||||||
```
|
```
|
||||||
|
|
||||||
|
## Trust boundary
|
||||||
|
|
||||||
|
No numerical enclosure is used to infer equality. The recurrence proof is
|
||||||
|
expanded into explicit equations and an elementary stable-graph contraction.
|
||||||
|
The sole imported mathematical theorem is the classical Chudnovsky formula,
|
||||||
|
identified precisely in `solution.tex` with a reference to a complete
|
||||||
|
modular/CM derivation. Thus the package is self-contained relative to that
|
||||||
|
published theorem; it does not claim to reconstruct the entire theory of the
|
||||||
|
Chudnovsky formula from first principles.
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,383 @@
|
||||||
|
# Standalone Equation Certificates for Problem 2.8
|
||||||
|
|
||||||
|
This sheet replaces every Ore-division or “the remainder simplifies” claim
|
||||||
|
in the proof. Each displayed assertion is an equality in a rational-function
|
||||||
|
field. Multiplying by the listed denominator produces a polynomial whose
|
||||||
|
coefficients are all zero.
|
||||||
|
|
||||||
|
The companion program `p28_standalone_equations.py` recreates these checks
|
||||||
|
with sparse dictionaries over `fractions.Fraction`. It implements addition,
|
||||||
|
multiplication, integer powers, and formal differentiation only. It does not
|
||||||
|
call a division algorithm, factorizer, simplifier, Gröbner basis, special
|
||||||
|
function library, root finder, or numerical sampler.
|
||||||
|
|
||||||
|
## 1. Input matrix
|
||||||
|
|
||||||
|
Let \(u\) and \(x\) be indeterminates, \(r=x^{-1}\), and
|
||||||
|
\(\omega=u(3u-2)(3u+2)\). Define
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
a_1={}&r(144u^5-288u^4+144u^3)
|
||||||
|
-99u^5+333u^4-229u^3-114u^2+40u+64,\\
|
||||||
|
a_2={}&r(432u^4-864u^3+432u^2)
|
||||||
|
-243u^4+909u^3-868u^2-80u+272,\\
|
||||||
|
a_3={}&r(432u^3-864u^2+432u)
|
||||||
|
-153u^3+648u^2-860u+360,\\
|
||||||
|
a_4={}&144r(u-1)^2,\\
|
||||||
|
b_1={}&-144ru^3+9u^4+63u^3+158u^2+168u+64,\\
|
||||||
|
b_2={}&216ru^2+36u^3-189u^2-316u-168,\\
|
||||||
|
b_3={}&108ru+54u^2-189u-158,\\
|
||||||
|
c_1={}&-288r^2u^3+
|
||||||
|
r(54u^4+378u^3+948u^2+1008u+384)\\
|
||||||
|
&+18u^5+45u^4-251u^3-1086u^2-1384u-576,\\
|
||||||
|
c_2={}&-432r^2u^2+
|
||||||
|
r(153u^4-657u^3+1292u^2+2064u+1072)\\
|
||||||
|
&-72u^4+702u^3-1069u^2-2508u-1512,\\
|
||||||
|
c_3={}&-216r^2u+
|
||||||
|
r(180u^3-891u^2+1450u+1116)\\
|
||||||
|
&-108u^3+864u^2-1385u-1422,\\
|
||||||
|
c_4={}&-4r^2+r(6u^2-33u+\tfrac{536}{9})-4u^2+32u-63.
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
|
Then
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal M(u,x)=
|
||||||
|
\begin{pmatrix}
|
||||||
|
a_1/\omega&a_2/\omega&a_3/\omega&a_4/\omega\\
|
||||||
|
-u^3&-3u^2&-3u&-1\\
|
||||||
|
xb_1/144&-xb_2/72&-xb_3/36&x(-2r-(2u-7))/2\\
|
||||||
|
x^2c_1/288&x^2c_2/144&x^2c_3/72&x^2c_4/4
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
For the recurrence, \(u=2N+3\), so \(u\ge3\).
|
||||||
|
|
||||||
|
## 2. Four Ore identities without division
|
||||||
|
|
||||||
|
Put
|
||||||
|
|
||||||
|
\[
|
||||||
|
m=\frac{u-1}{2},\qquad
|
||||||
|
P_i(t)=\sum_{s=0}^{3}\mathcal M(u,x)_{i+1,s+1}t^s,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal TQ=(1-x)x\partial_xQ+(t+1)Q
|
||||||
|
\]
|
||||||
|
|
||||||
|
and
|
||||||
|
|
||||||
|
\[
|
||||||
|
L_+(t)=(1-x)t(t+u)^3+
|
||||||
|
x(t+m+1)(t+m+\tfrac76)(t+m+\tfrac32)(t+m+\tfrac{11}{6}).
|
||||||
|
\]
|
||||||
|
|
||||||
|
Define
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
\ell_0={}&(u-1)u(3u-2)(3u+2)x/144,\\
|
||||||
|
\ell_1={}&[-576+864u-432u^2+72u^3
|
||||||
|
+(580-872u+405u^2-36u^3)x]/72,\\
|
||||||
|
\ell_2={}&[432-432u+108u^2
|
||||||
|
+(-436+405u-54u^2)x]/36,\\
|
||||||
|
\ell_3={}&(-12+6u+11x-2ux)/2,\\
|
||||||
|
q_3={}&-36+(536-297u+54u^2)x
|
||||||
|
+(-567+288u-36u^2)x^2.
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
|
The complete equation set is
|
||||||
|
|
||||||
|
\[
|
||||||
|
u(3u-2)(3u+2)x(\mathcal TP_0-P_1)
|
||||||
|
-144(u-1)^2L_+=0,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal TP_1-P_2+L_+=0,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
2(\mathcal TP_2-P_3)-(-2+7x-2ux)L_+=0,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
36(\mathcal TP_3+\ell_3P_3+\ell_2P_2+\ell_1P_1+\ell_0P_0)
|
||||||
|
-q_3L_+=0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
These are the quotient-and-zero-remainder claims written as four direct
|
||||||
|
factorizations. No quotient or remainder operation is needed.
|
||||||
|
|
||||||
|
## 3. Lowest and generic tail coefficients
|
||||||
|
|
||||||
|
Set
|
||||||
|
|
||||||
|
\[
|
||||||
|
A(t)=\frac{144(u-1)^2(t+u)^3}{u(3u-2)(3u+2)},\qquad
|
||||||
|
B(t)=P_0(t)-\frac{A(t)}x,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\varrho=-\frac{(3u-2)(3u+2)}{144(u-1)^2u^2},
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\chi_j=
|
||||||
|
\frac{(m+j)(m+\frac16+j)(m+\frac12+j)(m+\frac56+j)}
|
||||||
|
{m(m+\frac16)(m+\frac12)(m+\frac56)}
|
||||||
|
\left(\frac{2m(2m+1)}{(2m+j)(2m+j+1)}\right)^3,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\psi_j=
|
||||||
|
\frac{(m+j)(m+\frac16+j)(m+\frac12+j)(m+\frac56+j)}
|
||||||
|
{(2m+j)^3(j+1)}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The two identities are
|
||||||
|
|
||||||
|
\[
|
||||||
|
\varrho[-A(0)]-1=0
|
||||||
|
\]
|
||||||
|
|
||||||
|
and, for \(j\ge1\),
|
||||||
|
|
||||||
|
\[
|
||||||
|
\varrho\left[
|
||||||
|
-A(j)\chi_j+
|
||||||
|
\frac{(A(j-1)+B(j-1))\chi_{j-1}}{\psi_{j-1}}
|
||||||
|
\right]-1=0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
For \(u=2N+3\ge3\), the integer-dependent denominator factors are nonzero.
|
||||||
|
Factors of \(x\) are cleared before coefficient comparison; no conclusion
|
||||||
|
is obtained by evaluating a rational expression at \(x=0\).
|
||||||
|
|
||||||
|
## 4. Terminating denominator induction
|
||||||
|
|
||||||
|
For \(n\ge1\), define
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal L_n(t)=t(t+2n-1)^3
|
||||||
|
-z(t+n)(t+n+\tfrac16)(t+n+\tfrac12)(t+n+\tfrac56)
|
||||||
|
=\sum_{j=0}^4c_jt^j
|
||||||
|
\]
|
||||||
|
|
||||||
|
and, for operator polynomials with coefficients on the left,
|
||||||
|
|
||||||
|
\[
|
||||||
|
\Theta Q=z\partial_zQ+tQ.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The horizontal row is reconstructed by
|
||||||
|
|
||||||
|
\[
|
||||||
|
\pi_0=1,\qquad
|
||||||
|
\pi_3=\frac{c_4}{c_0}t,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\pi_2=\frac{c_3}{c_4}\pi_3-\Theta\pi_3,\qquad
|
||||||
|
\pi_1=\frac{c_2}{c_4}\pi_3-\Theta\pi_2.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Its final equation is
|
||||||
|
|
||||||
|
\[
|
||||||
|
\Theta\pi_1+1-\frac{c_1}{c_4}\pi_3
|
||||||
|
+\frac{72}{n(2n+1)(6n+1)(6n+5)z}
|
||||||
|
\left[
|
||||||
|
t(t-2n)^3
|
||||||
|
-z(t-n)(t-n-\tfrac16)(t-n-\tfrac12)(t-n-\tfrac56)
|
||||||
|
\right]=0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Let
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal C_n(z)=
|
||||||
|
\begin{pmatrix}
|
||||||
|
0&1&0&0\\
|
||||||
|
0&0&1&0\\
|
||||||
|
0&0&0&1\\
|
||||||
|
-c_0/c_4&-c_1/c_4&-c_2/c_4&-c_3/c_4
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The complete differential-gauge equation is
|
||||||
|
|
||||||
|
\[
|
||||||
|
\mathcal C_n[-z\mathcal M(2n+1,-z/(1-z))]
|
||||||
|
-\theta[-z\mathcal M(2n+1,-z/(1-z))]
|
||||||
|
-[-z\mathcal M(2n+1,-z/(1-z))]\mathcal C_{n+1}=0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The checker cross-multiplies all sixteen entries independently.
|
||||||
|
|
||||||
|
The exact matrix-to-scalar bridge is
|
||||||
|
|
||||||
|
\[
|
||||||
|
\sum_{r=0}^3\pi_r(t)
|
||||||
|
\left[-z\mathcal M(2n+1,-z/(1-z))\right]_{r+1,1}
|
||||||
|
-d_0(t)-zd_1(t)=0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The checker expands all five reconstruction/bridge equations before it
|
||||||
|
checks any hypergeometric coefficient identity. Thus \(d_0+zd_1\) is tied
|
||||||
|
to the displayed challenge matrix and is not a guessed surrogate.
|
||||||
|
|
||||||
|
Now define
|
||||||
|
|
||||||
|
\[
|
||||||
|
\nu_n=\frac{576n^2(2n+1)^2}{(6n+1)(6n+5)},
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
d_0(t)=
|
||||||
|
\frac{72(2n+1)^2(2n-t)^3}{n(6n+1)(6n+5)}
|
||||||
|
\]
|
||||||
|
|
||||||
|
and
|
||||||
|
|
||||||
|
\[
|
||||||
|
d_1(t)=-\frac{P(n,t)}{n(2n+1)(6n+1)(6n+5)},
|
||||||
|
\]
|
||||||
|
|
||||||
|
where
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
P(n,t)={}&-5n-76n^2+1404n^3+4360n^4+4320n^5+1440n^6\\
|
||||||
|
&+(5+127n-1760n^2-6536n^3-7632n^4-3024n^5)t\\
|
||||||
|
&+(-51+659n+3086n^2+4500n^3+2232n^4)t^2\\
|
||||||
|
&+(-72-432n-864n^2-576n^3)t^3.
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
|
Let
|
||||||
|
|
||||||
|
\[
|
||||||
|
h_{n,k}=
|
||||||
|
\frac{(-n)_k(-n-\frac16)_k(-n-\frac12)_k(-n-\frac56)_k}
|
||||||
|
{(1-2n)_k^3k!},
|
||||||
|
\qquad0\le k\le n.
|
||||||
|
\]
|
||||||
|
|
||||||
|
The induction is exactly:
|
||||||
|
|
||||||
|
\[
|
||||||
|
d_0(0)-\nu_n=0,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
d_0(k)+d_1(k-1)\frac{h_{n,k-1}}{h_{n,k}}
|
||||||
|
-\nu_n\frac{h_{n+1,k}}{h_{n,k}}=0
|
||||||
|
\qquad(1\le k\le n),
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
d_1(n)+
|
||||||
|
\nu_n\frac{(n+\frac76)(n+\frac32)(n+\frac{11}{6})}
|
||||||
|
{8(2n+1)^3}=0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Together with
|
||||||
|
|
||||||
|
\[
|
||||||
|
q_0(x)=18/x+159/4,\qquad Q_0(x)=xq_0(x),
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
p_1(z)=(1-z)Q_0(-z/(1-z))
|
||||||
|
=18(1-\tfrac{77}{24}z),\qquad
|
||||||
|
p_{n+1}=(d_0(\theta)+zd_1(\theta))p_n,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
-zC(-z/(1-z))
|
||||||
|
=\left.(\pi_0(\theta)p_1,\pi_1(\theta)p_1,
|
||||||
|
\pi_2(\theta)p_1,\pi_3(\theta)p_1)\right|_{n=1},
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\left[
|
||||||
|
\theta(\theta-2)^3
|
||||||
|
-z(\theta-1)(\theta-\tfrac76)
|
||||||
|
(\theta-\tfrac32)(\theta-\tfrac{11}{6})
|
||||||
|
\right]p_1=0,
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\theta[-zC(-z/(1-z))]
|
||||||
|
+[-zC(-z/(1-z))]\mathcal C_1=0,
|
||||||
|
\]
|
||||||
|
|
||||||
|
and
|
||||||
|
|
||||||
|
\[
|
||||||
|
\deg((d_0(\theta)+zd_1(\theta))p_n)\le n+1,
|
||||||
|
\]
|
||||||
|
|
||||||
|
these equations prove every coefficient, including the top boundary. The
|
||||||
|
free \(z^{2n}\) branch of the fourth-order differential equation is never
|
||||||
|
invoked.
|
||||||
|
|
||||||
|
For \(n\ge1\) and \(1\le k\le n\), all integer- and
|
||||||
|
Pochhammer-dependent factors in the coefficient identities are nonzero.
|
||||||
|
The \(z^{-1}\) factors in the horizontal reconstruction are handled in
|
||||||
|
\(\mathbb Q(n,z)(t)\) and cross-multiplied first; the checked base functions
|
||||||
|
have removable limits at \(z=0\).
|
||||||
|
|
||||||
|
## 5. Short hypergeometric identities
|
||||||
|
|
||||||
|
For
|
||||||
|
|
||||||
|
\[
|
||||||
|
y(z)=\sum_{k\ge0}
|
||||||
|
\frac{(\frac16)_k(\frac12)_k(\frac56)_k}{(k!)^3}z^k,
|
||||||
|
\]
|
||||||
|
|
||||||
|
the coefficient ratio is
|
||||||
|
|
||||||
|
\[
|
||||||
|
\frac{[z^{k+1}]y}{[z^k]y}
|
||||||
|
=\frac{(k+\frac16)(k+\frac12)(k+\frac56)}{(k+1)^3}.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Therefore
|
||||||
|
|
||||||
|
\[
|
||||||
|
y-1=\frac5{72}z\,
|
||||||
|
{}_4F_3\left(
|
||||||
|
\begin{matrix}1,\frac76,\frac32,\frac{11}{6}\\2,2,2\end{matrix};z
|
||||||
|
\right)
|
||||||
|
\]
|
||||||
|
|
||||||
|
and coefficient comparison gives
|
||||||
|
|
||||||
|
\[
|
||||||
|
\left[\theta^3-
|
||||||
|
z(\theta+\tfrac16)(\theta+\tfrac12)(\theta+\tfrac56)\right]y=0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
With \(z=-x/(1-x)\), this expands to
|
||||||
|
|
||||||
|
\[
|
||||||
|
72\theta^3y+108x\theta^2y+46x\theta y+5xy=0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
## 6. Replay
|
||||||
|
|
||||||
|
From the submission directory:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
python3 certificates/p28_standalone_equations.py
|
||||||
|
```
|
||||||
|
|
||||||
|
Success means every denominator-cleared numerator has an empty coefficient
|
||||||
|
dictionary. A stored transcript is not consulted.
|
||||||
|
|
@ -8,13 +8,12 @@ It certifies the algebraic part of the cyclic-frame lemma:
|
||||||
* the exact balanced limit S;
|
* the exact balanced limit S;
|
||||||
* charpoly(S)=Q_R/R^2;
|
* charpoly(S)=Q_R/R^2;
|
||||||
* an explicit left eigenvector w_rho;
|
* an explicit left eigenvector w_rho;
|
||||||
* every coordinate of w_rho is nonzero; and
|
* every coordinate of w_rho is positive at the exterior root; and
|
||||||
* the limiting cyclic frame [e1,S e1,S^2 e1,S^3 e1] is invertible.
|
* the limiting cyclic frame [e1,S e1,S^2 e1,S^3 e1] is invertible.
|
||||||
|
|
||||||
The analytic input is the scalar e1-column Birkhoff asymptotic proved in the
|
The analytic stable-graph contraction is proved equation by equation in the
|
||||||
main solution. The accompanying report derives the other three columns by
|
main solution. This file is only an independent exact algebra cross-check;
|
||||||
the exact finite frame, without invoking a new matrix-product asymptotic
|
it performs no irreducibility, polynomial-GCD, or numerical root decision.
|
||||||
theorem.
|
|
||||||
"""
|
"""
|
||||||
from sage.all import *
|
from sage.all import *
|
||||||
|
|
||||||
|
|
@ -101,18 +100,18 @@ Q = (
|
||||||
+ 1
|
+ 1
|
||||||
)
|
)
|
||||||
assert Rx(S.charpoly("x")) == Q/R^2
|
assert Rx(S.charpoly("x")) == Q/R^2
|
||||||
assert Q.is_irreducible()
|
|
||||||
assert gcd(Q, Q.derivative()) == 1
|
|
||||||
|
|
||||||
# On |x|=1 the cubic term strictly dominates all other terms. Rouché's
|
# On |x|=1 the cubic term strictly dominates all other terms. The homotopy
|
||||||
# theorem therefore puts exactly three roots in the open unit disk and one
|
# written in the manuscript therefore has no boundary zero and keeps winding
|
||||||
# outside it.
|
# number three.
|
||||||
rouche_margin = (
|
rouche_margin = (
|
||||||
(64*R^3-56*R^2-4)
|
(64*R^3-56*R^2-4)
|
||||||
- (R^2 + (48*R^2-262*R+220) + (12*R-8) + 1)
|
- (R^2 + (48*R^2-262*R+220) + (12*R-8) + 1)
|
||||||
)
|
)
|
||||||
assert rouche_margin == 64*R^3-105*R^2+250*R-217
|
assert rouche_margin == 64*R^3-105*R^2+250*R-217
|
||||||
assert rouche_margin > 0
|
assert rouche_margin > 0
|
||||||
|
assert Q(1) == -(64*R^3-105*R^2+274*R-233)
|
||||||
|
assert Q(1) < 0
|
||||||
|
|
||||||
# First row of R^2 adj(xI-S). At Q(x)=0 it is a left eigenvector.
|
# First row of R^2 adj(xI-S). At Q(x)=0 it is a left eigenvector.
|
||||||
w = vector(Rx, [
|
w = vector(Rx, [
|
||||||
|
|
@ -125,9 +124,17 @@ w = vector(Rx, [
|
||||||
])
|
])
|
||||||
assert w * (x*identity_matrix(Rx, 4) - S.change_ring(Rx)) == vector(Rx, [Q, 0, 0, 0])
|
assert w * (x*identity_matrix(Rx, 4) - S.change_ring(Rx)) == vector(Rx, [Q, 0, 0, 0])
|
||||||
|
|
||||||
# Since Q is irreducible of degree four and every w_j has degree < 4,
|
# These are the positive rewrites used at the unique exterior root rho>1.
|
||||||
# gcd(Q,w_j)=1 proves w_j(rho) != 0 for every root rho of Q.
|
w_positive = vector(Rx, [
|
||||||
assert [gcd(Q, z) for z in w] == [Rx(1)]*4
|
R*x*(R*x^2-7) + 12*R^2*x^2 + 4*x^2 + 44*x + 10,
|
||||||
|
2*(R^2*x*((48*R-27)*x-28)
|
||||||
|
+ (194*R-108)*x + 40*R-23),
|
||||||
|
R^2*x*((48*R-17)*x-8)
|
||||||
|
+ (198*R-68)*x + 71*R-32,
|
||||||
|
2*R*(8 + (17+3*R)*x + 4*R^2*x^2),
|
||||||
|
])
|
||||||
|
assert w_positive == w
|
||||||
|
assert R > 7
|
||||||
|
|
||||||
e1 = vector(QQ, [1, 0, 0, 0])
|
e1 = vector(QQ, [1, 0, 0, 0])
|
||||||
C = matrix(QQ, 4, 4)
|
C = matrix(QQ, 4, 4)
|
||||||
|
|
@ -138,8 +145,7 @@ assert C.det() == detC_expected
|
||||||
assert C.det() != 0
|
assert C.det() != 0
|
||||||
|
|
||||||
print("PASS: exact balanced limit and characteristic quartic")
|
print("PASS: exact balanced limit and characteristic quartic")
|
||||||
print("PASS: Rouché separation gives three roots inside |x|<1")
|
print("PASS: boundary-free homotopy has winding number three")
|
||||||
print("PASS: explicit left eigenvector has four nonvanishing coordinates")
|
print("PASS: explicit exterior-root eigenvector has four positive coordinates")
|
||||||
print("PASS: limiting e1 cyclic frame is invertible")
|
print("PASS: limiting e1 cyclic frame is invertible")
|
||||||
print("CONCLUSION (using the certified scalar e1 Birkhoff asymptotic):")
|
print("The analytic stable-graph contraction is proved in solution.tex.")
|
||||||
print(" lim_N P_(N,j)/Q_(N,j) is independent of j=1,2,3,4")
|
|
||||||
|
|
|
||||||
|
|
@ -7,6 +7,9 @@ known:
|
||||||
|
|
||||||
c_N/c_(N-1) >= 29*N^2,
|
c_N/c_(N-1) >= 29*N^2,
|
||||||
sum k^3*(1/3)^k < 5,
|
sum k^3*(1/3)^k < 5,
|
||||||
|
||E_0||_infinity < 6000,
|
||||||
|
||M_0||_infinity < 10^7,
|
||||||
|
||B_m||_infinity < 4*10^8 with the negative-exponent case separated,
|
||||||
beta(x_official) < 4*10^-19 < 1.
|
beta(x_official) < 4*10^-19 < 1.
|
||||||
"""
|
"""
|
||||||
|
|
||||||
|
|
@ -77,6 +80,42 @@ for row, caps in zip(raw_estimates, raw_caps):
|
||||||
assert cap < 10_000
|
assert cap < 10_000
|
||||||
|
|
||||||
|
|
||||||
|
# On |x|=1/4 the compact row has the following component bounds.
|
||||||
|
c_bounds = [
|
||||||
|
18*4 + F(159, 4),
|
||||||
|
54*4 + F(131, 2),
|
||||||
|
54*4 + 27,
|
||||||
|
18*4,
|
||||||
|
]
|
||||||
|
pascal_row_sum = 8
|
||||||
|
e0_bound = 5*sum(c_bounds) + F(5, 4)*pascal_row_sum
|
||||||
|
assert e0_bound < 6000
|
||||||
|
|
||||||
|
|
||||||
|
# The entrywise estimate at u=3 bounds M_0. Indices are one-based, so the
|
||||||
|
# powers are u^(i+2-j). Negative exponents are kept as exact fractions.
|
||||||
|
m0_row_bounds = [
|
||||||
|
10_000*sum(F(3)**(i+2-j) for j in range(1, 5))
|
||||||
|
for i in range(1, 5)
|
||||||
|
]
|
||||||
|
assert max(m0_row_bounds) < 10_000_000
|
||||||
|
|
||||||
|
|
||||||
|
# For m>=1, u=2m+3 gives u/m<=5 and
|
||||||
|
#
|
||||||
|
# 2 <= u/(m+1) <= 5/2.
|
||||||
|
#
|
||||||
|
# The exponent 3-j is negative at j=4, so that column must use the lower
|
||||||
|
# bound 2, not the upper bound 5/2. Summing the four column factors gives
|
||||||
|
# 25/4 + 5/2 + 1 + 1/2 = 41/4.
|
||||||
|
balanced_row_cap = 10_000 * 5**3 * (
|
||||||
|
F(25, 4) + F(5, 2) + 1 + F(1, 2)
|
||||||
|
)
|
||||||
|
assert balanced_row_cap == 12_812_500
|
||||||
|
assert 4*10_000*5**3*F(25, 4) == 31_250_000
|
||||||
|
assert 31_250_000 < TRANSFER_BOUND
|
||||||
|
|
||||||
|
|
||||||
beta = (
|
beta = (
|
||||||
F(TRANSFER_BOUND, 29)
|
F(TRANSFER_BOUND, 29)
|
||||||
* X**2
|
* X**2
|
||||||
|
|
@ -90,5 +129,8 @@ assert beta < 1
|
||||||
print("PASS: exact fixed-x convergence constants")
|
print("PASS: exact fixed-x convergence constants")
|
||||||
print("sum k^3/3^k =", theta3_sum)
|
print("sum k^3/3^k =", theta3_sum)
|
||||||
print("entrywise transfer constants < 10000")
|
print("entrywise transfer constants < 10000")
|
||||||
|
print("||E_0||_infinity bound =", e0_bound, "< 6000")
|
||||||
|
print("||M_0||_infinity bound =", max(m0_row_bounds), "< 10^7")
|
||||||
|
print("||B_m||_infinity bound < 31250000 < 4e8")
|
||||||
print("beta =", beta)
|
print("beta =", beta)
|
||||||
print("beta < 4e-19 < 1")
|
print("beta < 4e-19 < 1")
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,363 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
"""Dependency-free algebra for the explicit dominant-product argument.
|
||||||
|
|
||||||
|
The script uses exact rational arithmetic and elementary polynomial expansion
|
||||||
|
only. It verifies:
|
||||||
|
|
||||||
|
* the balanced transfer limit ``B_n = S + O(1/n)`` from the displayed matrix;
|
||||||
|
* ``det(t I-S)=Q_R(t)/R^2``;
|
||||||
|
* the strict unit-circle coefficient dominance;
|
||||||
|
* the explicit polynomial left-eigenvector identity; and
|
||||||
|
* rewrites making all four dominant eigenvector coordinates positive at the
|
||||||
|
unique real exterior root.
|
||||||
|
|
||||||
|
It performs no irreducibility test, polynomial GCD, root finding, or numerical
|
||||||
|
sampling.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from fractions import Fraction as F
|
||||||
|
from itertools import permutations
|
||||||
|
|
||||||
|
|
||||||
|
def trim(poly):
|
||||||
|
poly = [F(value) for value in poly]
|
||||||
|
while len(poly) > 1 and poly[-1] == 0:
|
||||||
|
poly.pop()
|
||||||
|
return poly
|
||||||
|
|
||||||
|
|
||||||
|
def padd(left, right):
|
||||||
|
size = max(len(left), len(right))
|
||||||
|
return trim([
|
||||||
|
(left[index] if index < len(left) else F(0))
|
||||||
|
+ (right[index] if index < len(right) else F(0))
|
||||||
|
for index in range(size)
|
||||||
|
])
|
||||||
|
|
||||||
|
|
||||||
|
def pneg(poly):
|
||||||
|
return trim([-value for value in poly])
|
||||||
|
|
||||||
|
|
||||||
|
def psub(left, right):
|
||||||
|
return padd(left, pneg(right))
|
||||||
|
|
||||||
|
|
||||||
|
def pmul(left, right):
|
||||||
|
result = [F(0)] * (len(left) + len(right) - 1)
|
||||||
|
for i, left_value in enumerate(left):
|
||||||
|
for j, right_value in enumerate(right):
|
||||||
|
result[i+j] += left_value * right_value
|
||||||
|
return trim(result)
|
||||||
|
|
||||||
|
|
||||||
|
def pscale(poly, scalar):
|
||||||
|
scalar = F(scalar)
|
||||||
|
return trim([scalar*value for value in poly])
|
||||||
|
|
||||||
|
|
||||||
|
def ppow(poly, exponent):
|
||||||
|
result = [F(1)]
|
||||||
|
base = trim(poly)
|
||||||
|
power = exponent
|
||||||
|
while power:
|
||||||
|
if power & 1:
|
||||||
|
result = pmul(result, base)
|
||||||
|
base = pmul(base, base)
|
||||||
|
power //= 2
|
||||||
|
return result
|
||||||
|
|
||||||
|
|
||||||
|
def pconstant(value):
|
||||||
|
return [F(value)]
|
||||||
|
|
||||||
|
|
||||||
|
N = [F(0), F(1)]
|
||||||
|
ONE = [F(1)]
|
||||||
|
N_PLUS_ONE = [F(1), F(1)]
|
||||||
|
|
||||||
|
|
||||||
|
class RatPoly:
|
||||||
|
"""Unreduced rational function in n over QQ."""
|
||||||
|
|
||||||
|
def __init__(self, numerator=ONE, denominator=ONE):
|
||||||
|
self.numerator = trim(numerator)
|
||||||
|
self.denominator = trim(denominator)
|
||||||
|
if self.denominator == [F(0)]:
|
||||||
|
raise ZeroDivisionError
|
||||||
|
|
||||||
|
def __add__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return RatPoly(
|
||||||
|
padd(
|
||||||
|
pmul(self.numerator, other.denominator),
|
||||||
|
pmul(other.numerator, self.denominator),
|
||||||
|
),
|
||||||
|
pmul(self.denominator, other.denominator),
|
||||||
|
)
|
||||||
|
|
||||||
|
__radd__ = __add__
|
||||||
|
|
||||||
|
def __neg__(self):
|
||||||
|
return RatPoly(pneg(self.numerator), self.denominator)
|
||||||
|
|
||||||
|
def __sub__(self, other):
|
||||||
|
return self + (-as_rat(other))
|
||||||
|
|
||||||
|
def __rsub__(self, other):
|
||||||
|
return as_rat(other) - self
|
||||||
|
|
||||||
|
def __mul__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return RatPoly(
|
||||||
|
pmul(self.numerator, other.numerator),
|
||||||
|
pmul(self.denominator, other.denominator),
|
||||||
|
)
|
||||||
|
|
||||||
|
__rmul__ = __mul__
|
||||||
|
|
||||||
|
def __truediv__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return RatPoly(
|
||||||
|
pmul(self.numerator, other.denominator),
|
||||||
|
pmul(self.denominator, other.numerator),
|
||||||
|
)
|
||||||
|
|
||||||
|
def __rtruediv__(self, other):
|
||||||
|
return as_rat(other) / self
|
||||||
|
|
||||||
|
def __pow__(self, exponent):
|
||||||
|
if exponent >= 0:
|
||||||
|
return RatPoly(
|
||||||
|
ppow(self.numerator, exponent),
|
||||||
|
ppow(self.denominator, exponent),
|
||||||
|
)
|
||||||
|
return RatPoly(
|
||||||
|
ppow(self.denominator, -exponent),
|
||||||
|
ppow(self.numerator, -exponent),
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def as_rat(value):
|
||||||
|
if isinstance(value, RatPoly):
|
||||||
|
return value
|
||||||
|
if isinstance(value, list):
|
||||||
|
return RatPoly(value)
|
||||||
|
return RatPoly(pconstant(value))
|
||||||
|
|
||||||
|
|
||||||
|
def limit_at_infinity(value):
|
||||||
|
value = as_rat(value)
|
||||||
|
numerator_degree = len(value.numerator)-1
|
||||||
|
denominator_degree = len(value.denominator)-1
|
||||||
|
if numerator_degree < denominator_degree:
|
||||||
|
return F(0)
|
||||||
|
if numerator_degree == denominator_degree:
|
||||||
|
return value.numerator[-1] / value.denominator[-1]
|
||||||
|
raise AssertionError("balanced entry diverges")
|
||||||
|
|
||||||
|
|
||||||
|
def vanishes_as_inverse_n(value):
|
||||||
|
value = as_rat(value)
|
||||||
|
if value.numerator == [F(0)]:
|
||||||
|
return True
|
||||||
|
return len(value.denominator)-len(value.numerator) >= 1
|
||||||
|
|
||||||
|
|
||||||
|
def matrix_multiply(left, right):
|
||||||
|
return [
|
||||||
|
[
|
||||||
|
sum(left[i][k]*right[k][j] for k in range(len(right)))
|
||||||
|
for j in range(len(right[0]))
|
||||||
|
]
|
||||||
|
for i in range(len(left))
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
def permutation_sign(permutation):
|
||||||
|
inversions = sum(
|
||||||
|
permutation[i] > permutation[j]
|
||||||
|
for i in range(len(permutation))
|
||||||
|
for j in range(i+1, len(permutation))
|
||||||
|
)
|
||||||
|
return -1 if inversions % 2 else 1
|
||||||
|
|
||||||
|
|
||||||
|
def determinant_polynomial(matrix):
|
||||||
|
size = len(matrix)
|
||||||
|
result = [F(0)]
|
||||||
|
for permutation in permutations(range(size)):
|
||||||
|
term = [F(permutation_sign(permutation))]
|
||||||
|
for row, column in enumerate(permutation):
|
||||||
|
term = pmul(term, matrix[row][column])
|
||||||
|
result = padd(result, term)
|
||||||
|
return trim(result)
|
||||||
|
|
||||||
|
|
||||||
|
R = F(151931373056001)
|
||||||
|
u = RatPoly([F(3), F(2)])
|
||||||
|
w = u*(3*u-2)*(3*u+2)
|
||||||
|
|
||||||
|
a1 = R*(144*u**5-288*u**4+144*u**3) + (
|
||||||
|
-99*u**5+333*u**4-229*u**3-114*u**2+40*u+64
|
||||||
|
)
|
||||||
|
a2 = R*(432*u**4-864*u**3+432*u**2) + (
|
||||||
|
-243*u**4+909*u**3-868*u**2-80*u+272
|
||||||
|
)
|
||||||
|
a3 = R*(432*u**3-864*u**2+432*u) + (
|
||||||
|
-153*u**3+648*u**2-860*u+360
|
||||||
|
)
|
||||||
|
a4 = R*144*(u-1)**2
|
||||||
|
|
||||||
|
b1 = R*(-144*u**3) + (9*u**4+63*u**3+158*u**2+168*u+64)
|
||||||
|
b2 = R*(216*u**2) + (36*u**3-189*u**2-316*u-168)
|
||||||
|
b3 = R*(108*u) + (54*u**2-189*u-158)
|
||||||
|
|
||||||
|
c1 = (
|
||||||
|
R**2*(-288*u**3)
|
||||||
|
+ R*(54*u**4+378*u**3+948*u**2+1008*u+384)
|
||||||
|
+ (18*u**5+45*u**4-251*u**3-1086*u**2-1384*u-576)
|
||||||
|
)
|
||||||
|
c2 = (
|
||||||
|
R**2*(-432*u**2)
|
||||||
|
+ R*(153*u**4-657*u**3+1292*u**2+2064*u+1072)
|
||||||
|
+ (-72*u**4+702*u**3-1069*u**2-2508*u-1512)
|
||||||
|
)
|
||||||
|
c3 = (
|
||||||
|
R**2*(-216*u)
|
||||||
|
+ R*(180*u**3-891*u**2+1450*u+1116)
|
||||||
|
+ (-108*u**3+864*u**2-1385*u-1422)
|
||||||
|
)
|
||||||
|
c4 = (
|
||||||
|
R**2*(-4)
|
||||||
|
+ R*(6*u**2-33*u+58+F(14, 9))
|
||||||
|
+ (-4*u**2+32*u-63)
|
||||||
|
)
|
||||||
|
|
||||||
|
M = [
|
||||||
|
[a1/w, a2/w, a3/w, a4/w],
|
||||||
|
[-u**3, -3*u**2, -3*u, -1],
|
||||||
|
[b1/(144*R), -b2/(72*R), -b3/(36*R), (-2*R-(2*u-7))/(2*R)],
|
||||||
|
[c1/(288*R**2), c2/(144*R**2), c3/(72*R**2), c4/(4*R**2)],
|
||||||
|
]
|
||||||
|
|
||||||
|
B = [
|
||||||
|
[
|
||||||
|
M[i][j]
|
||||||
|
* RatPoly(ppow(N_PLUS_ONE, j))
|
||||||
|
/ RatPoly(pmul(ppow(N, i), ppow(N_PLUS_ONE, 2)))
|
||||||
|
for j in range(4)
|
||||||
|
]
|
||||||
|
for i in range(4)
|
||||||
|
]
|
||||||
|
|
||||||
|
S = [
|
||||||
|
[64*R-44, 96*R-54, 48*R-17, 8*R],
|
||||||
|
[-8, -12, -6, -1],
|
||||||
|
[1/R, -4/R, -6/R, -2/R],
|
||||||
|
[
|
||||||
|
2/R**2,
|
||||||
|
(17*R-8)/R**2,
|
||||||
|
4*(5*R-3)/R**2,
|
||||||
|
(6*R-4)/R**2,
|
||||||
|
],
|
||||||
|
]
|
||||||
|
|
||||||
|
for row in range(4):
|
||||||
|
for column in range(4):
|
||||||
|
assert limit_at_infinity(B[row][column]) == S[row][column]
|
||||||
|
assert vanishes_as_inverse_n(B[row][column]-S[row][column])
|
||||||
|
print("PASS: balanced transfer is S+O(1/n) entry by entry")
|
||||||
|
|
||||||
|
|
||||||
|
# Characteristic polynomial det(tI-S).
|
||||||
|
t_poly = [F(0), F(1)]
|
||||||
|
char_matrix = [
|
||||||
|
[
|
||||||
|
psub(t_poly, pconstant(S[i][j]))
|
||||||
|
if i == j else pconstant(-S[i][j])
|
||||||
|
for j in range(4)
|
||||||
|
]
|
||||||
|
for i in range(4)
|
||||||
|
]
|
||||||
|
characteristic = determinant_polynomial(char_matrix)
|
||||||
|
Q = [
|
||||||
|
F(1),
|
||||||
|
-(12*R-8),
|
||||||
|
48*R**2-262*R+220,
|
||||||
|
-(64*R**3-56*R**2-4),
|
||||||
|
R**2,
|
||||||
|
]
|
||||||
|
assert characteristic == pscale(Q, F(1, R**2))
|
||||||
|
print("PASS: det(tI-S)=Q_R(t)/R^2")
|
||||||
|
|
||||||
|
|
||||||
|
margin = 64*R**3-105*R**2+250*R-217
|
||||||
|
assert margin > 0
|
||||||
|
q_at_one = sum(Q)
|
||||||
|
assert q_at_one == -(64*R**3-105*R**2+274*R-233)
|
||||||
|
assert q_at_one < 0
|
||||||
|
print("PASS: exact unit-circle dominance and positive exterior-root sign")
|
||||||
|
|
||||||
|
|
||||||
|
w_left = [
|
||||||
|
[10, 44-7*R, 4+12*R**2, R**2],
|
||||||
|
[2*(-23+40*R), 2*(-108+194*R-28*R**2), 2*(-27*R**2+48*R**3)],
|
||||||
|
[-32+71*R, -68+198*R-8*R**2, -17*R**2+48*R**3],
|
||||||
|
[16*R, 2*R*(17+3*R), 8*R**3],
|
||||||
|
]
|
||||||
|
|
||||||
|
residual = []
|
||||||
|
for column in range(4):
|
||||||
|
value = [F(0)]
|
||||||
|
for row in range(4):
|
||||||
|
factor = (
|
||||||
|
psub(t_poly, pconstant(S[row][column]))
|
||||||
|
if row == column else pconstant(-S[row][column])
|
||||||
|
)
|
||||||
|
value = padd(value, pmul(w_left[row], factor))
|
||||||
|
residual.append(value)
|
||||||
|
assert residual == [Q, [F(0)], [F(0)], [F(0)]]
|
||||||
|
print("PASS: w(t)(tI-S)=(Q_R(t),0,0,0)")
|
||||||
|
|
||||||
|
|
||||||
|
# Exact rewrites used to prove positivity for R>7 and t=rho>1.
|
||||||
|
w1_rewrite = padd(
|
||||||
|
pmul(pscale(t_poly, R), psub(pscale(ppow(t_poly, 2), R), [F(7)])),
|
||||||
|
padd(
|
||||||
|
pscale(ppow(t_poly, 2), 12*R**2+4),
|
||||||
|
padd(pscale(t_poly, 44), [F(10)]),
|
||||||
|
),
|
||||||
|
)
|
||||||
|
w2_half_rewrite = padd(
|
||||||
|
pmul(
|
||||||
|
pscale(t_poly, R**2),
|
||||||
|
psub(pscale(t_poly, 48*R-27), [F(28)]),
|
||||||
|
),
|
||||||
|
padd(pscale(t_poly, 194*R-108), [40*R-23]),
|
||||||
|
)
|
||||||
|
w3_rewrite = padd(
|
||||||
|
pmul(
|
||||||
|
pscale(t_poly, R**2),
|
||||||
|
psub(pscale(t_poly, 48*R-17), [F(8)]),
|
||||||
|
),
|
||||||
|
padd(pscale(t_poly, 198*R-68), [71*R-32]),
|
||||||
|
)
|
||||||
|
w4_rewrite = pscale(
|
||||||
|
padd([F(8)], padd(pscale(t_poly, 17+3*R), pscale(ppow(t_poly, 2), 4*R**2))),
|
||||||
|
2*R,
|
||||||
|
)
|
||||||
|
|
||||||
|
assert w1_rewrite == w_left[0]
|
||||||
|
assert pscale(w2_half_rewrite, 2) == w_left[1]
|
||||||
|
assert w3_rewrite == w_left[2]
|
||||||
|
assert w4_rewrite == w_left[3]
|
||||||
|
assert R > 7
|
||||||
|
assert 48*R-55 > 0
|
||||||
|
assert 48*R-25 > 0
|
||||||
|
assert 194*R-108 > 0
|
||||||
|
assert 198*R-68 > 0
|
||||||
|
assert 40*R-23 > 0
|
||||||
|
assert 71*R-32 > 0
|
||||||
|
print("PASS: all four exterior-root eigenvector coordinates are positive")
|
||||||
|
print("No irreducibility test, GCD, root finder, or numerical sample was used.")
|
||||||
|
|
@ -6,7 +6,7 @@ During evaluation of In[1]:= PASS: the scalar step operator has only z-degrees z
|
||||||
During evaluation of In[1]:= PASS: constant-term normalization recurrence
|
During evaluation of In[1]:= PASS: constant-term normalization recurrence
|
||||||
During evaluation of In[1]:= PASS: generic all-n terminating contiguity coefficient
|
During evaluation of In[1]:= PASS: generic all-n terminating contiguity coefficient
|
||||||
During evaluation of In[1]:= PASS: terminating top-coefficient boundary
|
During evaluation of In[1]:= PASS: terminating top-coefficient boundary
|
||||||
During evaluation of In[1]:= PASS: tail gauge selects the exponent-zero analytic solution
|
During evaluation of In[1]:= PASS: tail gauge satisfies the explicit row-zero coefficient identities
|
||||||
During evaluation of In[1]:= PASS: nonterminating kernel normalization and exact contiguity
|
During evaluation of In[1]:= PASS: nonterminating kernel normalization and exact contiguity
|
||||||
During evaluation of In[1]:= PASS: binomial jet converts K_0 to the CM first jet
|
During evaluation of In[1]:= PASS: binomial jet converts K_0 to the CM first jet
|
||||||
During evaluation of In[1]:= PASS: compact denominator row reduces to the 3F2 operator
|
During evaluation of In[1]:= PASS: compact denominator row reduces to the 3F2 operator
|
||||||
|
|
@ -16,10 +16,10 @@ During evaluation of In[1]:= PASS: regularized determinant has exact x-adic orde
|
||||||
During evaluation of In[1]:= PASS: Smith valuations are exactly (0,1,1,1)
|
During evaluation of In[1]:= PASS: Smith valuations are exactly (0,1,1,1)
|
||||||
During evaluation of In[1]:= PASS: regular annihilator transfer gains one power of x
|
During evaluation of In[1]:= PASS: regular annihilator transfer gains one power of x
|
||||||
During evaluation of In[1]:= PASS: balanced characteristic polynomial is the authoritative quartic
|
During evaluation of In[1]:= PASS: balanced characteristic polynomial is the authoritative quartic
|
||||||
During evaluation of In[1]:= PASS: characteristic quartic is irreducible
|
During evaluation of In[1]:= PASS: exterior characteristic root is positive
|
||||||
During evaluation of In[1]:= PASS: Rouche separation has three roots in the unit disk
|
During evaluation of In[1]:= PASS: unit-circle homotopy has winding number three
|
||||||
During evaluation of In[1]:= PASS: limiting first-coordinate cyclic frame is invertible
|
During evaluation of In[1]:= PASS: limiting first-coordinate cyclic frame is invertible
|
||||||
During evaluation of In[1]:= PASS: dominant left eigenvector has four nonzero coordinates
|
During evaluation of In[1]:= PASS: dominant left eigenvector has four positive exterior-root rewrites
|
||||||
During evaluation of In[1]:= PASS: consolidated exact hypergeometric-closure certificate
|
During evaluation of In[1]:= PASS: consolidated exact hypergeometric-closure certificate
|
||||||
During evaluation of In[1]:= M_N K_(N+1)=K_N with kappa_(n+1)/kappa_n=-(6n+1)(6n+5)/(576n^2(2n+1)^2)
|
During evaluation of In[1]:= M_N K_(N+1)=K_N with kappa_(n+1)/kappa_n=-(6n+1)(6n+5)/(576n^2(2n+1)^2)
|
||||||
During evaluation of In[1]:= P_n(z)[[1]]/a_n = 4F3(-n,-n-1/6,-n-1/2,-n-5/6;1-2n,1-2n,1-2n;z)
|
During evaluation of In[1]:= P_n(z)[[1]]/a_n = 4F3(-n,-n-1/6,-n-1/2,-n-5/6;1-2n,1-2n,1-2n;z)
|
||||||
|
|
|
||||||
|
|
@ -295,7 +295,7 @@ tailColumnAtOrigin = Map[
|
||||||
Limit[gauge[[All,1]],z->0]
|
Limit[gauge[[All,1]],z->0]
|
||||||
];
|
];
|
||||||
check[
|
check[
|
||||||
"tail gauge selects the exponent-zero analytic solution",
|
"tail gauge satisfies the explicit row-zero coefficient identities",
|
||||||
tailColumnAtOrigin === {normalizationRatio,0,0,0}
|
tailColumnAtOrigin === {normalizationRatio,0,0,0}
|
||||||
];
|
];
|
||||||
|
|
||||||
|
|
@ -441,14 +441,16 @@ check[
|
||||||
] === 0
|
] === 0
|
||||||
];
|
];
|
||||||
check[
|
check[
|
||||||
"characteristic quartic is irreducible",
|
"exterior characteristic root is positive",
|
||||||
TrueQ[IrreduciblePolynomialQ[qQuartic[lam]]]
|
qQuartic[1] ===
|
||||||
|
-(64rOfficial^3-105rOfficial^2+274rOfficial-233)
|
||||||
|
&& qQuartic[1] < 0
|
||||||
];
|
];
|
||||||
|
|
||||||
roucheMargin =
|
roucheMargin =
|
||||||
64rOfficial^3-105rOfficial^2+250rOfficial-217;
|
64rOfficial^3-105rOfficial^2+250rOfficial-217;
|
||||||
check[
|
check[
|
||||||
"Rouche separation has three roots in the unit disk",
|
"unit-circle homotopy has winding number three",
|
||||||
roucheMargin > 0
|
roucheMargin > 0
|
||||||
];
|
];
|
||||||
|
|
||||||
|
|
@ -487,12 +489,21 @@ leftResidual = Map[
|
||||||
]
|
]
|
||||||
];
|
];
|
||||||
check[
|
check[
|
||||||
"dominant left eigenvector has four nonzero coordinates",
|
"dominant left eigenvector has four positive exterior-root rewrites",
|
||||||
leftResidual === ConstantArray[0,4]
|
leftResidual === ConstantArray[0,4]
|
||||||
&& And@@Map[
|
&& Expand[wLeft[[1]]
|
||||||
Exponent[PolynomialGCD[qQuartic[lam],#],lam] === 0&,
|
-(rOfficial lam(rOfficial lam^2-7)
|
||||||
wLeft
|
+12rOfficial^2 lam^2+4lam^2+44lam+10)] === 0
|
||||||
]
|
&& Expand[wLeft[[2]]/2
|
||||||
|
-(rOfficial^2 lam((48rOfficial-27)lam-28)
|
||||||
|
+(194rOfficial-108)lam+40rOfficial-23)] === 0
|
||||||
|
&& Expand[wLeft[[3]]
|
||||||
|
-(rOfficial^2 lam((48rOfficial-17)lam-8)
|
||||||
|
+(198rOfficial-68)lam+71rOfficial-32)] === 0
|
||||||
|
&& Expand[wLeft[[4]]
|
||||||
|
-2rOfficial(8+(17+3rOfficial)lam
|
||||||
|
+4rOfficial^2 lam^2)] === 0
|
||||||
|
&& rOfficial > 7
|
||||||
];
|
];
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -121,8 +121,8 @@ assert P[1] == -(t+u)**3
|
||||||
|
|
||||||
|
|
||||||
# Once row 0 gives F_N=P_0(t)F_{N+1}, the other rows must be its first,
|
# Once row 0 gives F_N=P_0(t)F_{N+1}, the other rows must be its first,
|
||||||
# second and third delta_N derivatives. The following exact congruences
|
# second and third delta_N derivatives. The following exact factorizations
|
||||||
# prove precisely that, modulo the shifted 4F3 equation L(t)F=0.
|
# prove this directly. No polynomial division or remainder command is used.
|
||||||
expected_quotients = [
|
expected_quotients = [
|
||||||
144*(u-1)**2 / (u*(3*u-2)*(3*u+2)*x),
|
144*(u-1)**2 / (u*(3*u-2)*(3*u+2)*x),
|
||||||
-1,
|
-1,
|
||||||
|
|
@ -131,9 +131,40 @@ expected_quotients = [
|
||||||
|
|
||||||
for r in range(3):
|
for r in range(3):
|
||||||
difference = T(shifted_derivative(P[r]) - P[r+1])
|
difference = T(shifted_derivative(P[r]) - P[r+1])
|
||||||
quotient, remainder = difference.quo_rem(L)
|
quotient = T(expected_quotients[r])
|
||||||
assert remainder == 0
|
assert difference == quotient*L
|
||||||
assert K(quotient) == K(expected_quotients[r])
|
|
||||||
|
|
||||||
|
# The fourth companion closure is the row omitted by a mere three-row
|
||||||
|
# derivative check. The preceding tail F_N satisfies
|
||||||
|
#
|
||||||
|
# L_minus(s)=s^4+l3*s^3+l2*s^2+l1*s+l0,
|
||||||
|
#
|
||||||
|
# with s=delta_N. Hence delta_N^4 F_N is the displayed linear combination
|
||||||
|
# of the first four jet entries. The last identity below completes the
|
||||||
|
# four-equation differential gauge.
|
||||||
|
l0 = (u-1)*u*(3*u-2)*(3*u+2)*x/144
|
||||||
|
l1 = (
|
||||||
|
-576 + 864*u - 432*u**2 + 72*u**3
|
||||||
|
+ 580*x - 872*u*x + 405*u**2*x - 36*u**3*x
|
||||||
|
) / 72
|
||||||
|
l2 = (
|
||||||
|
432 - 432*u + 108*u**2
|
||||||
|
- 436*x + 405*u*x - 54*u**2*x
|
||||||
|
) / 36
|
||||||
|
l3 = (-12 + 6*u + 11*x - 2*u*x) / 2
|
||||||
|
|
||||||
|
difference4 = T(
|
||||||
|
shifted_derivative(P[3])
|
||||||
|
+ l3*P[3] + l2*P[2] + l1*P[1] + l0*P[0]
|
||||||
|
)
|
||||||
|
quotient4 = T(
|
||||||
|
(
|
||||||
|
-36 + 536*x - 297*u*x + 54*u**2*x
|
||||||
|
- 567*x**2 + 288*u*x**2 - 36*u**2*x**2
|
||||||
|
) / 36
|
||||||
|
)
|
||||||
|
assert difference4 == quotient4*L
|
||||||
|
|
||||||
|
|
||||||
# It remains to certify row 0, i.e. F_N=P_0(t)F_{N+1}.
|
# It remains to certify row 0, i.e. F_N=P_0(t)F_{N+1}.
|
||||||
|
|
|
||||||
|
|
@ -7,11 +7,12 @@ the pieces that do not require a hypergeometric CAS:
|
||||||
* the rank-one x=0 factorization of H M_N;
|
* the rank-one x=0 factorization of H M_N;
|
||||||
* the rank-one x^(-1) coefficient of M_N and c_N normalization;
|
* the rank-one x^(-1) coefficient of M_N and c_N normalization;
|
||||||
* the compact-row/ODE cancellation;
|
* the compact-row/ODE cancellation;
|
||||||
* the exact Rouché separation of the characteristic quartic; and
|
* the exact unit-circle coefficient separation of the characteristic
|
||||||
|
quartic; and
|
||||||
* the explicit fixed-point convergence constants.
|
* the explicit fixed-point convergence constants.
|
||||||
|
|
||||||
The two hypergeometric all-N contiguity identities are checked separately by
|
The hypergeometric all-N identities and matrix-to-scalar bridge are checked
|
||||||
the Sage and Wolfram certificates named in TAIL_LATTICE_CLOSURE_REPORT.md.
|
by the dependency-free ``p28_standalone_equations.py`` verifier.
|
||||||
"""
|
"""
|
||||||
|
|
||||||
from fractions import Fraction as Q
|
from fractions import Fraction as Q
|
||||||
|
|
@ -83,7 +84,12 @@ assert official_j0_times_w == rank_one_j0_times_w
|
||||||
|
|
||||||
# Clear w in lim x M_N. Only the first row is nonzero.
|
# Clear w in lim x M_N. Only the first row is nonzero.
|
||||||
official_mminus1_times_w = [
|
official_mminus1_times_w = [
|
||||||
rank_one_j0_times_w[0],
|
[
|
||||||
|
poly([(5, 144), (4, -288), (3, 144)]),
|
||||||
|
poly([(4, 432), (3, -864), (2, 432)]),
|
||||||
|
poly([(3, 432), (2, -864), (1, 432)]),
|
||||||
|
scale(power(u_minus_1, 2), 144),
|
||||||
|
],
|
||||||
[{}, {}, {}, {}],
|
[{}, {}, {}, {}],
|
||||||
[{}, {}, {}, {}],
|
[{}, {}, {}, {}],
|
||||||
[{}, {}, {}, {}],
|
[{}, {}, {}, {}],
|
||||||
|
|
@ -97,13 +103,32 @@ expected_mminus1_times_w = [
|
||||||
assert official_mminus1_times_w == expected_mminus1_times_w
|
assert official_mminus1_times_w == expected_mminus1_times_w
|
||||||
|
|
||||||
|
|
||||||
# The first tail coefficient is
|
# The first tail coefficient, derived independently from the four upper and
|
||||||
|
# three lower parameters, is
|
||||||
#
|
#
|
||||||
# c = u(3u-2)(3u+2)/(144(u-1)^2),
|
# c = u(3u-2)(3u+2)/(144(u-1)^2),
|
||||||
#
|
#
|
||||||
# so the leading direction of H k_N is (1,-c,-c,-c), exactly the image
|
# so the leading direction of H k_N is (1,-c,-c,-c), exactly the image
|
||||||
# direction of J(0). Clearing the denominator gives the identity below.
|
# direction of J(0). Clear denominators in
|
||||||
assert w == mul(u, mul(three_u_minus_2, three_u_plus_2))
|
#
|
||||||
|
# ((u-1)/2)((u-1)/2+1/6)((u-1)/2+1/2)((u-1)/2+5/6)/(u-1)^3 = c.
|
||||||
|
n_tail = scale(u_minus_1, Q(1, 2))
|
||||||
|
hyper_first_numerator = mul(
|
||||||
|
mul(n_tail, add(n_tail, poly([(0, Q(1, 6))]))),
|
||||||
|
mul(
|
||||||
|
add(n_tail, poly([(0, Q(1, 2))])),
|
||||||
|
add(n_tail, poly([(0, Q(5, 6))])),
|
||||||
|
),
|
||||||
|
)
|
||||||
|
hyper_first_denominator = power(u_minus_1, 3)
|
||||||
|
closed_first_numerator = mul(u, mul(three_u_minus_2, three_u_plus_2))
|
||||||
|
closed_first_denominator = scale(power(u_minus_1, 2), 144)
|
||||||
|
assert mul(hyper_first_numerator, closed_first_denominator) == mul(
|
||||||
|
closed_first_numerator, hyper_first_denominator
|
||||||
|
)
|
||||||
|
|
||||||
|
# Together with the independently entered rank-one first row above, this
|
||||||
|
# identifies its scalar \(144(u-1)^2/w\) as the reciprocal of c.
|
||||||
|
|
||||||
|
|
||||||
# Transformed ODE:
|
# Transformed ODE:
|
||||||
|
|
@ -182,5 +207,5 @@ assert beta < Q(4, 10**19) < 1
|
||||||
|
|
||||||
print("PASS: exact rank-one transfer factorization")
|
print("PASS: exact rank-one transfer factorization")
|
||||||
print("PASS: exact transformed ODE and compact-row cancellation")
|
print("PASS: exact transformed ODE and compact-row cancellation")
|
||||||
print("PASS: exact Rouché separation of the characteristic roots")
|
print("PASS: exact unit-circle coefficient separation of the characteristic roots")
|
||||||
print("PASS: exact convergence constants; beta =", beta)
|
print("PASS: exact convergence constants; beta =", beta)
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,743 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
"""Transparent exact equation checks for Ramanujan Challenge 2.8.
|
||||||
|
|
||||||
|
This verifier deliberately implements only:
|
||||||
|
|
||||||
|
* sparse multivariate polynomials over ``fractions.Fraction``;
|
||||||
|
* rational functions represented by numerator/denominator pairs;
|
||||||
|
* addition, multiplication, integer powers, and formal differentiation.
|
||||||
|
|
||||||
|
It does not call polynomial division, factorization, simplification, Gröbner
|
||||||
|
bases, a special-function library, a root finder, or numerical sampling.
|
||||||
|
Every obligation is entered as a displayed denominator-cleared identity and
|
||||||
|
passes only when every coefficient of the expanded numerator is exactly zero.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from fractions import Fraction as F
|
||||||
|
|
||||||
|
|
||||||
|
VARIABLES = ("u", "x", "t", "j", "n", "k", "z")
|
||||||
|
NVARS = len(VARIABLES)
|
||||||
|
INDEX = {name: position for position, name in enumerate(VARIABLES)}
|
||||||
|
ZERO_EXPONENT = (0,) * NVARS
|
||||||
|
|
||||||
|
|
||||||
|
class Poly:
|
||||||
|
"""Sparse polynomial over QQ in the fixed variables above."""
|
||||||
|
|
||||||
|
def __init__(self, terms=None):
|
||||||
|
combined = {}
|
||||||
|
for exponent, coefficient in (terms or {}).items():
|
||||||
|
coefficient = F(coefficient)
|
||||||
|
if coefficient:
|
||||||
|
combined[tuple(exponent)] = (
|
||||||
|
combined.get(tuple(exponent), F(0)) + coefficient
|
||||||
|
)
|
||||||
|
self.terms = {
|
||||||
|
exponent: coefficient
|
||||||
|
for exponent, coefficient in combined.items()
|
||||||
|
if coefficient
|
||||||
|
}
|
||||||
|
|
||||||
|
@staticmethod
|
||||||
|
def constant(value):
|
||||||
|
value = F(value)
|
||||||
|
return Poly({ZERO_EXPONENT: value}) if value else Poly()
|
||||||
|
|
||||||
|
@staticmethod
|
||||||
|
def variable(name):
|
||||||
|
exponent = [0] * NVARS
|
||||||
|
exponent[INDEX[name]] = 1
|
||||||
|
return Poly({tuple(exponent): F(1)})
|
||||||
|
|
||||||
|
def __add__(self, other):
|
||||||
|
other = as_poly(other)
|
||||||
|
terms = dict(self.terms)
|
||||||
|
for exponent, coefficient in other.terms.items():
|
||||||
|
terms[exponent] = terms.get(exponent, F(0)) + coefficient
|
||||||
|
return Poly(terms)
|
||||||
|
|
||||||
|
__radd__ = __add__
|
||||||
|
|
||||||
|
def __neg__(self):
|
||||||
|
return Poly({
|
||||||
|
exponent: -coefficient
|
||||||
|
for exponent, coefficient in self.terms.items()
|
||||||
|
})
|
||||||
|
|
||||||
|
def __sub__(self, other):
|
||||||
|
return self + (-as_poly(other))
|
||||||
|
|
||||||
|
def __rsub__(self, other):
|
||||||
|
return as_poly(other) - self
|
||||||
|
|
||||||
|
def __mul__(self, other):
|
||||||
|
other = as_poly(other)
|
||||||
|
terms = {}
|
||||||
|
for left_exp, left_coefficient in self.terms.items():
|
||||||
|
for right_exp, right_coefficient in other.terms.items():
|
||||||
|
exponent = tuple(
|
||||||
|
left_exp[position] + right_exp[position]
|
||||||
|
for position in range(NVARS)
|
||||||
|
)
|
||||||
|
terms[exponent] = (
|
||||||
|
terms.get(exponent, F(0))
|
||||||
|
+ left_coefficient * right_coefficient
|
||||||
|
)
|
||||||
|
return Poly(terms)
|
||||||
|
|
||||||
|
__rmul__ = __mul__
|
||||||
|
|
||||||
|
def __pow__(self, exponent):
|
||||||
|
if exponent < 0:
|
||||||
|
raise ValueError("Poly powers must be nonnegative")
|
||||||
|
result = Poly.constant(1)
|
||||||
|
base = self
|
||||||
|
power = exponent
|
||||||
|
while power:
|
||||||
|
if power & 1:
|
||||||
|
result = result * base
|
||||||
|
base = base * base
|
||||||
|
power //= 2
|
||||||
|
return result
|
||||||
|
|
||||||
|
def derivative(self, name):
|
||||||
|
position = INDEX[name]
|
||||||
|
terms = {}
|
||||||
|
for exponent, coefficient in self.terms.items():
|
||||||
|
degree = exponent[position]
|
||||||
|
if degree:
|
||||||
|
new_exponent = list(exponent)
|
||||||
|
new_exponent[position] -= 1
|
||||||
|
terms[tuple(new_exponent)] = coefficient * degree
|
||||||
|
return Poly(terms)
|
||||||
|
|
||||||
|
def is_zero(self):
|
||||||
|
return not self.terms
|
||||||
|
|
||||||
|
|
||||||
|
def as_poly(value):
|
||||||
|
if isinstance(value, Poly):
|
||||||
|
return value
|
||||||
|
return Poly.constant(value)
|
||||||
|
|
||||||
|
|
||||||
|
class Rat:
|
||||||
|
"""Unreduced rational function over the sparse polynomial ring."""
|
||||||
|
|
||||||
|
def __init__(self, numerator=0, denominator=1):
|
||||||
|
self.numerator = as_poly(numerator)
|
||||||
|
self.denominator = as_poly(denominator)
|
||||||
|
if self.denominator.is_zero():
|
||||||
|
raise ZeroDivisionError("zero polynomial denominator")
|
||||||
|
|
||||||
|
def __add__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.denominator
|
||||||
|
+ other.numerator * self.denominator,
|
||||||
|
self.denominator * other.denominator,
|
||||||
|
)
|
||||||
|
|
||||||
|
__radd__ = __add__
|
||||||
|
|
||||||
|
def __neg__(self):
|
||||||
|
return Rat(-self.numerator, self.denominator)
|
||||||
|
|
||||||
|
def __sub__(self, other):
|
||||||
|
return self + (-as_rat(other))
|
||||||
|
|
||||||
|
def __rsub__(self, other):
|
||||||
|
return as_rat(other) - self
|
||||||
|
|
||||||
|
def __mul__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.numerator,
|
||||||
|
self.denominator * other.denominator,
|
||||||
|
)
|
||||||
|
|
||||||
|
__rmul__ = __mul__
|
||||||
|
|
||||||
|
def __truediv__(self, other):
|
||||||
|
other = as_rat(other)
|
||||||
|
if other.numerator.is_zero():
|
||||||
|
raise ZeroDivisionError("division by the zero rational function")
|
||||||
|
return Rat(
|
||||||
|
self.numerator * other.denominator,
|
||||||
|
self.denominator * other.numerator,
|
||||||
|
)
|
||||||
|
|
||||||
|
def __rtruediv__(self, other):
|
||||||
|
return as_rat(other) / self
|
||||||
|
|
||||||
|
def __pow__(self, exponent):
|
||||||
|
if exponent >= 0:
|
||||||
|
return Rat(
|
||||||
|
self.numerator ** exponent,
|
||||||
|
self.denominator ** exponent,
|
||||||
|
)
|
||||||
|
return Rat(
|
||||||
|
self.denominator ** (-exponent),
|
||||||
|
self.numerator ** (-exponent),
|
||||||
|
)
|
||||||
|
|
||||||
|
def derivative(self, name):
|
||||||
|
return Rat(
|
||||||
|
self.numerator.derivative(name) * self.denominator
|
||||||
|
- self.numerator * self.denominator.derivative(name),
|
||||||
|
self.denominator ** 2,
|
||||||
|
)
|
||||||
|
|
||||||
|
def is_zero(self):
|
||||||
|
return self.numerator.is_zero()
|
||||||
|
|
||||||
|
|
||||||
|
def as_rat(value):
|
||||||
|
if isinstance(value, Rat):
|
||||||
|
return value
|
||||||
|
if isinstance(value, Poly):
|
||||||
|
return Rat(value)
|
||||||
|
return Rat(F(value))
|
||||||
|
|
||||||
|
|
||||||
|
def check_zero(label, expression):
|
||||||
|
expression = as_rat(expression)
|
||||||
|
assert expression.is_zero(), label
|
||||||
|
print("PASS:", label)
|
||||||
|
|
||||||
|
|
||||||
|
def matrix_multiply(left, right):
|
||||||
|
return [
|
||||||
|
[
|
||||||
|
sum(
|
||||||
|
left[row][middle] * right[middle][column]
|
||||||
|
for middle in range(len(right))
|
||||||
|
)
|
||||||
|
for column in range(len(right[0]))
|
||||||
|
]
|
||||||
|
for row in range(len(left))
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
def check_zero_matrix(label, matrix):
|
||||||
|
assert all(
|
||||||
|
as_rat(entry).is_zero()
|
||||||
|
for row in matrix
|
||||||
|
for entry in row
|
||||||
|
), label
|
||||||
|
print("PASS:", label)
|
||||||
|
|
||||||
|
|
||||||
|
u, x, t, j, n, k, z = [
|
||||||
|
Rat(Poly.variable(name)) for name in VARIABLES
|
||||||
|
]
|
||||||
|
SYMBOLS = dict(zip(VARIABLES, (u, x, t, j, n, k, z)))
|
||||||
|
|
||||||
|
|
||||||
|
def substitute_polynomial(polynomial, replacements):
|
||||||
|
"""Evaluate a sparse polynomial at rational-function replacements."""
|
||||||
|
result = Rat(0)
|
||||||
|
for exponent, coefficient in polynomial.terms.items():
|
||||||
|
term = Rat(coefficient)
|
||||||
|
for position, degree in enumerate(exponent):
|
||||||
|
if degree:
|
||||||
|
name = VARIABLES[position]
|
||||||
|
term *= replacements.get(name, SYMBOLS[name]) ** degree
|
||||||
|
result += term
|
||||||
|
return result
|
||||||
|
|
||||||
|
|
||||||
|
def substitute_rational(expression, replacements):
|
||||||
|
"""Evaluate an unreduced rational function by cross multiplication."""
|
||||||
|
expression = as_rat(expression)
|
||||||
|
return (
|
||||||
|
substitute_polynomial(expression.numerator, replacements)
|
||||||
|
/ substitute_polynomial(expression.denominator, replacements)
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def polynomial_coefficient(expression, name, degree):
|
||||||
|
"""Extract one coefficient when the denominator omits ``name``."""
|
||||||
|
expression = as_rat(expression)
|
||||||
|
position = INDEX[name]
|
||||||
|
assert all(
|
||||||
|
exponent[position] == 0
|
||||||
|
for exponent in expression.denominator.terms
|
||||||
|
)
|
||||||
|
terms = {}
|
||||||
|
for exponent, coefficient in expression.numerator.terms.items():
|
||||||
|
if exponent[position] == degree:
|
||||||
|
reduced = list(exponent)
|
||||||
|
reduced[position] = 0
|
||||||
|
terms[tuple(reduced)] = coefficient
|
||||||
|
return Rat(Poly(terms), expression.denominator)
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# Four standalone tail/Ore factorizations.
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
m = (u - 1) / 2
|
||||||
|
R = 1 / x
|
||||||
|
w = u * (3*u - 2) * (3*u + 2)
|
||||||
|
|
||||||
|
a1 = (
|
||||||
|
R * (144*u**5 - 288*u**4 + 144*u**3)
|
||||||
|
+ (-99*u**5 + 333*u**4 - 229*u**3 - 114*u**2 + 40*u + 64)
|
||||||
|
)
|
||||||
|
a2 = (
|
||||||
|
R * (432*u**4 - 864*u**3 + 432*u**2)
|
||||||
|
+ (-243*u**4 + 909*u**3 - 868*u**2 - 80*u + 272)
|
||||||
|
)
|
||||||
|
a3 = (
|
||||||
|
R * (432*u**3 - 864*u**2 + 432*u)
|
||||||
|
+ (-153*u**3 + 648*u**2 - 860*u + 360)
|
||||||
|
)
|
||||||
|
a4 = R * 144 * (u - 1)**2
|
||||||
|
|
||||||
|
b1 = R * (-144*u**3) + (9*u**4 + 63*u**3 + 158*u**2 + 168*u + 64)
|
||||||
|
b2 = R * (216*u**2) + (36*u**3 - 189*u**2 - 316*u - 168)
|
||||||
|
b3 = R * (108*u) + (54*u**2 - 189*u - 158)
|
||||||
|
|
||||||
|
c1 = (
|
||||||
|
R**2 * (-288*u**3)
|
||||||
|
+ R * (54*u**4 + 378*u**3 + 948*u**2 + 1008*u + 384)
|
||||||
|
+ (18*u**5 + 45*u**4 - 251*u**3 - 1086*u**2 - 1384*u - 576)
|
||||||
|
)
|
||||||
|
c2 = (
|
||||||
|
R**2 * (-432*u**2)
|
||||||
|
+ R * (153*u**4 - 657*u**3 + 1292*u**2 + 2064*u + 1072)
|
||||||
|
+ (-72*u**4 + 702*u**3 - 1069*u**2 - 2508*u - 1512)
|
||||||
|
)
|
||||||
|
c3 = (
|
||||||
|
R**2 * (-216*u)
|
||||||
|
+ R * (180*u**3 - 891*u**2 + 1450*u + 1116)
|
||||||
|
+ (-108*u**3 + 864*u**2 - 1385*u - 1422)
|
||||||
|
)
|
||||||
|
c4 = (
|
||||||
|
R**2 * (-4)
|
||||||
|
+ R * (6*u**2 - 33*u + 58 + F(14, 9))
|
||||||
|
+ (-4*u**2 + 32*u - 63)
|
||||||
|
)
|
||||||
|
|
||||||
|
matrix = [
|
||||||
|
[a1/w, a2/w, a3/w, a4/w],
|
||||||
|
[-u**3, -3*u**2, -3*u, -1],
|
||||||
|
[x*b1/144, -x*b2/72, -x*b3/36, x*(-2*R-(2*u-7))/2],
|
||||||
|
[x**2*c1/288, x**2*c2/144, x**2*c3/72, x**2*c4/4],
|
||||||
|
]
|
||||||
|
|
||||||
|
# The first column of the z-coordinate gauge
|
||||||
|
# -z M(2n+1,-z/(1-z)).
|
||||||
|
# It will be contracted below with four explicitly reconstructed horizontal
|
||||||
|
# row components to verify that the displayed d0+z*d1 step is induced by the
|
||||||
|
# authoritative matrix, rather than merely guessed and checked afterward.
|
||||||
|
matrix_nz = [
|
||||||
|
[
|
||||||
|
substitute_rational(
|
||||||
|
entry,
|
||||||
|
{"u": 2*n+1, "x": -z/(1-z)},
|
||||||
|
)
|
||||||
|
for entry in row
|
||||||
|
]
|
||||||
|
for row in matrix
|
||||||
|
]
|
||||||
|
gauge_first_column = [-z*matrix_nz[row][0] for row in range(4)]
|
||||||
|
|
||||||
|
|
||||||
|
def p_row(row, argument=t):
|
||||||
|
return sum(matrix[row][column] * argument**column for column in range(4))
|
||||||
|
|
||||||
|
|
||||||
|
P = [p_row(row) for row in range(4)]
|
||||||
|
|
||||||
|
|
||||||
|
def shifted_derivative(expression):
|
||||||
|
return (1-x)*x*expression.derivative("x") + (t+1)*expression
|
||||||
|
|
||||||
|
|
||||||
|
L_plus = (
|
||||||
|
(1-x)*t*(t+u)**3
|
||||||
|
+ x*(t+m+1)*(t+m+F(7, 6))*(t+m+F(3, 2))*(t+m+F(11, 6))
|
||||||
|
)
|
||||||
|
|
||||||
|
l0 = (u-1)*u*(3*u-2)*(3*u+2)*x/144
|
||||||
|
l1 = (
|
||||||
|
-576 + 864*u - 432*u**2 + 72*u**3
|
||||||
|
+ 580*x - 872*u*x + 405*u**2*x - 36*u**3*x
|
||||||
|
) / 72
|
||||||
|
l2 = (
|
||||||
|
432 - 432*u + 108*u**2
|
||||||
|
- 436*x + 405*u*x - 54*u**2*x
|
||||||
|
) / 36
|
||||||
|
l3 = (-12 + 6*u + 11*x - 2*u*x) / 2
|
||||||
|
|
||||||
|
D0 = shifted_derivative(P[0]) - P[1]
|
||||||
|
D1 = shifted_derivative(P[1]) - P[2]
|
||||||
|
D2 = shifted_derivative(P[2]) - P[3]
|
||||||
|
D3 = shifted_derivative(P[3]) + l3*P[3] + l2*P[2] + l1*P[1] + l0*P[0]
|
||||||
|
|
||||||
|
q3_numerator = (
|
||||||
|
-36 + 536*x - 297*u*x + 54*u**2*x
|
||||||
|
- 567*x**2 + 288*u*x**2 - 36*u**2*x**2
|
||||||
|
)
|
||||||
|
|
||||||
|
check_zero(
|
||||||
|
"cleared tail factorization D0=q0*L_plus",
|
||||||
|
u*(3*u-2)*(3*u+2)*x*D0 - 144*(u-1)**2*L_plus,
|
||||||
|
)
|
||||||
|
check_zero("cleared tail factorization D1=-L_plus", D1 + L_plus)
|
||||||
|
check_zero(
|
||||||
|
"cleared tail factorization D2=q2*L_plus",
|
||||||
|
2*D2 - (-2+7*x-2*u*x)*L_plus,
|
||||||
|
)
|
||||||
|
check_zero(
|
||||||
|
"cleared fourth companion closure D3=q3*L_plus",
|
||||||
|
36*D3 - q3_numerator*L_plus,
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# Row-zero coefficient identities. These prove F_N=P_0(delta)F_(N+1)
|
||||||
|
# without any Ore division or finite sampling.
|
||||||
|
def A(argument):
|
||||||
|
return (
|
||||||
|
144*(u-1)**2*(argument+u)**3
|
||||||
|
/ (u*(3*u-2)*(3*u+2))
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def P0(argument):
|
||||||
|
return p_row(0, argument)
|
||||||
|
|
||||||
|
|
||||||
|
def B(argument):
|
||||||
|
return P0(argument) - A(argument)/x
|
||||||
|
|
||||||
|
|
||||||
|
rho = -(3*u-2)*(3*u+2) / (144*(u-1)**2*u**2)
|
||||||
|
|
||||||
|
|
||||||
|
def coeff_cross_ratio(argument):
|
||||||
|
return (
|
||||||
|
(
|
||||||
|
(m+argument)
|
||||||
|
* (m+F(1, 6)+argument)
|
||||||
|
* (m+F(1, 2)+argument)
|
||||||
|
* (m+F(5, 6)+argument)
|
||||||
|
)
|
||||||
|
/ (m*(m+F(1, 6))*(m+F(1, 2))*(m+F(5, 6)))
|
||||||
|
* (
|
||||||
|
2*m*(2*m+1)
|
||||||
|
/ ((2*m+argument)*(2*m+argument+1))
|
||||||
|
)**3
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def coeff_within_ratio(argument):
|
||||||
|
return (
|
||||||
|
(m+argument)
|
||||||
|
* (m+F(1, 6)+argument)
|
||||||
|
* (m+F(1, 2)+argument)
|
||||||
|
* (m+F(5, 6)+argument)
|
||||||
|
/ ((2*m+argument)**3*(argument+1))
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
check_zero("tail lowest-coefficient normalization", rho*(-A(0))-1)
|
||||||
|
check_zero(
|
||||||
|
"tail generic coefficient identity",
|
||||||
|
rho * (
|
||||||
|
-A(j)*coeff_cross_ratio(j)
|
||||||
|
+ (A(j-1)+B(j-1))
|
||||||
|
* coeff_cross_ratio(j-1)
|
||||||
|
/ coeff_within_ratio(j-1)
|
||||||
|
) - 1,
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# Terminating denominator: explicit one-step coefficient induction.
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
normalization = 576*n**2*(2*n+1)**2 / ((6*n+1)*(6*n+5))
|
||||||
|
|
||||||
|
|
||||||
|
def d0(argument):
|
||||||
|
return (
|
||||||
|
72*(2*n+1)**2*(2*n-argument)**3
|
||||||
|
/ (n*(6*n+1)*(6*n+5))
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def d1_polynomial(argument):
|
||||||
|
return (
|
||||||
|
5*argument - 51*argument**2 - 72*argument**3
|
||||||
|
- 5*n + 127*argument*n + 659*argument**2*n - 432*argument**3*n
|
||||||
|
- 76*n**2 - 1760*argument*n**2 + 3086*argument**2*n**2
|
||||||
|
- 864*argument**3*n**2
|
||||||
|
+ 1404*n**3 - 6536*argument*n**3 + 4500*argument**2*n**3
|
||||||
|
- 576*argument**3*n**3
|
||||||
|
+ 4360*n**4 - 7632*argument*n**4 + 2232*argument**2*n**4
|
||||||
|
+ 4320*n**5 - 3024*argument*n**5
|
||||||
|
+ 1440*n**6
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def d1(argument):
|
||||||
|
return (
|
||||||
|
-d1_polynomial(argument)
|
||||||
|
/ (n*(2*n+1)*(6*n+1)*(6*n+5))
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# Horizontal adjoint reconstruction. If p is the first row component, the
|
||||||
|
# other three are p_i(theta)p with the following explicit polynomials. Their
|
||||||
|
# contraction with the first column of -z M(2n+1,-z/(1-z)) must be exactly
|
||||||
|
# d0(theta)+z*d1(theta). This is the formerly implicit matrix-to-scalar
|
||||||
|
# bridge.
|
||||||
|
p_ops = [
|
||||||
|
Rat(1),
|
||||||
|
(
|
||||||
|
2*t*(
|
||||||
|
-36 + 216*n - 432*n**2
|
||||||
|
- 36*t + 216*n*t - 36*t**2
|
||||||
|
+ 23*z + 162*n*z + 216*n**2*z
|
||||||
|
- 54*t*z - 144*n*t*z + 36*t**2*z
|
||||||
|
)
|
||||||
|
/ (n*(1+2*n)*(1+6*n)*(5+6*n)*z)
|
||||||
|
),
|
||||||
|
(
|
||||||
|
36*t*(
|
||||||
|
4 - 12*n + 2*t + 3*z + 8*n*z - 2*t*z
|
||||||
|
)
|
||||||
|
/ (n*(1+2*n)*(1+6*n)*(5+6*n)*z)
|
||||||
|
),
|
||||||
|
(
|
||||||
|
72*t*(-1+z)
|
||||||
|
/ (n*(1+2*n)*(1+6*n)*(5+6*n)*z)
|
||||||
|
),
|
||||||
|
]
|
||||||
|
|
||||||
|
l_tail = (
|
||||||
|
t*(t+2*n-1)**3
|
||||||
|
- z*(t+n)*(t+n+F(1, 6))*(t+n+F(1, 2))*(t+n+F(5, 6))
|
||||||
|
)
|
||||||
|
l_coefficients = [
|
||||||
|
polynomial_coefficient(l_tail, "t", degree)
|
||||||
|
for degree in range(5)
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
def companion(parameter):
|
||||||
|
operator = (
|
||||||
|
t*(t+2*parameter-1)**3
|
||||||
|
- z*(t+parameter)
|
||||||
|
*(t+parameter+F(1, 6))
|
||||||
|
*(t+parameter+F(1, 2))
|
||||||
|
*(t+parameter+F(5, 6))
|
||||||
|
)
|
||||||
|
coefficients = [
|
||||||
|
polynomial_coefficient(operator, "t", degree)
|
||||||
|
for degree in range(5)
|
||||||
|
]
|
||||||
|
return [
|
||||||
|
[0, 1, 0, 0],
|
||||||
|
[0, 0, 1, 0],
|
||||||
|
[0, 0, 0, 1],
|
||||||
|
[
|
||||||
|
-coefficients[column]/coefficients[4]
|
||||||
|
for column in range(4)
|
||||||
|
],
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
def theta_operator(operator):
|
||||||
|
"""Left-coefficient Euler composition: theta Q = z Q_z + t Q."""
|
||||||
|
return z*operator.derivative("z") + t*operator
|
||||||
|
|
||||||
|
|
||||||
|
check_zero(
|
||||||
|
"horizontal reconstruction pi3",
|
||||||
|
p_ops[3] - l_coefficients[4]/l_coefficients[0]*t,
|
||||||
|
)
|
||||||
|
check_zero(
|
||||||
|
"horizontal reconstruction pi2",
|
||||||
|
p_ops[2]
|
||||||
|
- l_coefficients[3]/l_coefficients[4]*p_ops[3]
|
||||||
|
+ theta_operator(p_ops[3]),
|
||||||
|
)
|
||||||
|
check_zero(
|
||||||
|
"horizontal reconstruction pi1",
|
||||||
|
p_ops[1]
|
||||||
|
- l_coefficients[2]/l_coefficients[4]*p_ops[3]
|
||||||
|
+ theta_operator(p_ops[2]),
|
||||||
|
)
|
||||||
|
|
||||||
|
terminating_operator = (
|
||||||
|
t*(t-2*n)**3
|
||||||
|
- z*(t-n)*(t-n-F(1, 6))*(t-n-F(1, 2))*(t-n-F(5, 6))
|
||||||
|
)
|
||||||
|
adjoint_factor = -72/(n*(2*n+1)*(6*n+1)*(6*n+5)*z)
|
||||||
|
check_zero(
|
||||||
|
"horizontal reconstruction closes to the terminating operator",
|
||||||
|
theta_operator(p_ops[1]) + 1
|
||||||
|
- l_coefficients[1]/l_coefficients[4]*p_ops[3]
|
||||||
|
- adjoint_factor*terminating_operator,
|
||||||
|
)
|
||||||
|
|
||||||
|
gauge = [[-z*entry for entry in row] for row in matrix_nz]
|
||||||
|
left_gauge = matrix_multiply(companion(n), gauge)
|
||||||
|
right_gauge = matrix_multiply(gauge, companion(n+1))
|
||||||
|
gauge_residual = [
|
||||||
|
[
|
||||||
|
left_gauge[row][column]
|
||||||
|
- z*gauge[row][column].derivative("z")
|
||||||
|
- right_gauge[row][column]
|
||||||
|
for column in range(4)
|
||||||
|
]
|
||||||
|
for row in range(4)
|
||||||
|
]
|
||||||
|
check_zero_matrix(
|
||||||
|
"all sixteen authoritative differential-gauge equations",
|
||||||
|
gauge_residual,
|
||||||
|
)
|
||||||
|
|
||||||
|
matrix_induced_step = sum(
|
||||||
|
p_ops[row] * gauge_first_column[row]
|
||||||
|
for row in range(4)
|
||||||
|
)
|
||||||
|
check_zero(
|
||||||
|
"authoritative matrix induces the displayed d0+z*d1 scalar step",
|
||||||
|
matrix_induced_step - d0(t) - z*d1(t),
|
||||||
|
)
|
||||||
|
|
||||||
|
# Base polynomial from the compact denominator row:
|
||||||
|
# q_0(x)=18/x+159/4, Q_0=x q_0, p_1=(1-z)Q_0(-z/(1-z)).
|
||||||
|
q_zero = 18/x + F(159, 4)
|
||||||
|
Q_zero = x*q_zero
|
||||||
|
p_one = (1-z)*substitute_rational(Q_zero, {"x": -z/(1-z)})
|
||||||
|
check_zero(
|
||||||
|
"terminating base polynomial from the compact denominator row",
|
||||||
|
p_one - 18*(1-F(77, 24)*z),
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
def apply_euler_operator(operator, function, maximum_degree=3):
|
||||||
|
result = Rat(0)
|
||||||
|
theta_power = function
|
||||||
|
for degree in range(maximum_degree+1):
|
||||||
|
result += polynomial_coefficient(operator, "t", degree)*theta_power
|
||||||
|
theta_power = z*theta_power.derivative("z")
|
||||||
|
return result
|
||||||
|
|
||||||
|
|
||||||
|
compact_denominator = [
|
||||||
|
18/x + F(159, 4),
|
||||||
|
54/x + F(131, 2),
|
||||||
|
54/x + 27,
|
||||||
|
18/x,
|
||||||
|
]
|
||||||
|
base_horizontal_row = [
|
||||||
|
-z*substitute_rational(entry, {"x": -z/(1-z)})
|
||||||
|
for entry in compact_denominator
|
||||||
|
]
|
||||||
|
for row in range(4):
|
||||||
|
reconstructed = apply_euler_operator(
|
||||||
|
substitute_rational(p_ops[row], {"n": 1}),
|
||||||
|
p_one,
|
||||||
|
)
|
||||||
|
check_zero(
|
||||||
|
f"base horizontal-row reconstruction component {row}",
|
||||||
|
base_horizontal_row[row] - reconstructed,
|
||||||
|
)
|
||||||
|
|
||||||
|
base_terminating_operator = substitute_rational(
|
||||||
|
terminating_operator,
|
||||||
|
{"n": 1},
|
||||||
|
)
|
||||||
|
check_zero(
|
||||||
|
"base polynomial satisfies the terminating operator",
|
||||||
|
apply_euler_operator(
|
||||||
|
base_terminating_operator,
|
||||||
|
p_one,
|
||||||
|
maximum_degree=4,
|
||||||
|
),
|
||||||
|
)
|
||||||
|
|
||||||
|
base_times_companion = matrix_multiply(
|
||||||
|
[base_horizontal_row],
|
||||||
|
companion(Rat(1)),
|
||||||
|
)[0]
|
||||||
|
for column in range(4):
|
||||||
|
check_zero(
|
||||||
|
f"base horizontal adjoint residual component {column}",
|
||||||
|
z*base_horizontal_row[column].derivative("z")
|
||||||
|
+ base_times_companion[column],
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
within_ratio = (
|
||||||
|
(k-1-n)
|
||||||
|
* (k-1-n-F(1, 6))
|
||||||
|
* (k-1-n-F(1, 2))
|
||||||
|
* (k-1-n-F(5, 6))
|
||||||
|
/ ((k-2*n)**3*k)
|
||||||
|
)
|
||||||
|
cross_ratio = (
|
||||||
|
(n+1)/(n+1-k)
|
||||||
|
* (n+1+F(1, 6))/(n+1+F(1, 6)-k)
|
||||||
|
* (n+1+F(1, 2))/(n+1+F(1, 2)-k)
|
||||||
|
* (n+1+F(5, 6))/(n+1+F(5, 6)-k)
|
||||||
|
* ((k-2*n-1)*(k-2*n)/(2*n*(2*n+1)))**3
|
||||||
|
)
|
||||||
|
top_ratio = (
|
||||||
|
-(n+F(7, 6))*(n+F(3, 2))*(n+F(11, 6))
|
||||||
|
/ (8*(2*n+1)**3)
|
||||||
|
)
|
||||||
|
|
||||||
|
check_zero("terminating constant-term normalization", d0(0)-normalization)
|
||||||
|
check_zero(
|
||||||
|
"terminating generic coefficient induction",
|
||||||
|
d0(k) + d1(k-1)/within_ratio - normalization*cross_ratio,
|
||||||
|
)
|
||||||
|
check_zero(
|
||||||
|
"terminating top-degree boundary",
|
||||||
|
d1(n) - normalization*top_ratio,
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# Two formerly named special-function steps, reduced to coefficients.
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
ascension_left_ratio = (
|
||||||
|
(k-F(5, 6))*(k-F(1, 2))*(k-F(1, 6))/k**3
|
||||||
|
)
|
||||||
|
ascension_right_ratio = (
|
||||||
|
(k-1)
|
||||||
|
* (k-F(5, 6))
|
||||||
|
* (k-F(1, 2))
|
||||||
|
* (k-F(1, 6))
|
||||||
|
/ (k**3*(k-1))
|
||||||
|
)
|
||||||
|
check_zero("ascension base coefficient", F(1, 6)*F(1, 2)*F(5, 6)-F(5, 72))
|
||||||
|
check_zero(
|
||||||
|
"ascension consecutive-coefficient ratio",
|
||||||
|
ascension_left_ratio-ascension_right_ratio,
|
||||||
|
)
|
||||||
|
|
||||||
|
theta_product = (
|
||||||
|
(t+F(1, 6))*(t+F(1, 2))*(t+F(5, 6))
|
||||||
|
)
|
||||||
|
theta_product_expanded = (
|
||||||
|
t**3 + F(3, 2)*t**2 + F(23, 36)*t + F(5, 72)
|
||||||
|
)
|
||||||
|
check_zero(
|
||||||
|
"3F2 Euler-operator coefficient expansion",
|
||||||
|
theta_product-theta_product_expanded,
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
print("PASS: all standalone exact-equation obligations")
|
||||||
|
print("No division algorithm, CAS simplifier, root finder, or sampling was used.")
|
||||||
Binary file not shown.
|
|
@ -5,12 +5,40 @@ cd "$(dirname "$0")"
|
||||||
|
|
||||||
python3 certificates/p28_rank_ode_bound_verifier.py
|
python3 certificates/p28_rank_ode_bound_verifier.py
|
||||||
python3 certificates/p28_convergence_constants.py
|
python3 certificates/p28_convergence_constants.py
|
||||||
|
python3 certificates/p28_standalone_equations.py
|
||||||
|
python3 certificates/p28_dominant_product_algebra.py
|
||||||
|
|
||||||
|
python3 - <<'PY'
|
||||||
|
from pathlib import Path
|
||||||
|
|
||||||
|
forbidden = {
|
||||||
|
Path("solution.tex"): (
|
||||||
|
"Birkhoff",
|
||||||
|
"Poincar",
|
||||||
|
"standard ascension",
|
||||||
|
"analytic solution normalized at",
|
||||||
|
),
|
||||||
|
Path("certificates/p28_kernel_contiguity_certificate.sage"): ("quo_rem",),
|
||||||
|
Path("certificates/all_four_columns_certificate.sage"): (
|
||||||
|
"is_irreducible",
|
||||||
|
"gcd(",
|
||||||
|
),
|
||||||
|
}
|
||||||
|
for path, needles in forbidden.items():
|
||||||
|
text = path.read_text(encoding="utf-8")
|
||||||
|
for needle in needles:
|
||||||
|
if needle in text:
|
||||||
|
raise SystemExit(f"FAIL: forbidden proof shortcut {needle!r} in {path}")
|
||||||
|
print("PASS: no forbidden proof shortcuts in the mandatory path")
|
||||||
|
PY
|
||||||
|
|
||||||
|
echo "DIAGNOSTIC (not an all-N proof): finite Padé regression"
|
||||||
python3 certificates/p28_parametric_pade_probe.py
|
python3 certificates/p28_parametric_pade_probe.py
|
||||||
|
|
||||||
if command -v wolframscript >/dev/null 2>&1; then
|
if command -v wolframscript >/dev/null 2>&1; then
|
||||||
wolframscript -file certificates/p28_full_closure_certificate.wl
|
wolframscript -file certificates/p28_full_closure_certificate.wl
|
||||||
else
|
else
|
||||||
echo "SKIP: wolframscript is not installed; see the included PASS transcript."
|
echo "OPTIONAL: wolframscript is not installed; mandatory equations already passed."
|
||||||
fi
|
fi
|
||||||
|
|
||||||
if command -v sage >/dev/null 2>&1; then
|
if command -v sage >/dev/null 2>&1; then
|
||||||
|
|
@ -18,5 +46,5 @@ if command -v sage >/dev/null 2>&1; then
|
||||||
sage certificates/p28_lattice_hypotheses_certificate.sage
|
sage certificates/p28_lattice_hypotheses_certificate.sage
|
||||||
sage certificates/all_four_columns_certificate.sage
|
sage certificates/all_four_columns_certificate.sage
|
||||||
else
|
else
|
||||||
echo "SKIP: SageMath is not installed; independent Sage checks were not run."
|
echo "OPTIONAL: SageMath is not installed; mandatory equations already passed."
|
||||||
fi
|
fi
|
||||||
|
|
|
||||||
Binary file not shown.
|
|
@ -58,15 +58,17 @@ Equivalently, \(Q_{N,j}/P_{N,j}\to\pi/\sqrt{10005}\).
|
||||||
|
|
||||||
The missing connection constant is fixed by an exact rank-three
|
The missing connection constant is fixed by an exact rank-three
|
||||||
hypergeometric tail. A nonterminating \(\F43\) Euler jet is carried
|
hypergeometric tail. A nonterminating \(\F43\) Euler jet is carried
|
||||||
backward by the authoritative matrix, while the first denominator is a
|
backward by the displayed matrix, while the first denominator is a
|
||||||
terminating adjoint \(\F43\). Their common differential gauge gives an
|
terminating adjoint \(\F43\). Four denominator-cleared Ore identities
|
||||||
all-\(N\) Pad\'e divisibility theorem. Positivity of the terminating
|
and three coefficient identities give an all-\(N\) Pad\'e divisibility
|
||||||
denominator at the negative CM point, together with a balanced-transfer
|
theorem. Positivity at the negative CM point, a Cauchy estimate, and an
|
||||||
Cauchy estimate, turns that formal divisibility into a direct fixed-point
|
explicit stable-graph contraction prove convergence for all four columns.
|
||||||
convergence proof. The symbolic contiguity and adjoint identities are
|
Every algebraic identity used below is reproduced by a dependency-free
|
||||||
included as reproducible Wolfram Language and SageMath certificates.
|
rational-polynomial checker. The classical Chudnovsky formula, cited
|
||||||
|
precisely in Section~2, is the sole imported theorem.
|
||||||
\end{abstract}
|
\end{abstract}
|
||||||
|
|
||||||
|
\enlargethispage{2\baselineskip}
|
||||||
\tableofcontents
|
\tableofcontents
|
||||||
|
|
||||||
\section{Statement and compact form of the seeds}
|
\section{Statement and compact form of the seeds}
|
||||||
|
|
@ -85,16 +87,49 @@ Let
|
||||||
\[
|
\[
|
||||||
G_N=M_0M_1\cdots M_{N-1},\qquad G_0=I_4,
|
G_N=M_0M_1\cdots M_{N-1},\qquad G_0=I_4,
|
||||||
\]
|
\]
|
||||||
where \(M_N=M(N,x)\) is the authoritative transfer matrix in the analytic
|
where the rational family is defined as follows. Put \(r=x^{-1}\),
|
||||||
deformation
|
\(\omega=u(3u-2)(3u+2)\), and
|
||||||
|
\begin{align*}
|
||||||
|
a_1={}&r(144u^5-288u^4+144u^3)
|
||||||
|
-99u^5+333u^4-229u^3-114u^2+40u+64,\\
|
||||||
|
a_2={}&r(432u^4-864u^3+432u^2)
|
||||||
|
-243u^4+909u^3-868u^2-80u+272,\\
|
||||||
|
a_3={}&r(432u^3-864u^2+432u)
|
||||||
|
-153u^3+648u^2-860u+360,\\
|
||||||
|
a_4={}&144r(u-1)^2,\\
|
||||||
|
b_1={}&-144ru^3+9u^4+63u^3+158u^2+168u+64,\\
|
||||||
|
b_2={}&216ru^2+36u^3-189u^2-316u-168,\\
|
||||||
|
b_3={}&108ru+54u^2-189u-158,\\
|
||||||
|
c_1={}&-288r^2u^3+
|
||||||
|
r(54u^4+378u^3+948u^2+1008u+384)\\
|
||||||
|
&\hspace{2.2em}+18u^5+45u^4-251u^3-1086u^2-1384u-576,\\
|
||||||
|
c_2={}&-432r^2u^2+
|
||||||
|
r(153u^4-657u^3+1292u^2+2064u+1072)\\
|
||||||
|
&\hspace{2.2em}-72u^4+702u^3-1069u^2-2508u-1512,\\
|
||||||
|
c_3={}&-216r^2u+
|
||||||
|
r(180u^3-891u^2+1450u+1116)\\
|
||||||
|
&\hspace{2.2em}-108u^3+864u^2-1385u-1422,\\
|
||||||
|
c_4={}&-4r^2+r(6u^2-33u+\tfrac{536}{9})
|
||||||
|
-4u^2+32u-63.
|
||||||
|
\end{align*}
|
||||||
|
Define
|
||||||
|
\begin{equation}\label{eq:deformed-matrix}
|
||||||
|
\mathcal M(u,x)=
|
||||||
|
\begin{pmatrix}
|
||||||
|
a_1/\omega&a_2/\omega&a_3/\omega&a_4/\omega\\
|
||||||
|
-u^3&-3u^2&-3u&-1\\
|
||||||
|
xb_1/144&-xb_2/72&-xb_3/36&
|
||||||
|
x(-2r-(2u-7))/2\\
|
||||||
|
x^2c_1/288&x^2c_2/144&x^2c_3/72&x^2c_4/4
|
||||||
|
\end{pmatrix},
|
||||||
|
\qquad M_N(x)=\mathcal M(2N+3,x).
|
||||||
|
\end{equation}
|
||||||
|
At \(x=x_0\), the only deformed challenge coefficient is restored by
|
||||||
\[
|
\[
|
||||||
236337691420383\ \longmapsto\ \frac{14/x-567}{9}.
|
236337691420383=\frac{14R-567}{9}.
|
||||||
\]
|
\]
|
||||||
At \(x=x_0\), this is the exact identity
|
Thus every use of Cauchy's theorem below concerns the explicitly displayed
|
||||||
\(236337691420383=(14R-567)/9\). Thus every later use of Cauchy's theorem
|
rational \(x\)-family, not an unspecified continuation.
|
||||||
concerns this explicitly defined rational \(x\)-family.
|
|
||||||
The complete entries of \(M(N,x)\) appear verbatim in the accompanying
|
|
||||||
CAS certificates.
|
|
||||||
|
|
||||||
Define four Pascal rows
|
Define four Pascal rows
|
||||||
\[
|
\[
|
||||||
|
|
@ -131,7 +166,19 @@ The two official initial rows have the exact form
|
||||||
H_0=Ab_0+Bb_1=(A+B,B,0,0).
|
H_0=Ab_0+Bb_1=(A+B,B,0,0).
|
||||||
\end{equation}
|
\end{equation}
|
||||||
At \(x=x_0\), these identities reproduce the official integer rows
|
At \(x=x_0\), these identities reproduce the official integer rows
|
||||||
entry by entry.
|
entry by entry:
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
A_0={}&(37169305760442252761441,\,
|
||||||
|
111507917281327441564208,\\
|
||||||
|
&\hspace{4.7em}111507917281327599720129,\,
|
||||||
|
37169305760442410917362),\\
|
||||||
|
A_1={}&(1167416361542639692320,\,
|
||||||
|
3502249084627896132160,\\
|
||||||
|
&\hspace{4.7em}3502249084627879697280,\,
|
||||||
|
1167416361542622723840).
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
|
||||||
For \(j=1,\ldots,4\), write
|
For \(j=1,\ldots,4\), write
|
||||||
\[
|
\[
|
||||||
|
|
@ -156,7 +203,10 @@ and define
|
||||||
\Phi(x)=\frac{Ay(z)+B\theta y(z)}{S}.
|
\Phi(x)=\frac{Ay(z)+B\theta y(z)}{S}.
|
||||||
\end{equation}
|
\end{equation}
|
||||||
|
|
||||||
The classical Chudnovsky identity is
|
We use one external theorem: the classical Chudnovsky identity. In the
|
||||||
|
normalization used here it is Theorem~0.1 of Milla's equation-by-equation
|
||||||
|
derivation \([2]\), whose modular and CM proof is completed in
|
||||||
|
Theorem~9.7 and Chapter~10:
|
||||||
\[
|
\[
|
||||||
\frac1\pi=
|
\frac1\pi=
|
||||||
\frac{12}{640320^{3/2}}
|
\frac{12}{640320^{3/2}}
|
||||||
|
|
@ -212,24 +262,89 @@ Its Euler jet is
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
The first row is verified coefficientwise from the ratio of consecutive
|
Put \(m=(u-1)/2=N+1\). For the \(r\)-th row of
|
||||||
\(\F43\) coefficients. For the other rows, let \(t=\delta_{N+1}\).
|
\(\mathcal M(u,x)\), define
|
||||||
|
\[
|
||||||
|
P_r(t)=\sum_{s=0}^3\mathcal M(u,x)_{r+1,s+1}t^s,\qquad
|
||||||
|
\mathcal TQ=(1-x)x\partial_xQ+(t+1)Q.
|
||||||
|
\]
|
||||||
The shifted tail satisfies
|
The shifted tail satisfies
|
||||||
\[
|
\[
|
||||||
\left[
|
L_+(t)F_{N+1}=0,
|
||||||
(1-x)t(t+u)^3+
|
|
||||||
x(t+n+1)(t+n+\tfrac76)(t+n+\tfrac32)(t+n+\tfrac{11}{6})
|
|
||||||
\right]F_{N+1}=0,
|
|
||||||
\]
|
\]
|
||||||
where \(u=2N+3\). Each of the remaining three row differences is divided
|
where
|
||||||
by this degree-four Ore polynomial; its remainder is identically zero in
|
\[
|
||||||
\(\Q(N,x)[t]\). The exact coefficient identity, the three Ore divisions,
|
L_+(t)=(1-x)t(t+u)^3+
|
||||||
and the normalization ratio are checked in
|
x(t+m+1)(t+m+\tfrac76)(t+m+\tfrac32)(t+m+\tfrac{11}{6}).
|
||||||
\texttt{p28\_full\_closure\_certificate.wl} and
|
\]
|
||||||
\texttt{p28\_kernel\_contiguity\_certificate.sage}.
|
There is no division step: direct expansion gives the following four
|
||||||
|
denominator-cleared polynomial identities:
|
||||||
|
\begin{align}
|
||||||
|
u(3u-2)(3u+2)x(\mathcal TP_0-P_1)
|
||||||
|
& =144(u-1)^2L_+,\label{eq:ore0}\\
|
||||||
|
\mathcal TP_1-P_2&=-L_+,\label{eq:ore1}\\
|
||||||
|
2(\mathcal TP_2-P_3)&=(-2+7x-2ux)L_+,\label{eq:ore2}\\
|
||||||
|
36(\mathcal TP_3+\ell_3P_3+\ell_2P_2+\ell_1P_1+\ell_0P_0)
|
||||||
|
&=q_3L_+,\label{eq:ore3}
|
||||||
|
\end{align}
|
||||||
|
with
|
||||||
|
\begin{align*}
|
||||||
|
\ell_0={}&(u-1)u(3u-2)(3u+2)x/144,\\
|
||||||
|
\ell_1={}&[-576+864u-432u^2+72u^3
|
||||||
|
+(580-872u+405u^2-36u^3)x]/72,\\
|
||||||
|
\ell_2={}&[432-432u+108u^2
|
||||||
|
+(-436+405u-54u^2)x]/36,\\
|
||||||
|
\ell_3={}&(-12+6u+11x-2ux)/2,\\
|
||||||
|
q_3={}&-36+(536-297u+54u^2)x
|
||||||
|
+(-567+288u-36u^2)x^2.
|
||||||
|
\end{align*}
|
||||||
|
|
||||||
|
For clarity, the coefficient calculation producing the first row is also
|
||||||
|
written without a special-function routine. Set
|
||||||
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
A(t)&=\frac{144(u-1)^2(t+u)^3}{u(3u-2)(3u+2)},&
|
||||||
|
B(t)&=P_0(t)-\frac{A(t)}x,\\
|
||||||
|
\varrho&=-\frac{(3u-2)(3u+2)}{144(u-1)^2u^2},\\
|
||||||
|
\chi_j&=
|
||||||
|
\frac{(m+j)(m+\frac16+j)(m+\frac12+j)(m+\frac56+j)}
|
||||||
|
{m(m+\frac16)(m+\frac12)(m+\frac56)}\\
|
||||||
|
&\quad{}\times
|
||||||
|
\left(\frac{2m(2m+1)}{(2m+j)(2m+j+1)}\right)^3,\\
|
||||||
|
\psi_j&=
|
||||||
|
\frac{(m+j)(m+\frac16+j)(m+\frac12+j)(m+\frac56+j)}
|
||||||
|
{(2m+j)^3(j+1)} .
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
The constant and generic coefficient equations are
|
||||||
|
\begin{equation}\label{eq:tail-coefficients}
|
||||||
|
\varrho[-A(0)]=1,\qquad
|
||||||
|
\varrho\left[-A(j)\chi_j+
|
||||||
|
\frac{(A(j-1)+B(j-1))\chi_{j-1}}{\psi_{j-1}}\right]=1
|
||||||
|
\quad(j\ge1).
|
||||||
|
\end{equation}
|
||||||
|
Clearing the displayed nonzero factors turns
|
||||||
|
\eqref{eq:ore0}--\eqref{eq:tail-coefficients} into polynomial
|
||||||
|
equalities with every coefficient zero. The independent script
|
||||||
|
\texttt{p28\_standalone\_equations.py} expands precisely these equalities
|
||||||
|
using only rational addition and multiplication. Equation
|
||||||
|
\eqref{eq:tail-coefficients} gives the first row of
|
||||||
|
\eqref{eq:tail-contiguity}; applying
|
||||||
|
\eqref{eq:ore0}--\eqref{eq:ore3} successively gives the other three
|
||||||
|
Euler-jet rows.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
For \(N=0\), the standard ascension identity gives
|
For \(N=0\), write \(y(z)=1+\sum_{k\ge1}c_kz^k\). The coefficient of
|
||||||
|
\(z\) is
|
||||||
|
\[
|
||||||
|
c_1=\frac{(1/6)(1/2)(5/6)}{1^3}=\frac5{72},
|
||||||
|
\]
|
||||||
|
and, after shifting \(k\mapsto k+1\), both sides below have initial
|
||||||
|
coefficient \(5/72\) and consecutive-coefficient ratio
|
||||||
|
\[
|
||||||
|
\frac{(k+\frac16)(k+\frac12)(k+\frac56)}{(k+1)^3}.
|
||||||
|
\]
|
||||||
|
Hence coefficient equality, rather than a named ascension rule, gives
|
||||||
\begin{equation}\label{eq:ascension}
|
\begin{equation}\label{eq:ascension}
|
||||||
F_0=y-1
|
F_0=y-1
|
||||||
=\frac5{72}z
|
=\frac5{72}z
|
||||||
|
|
@ -255,6 +370,14 @@ The transformed hypergeometric equation is
|
||||||
\begin{equation}\label{eq:transformed-ode}
|
\begin{equation}\label{eq:transformed-ode}
|
||||||
72\theta^3y+108x\theta^2y+46x\theta y+5xy=0.
|
72\theta^3y+108x\theta^2y+46x\theta y+5xy=0.
|
||||||
\end{equation}
|
\end{equation}
|
||||||
|
Indeed the coefficient ratio of \(y\) gives
|
||||||
|
\[
|
||||||
|
\left[\theta^3-
|
||||||
|
z(\theta+\tfrac16)(\theta+\tfrac12)(\theta+\tfrac56)\right]y=0.
|
||||||
|
\]
|
||||||
|
Substituting \(z=-x/(1-x)\), using
|
||||||
|
\(\theta=(1-x)x\partial_x\), and multiplying by \(72(1-x)\)
|
||||||
|
expands to \eqref{eq:transformed-ode}.
|
||||||
Using the displayed decomposition of \(C\), equations
|
Using the displayed decomposition of \(C\), equations
|
||||||
\eqref{eq:ascension}--\eqref{eq:transformed-ode} give
|
\eqref{eq:ascension}--\eqref{eq:transformed-ode} give
|
||||||
\[
|
\[
|
||||||
|
|
@ -309,6 +432,21 @@ Since \(z=-x+O(x^2)\),
|
||||||
\end{equation}
|
\end{equation}
|
||||||
The leading vector in \eqref{eq:tail-direction} is precisely the image
|
The leading vector in \eqref{eq:tail-direction} is precisely the image
|
||||||
direction in \eqref{eq:rank-one}.
|
direction in \eqref{eq:rank-one}.
|
||||||
|
The other expansion required below is equally direct. Since
|
||||||
|
\[
|
||||||
|
F_{N+1}=\kappa_{N+1}z^{N+2}(1+O(z)),\qquad
|
||||||
|
\delta_{N+1}=\theta-(N+2),
|
||||||
|
\]
|
||||||
|
the shifted derivatives kill the leading monomial, and therefore
|
||||||
|
\begin{equation}\label{eq:next-tail-direction}
|
||||||
|
k_{N+1}=x^{N+2}\widetilde\eta_N
|
||||||
|
\left(\e_1+xs_N+O(x^2)\right),
|
||||||
|
\qquad\widetilde\eta_N\ne0.
|
||||||
|
\end{equation}
|
||||||
|
Moreover, \eqref{eq:rank-one} gives
|
||||||
|
\[
|
||||||
|
J_N(0)\e_1=u^3(a_N,-1,-1,-1)^T\ne0.
|
||||||
|
\]
|
||||||
|
|
||||||
\begin{lemma}[DVR step, including the extra first-column zero]
|
\begin{lemma}[DVR step, including the extra first-column zero]
|
||||||
\label{lem:dvr}
|
\label{lem:dvr}
|
||||||
|
|
@ -378,7 +516,8 @@ Consequently the constant term in the first column of \(fC\) is
|
||||||
|
|
||||||
Apply Lemma~\ref{lem:dvr} inductively, using
|
Apply Lemma~\ref{lem:dvr} inductively, using
|
||||||
\eqref{eq:annihilation}, \eqref{eq:rank-one},
|
\eqref{eq:annihilation}, \eqref{eq:rank-one},
|
||||||
\eqref{eq:tail-direction}, and \(M_Nk_{N+1}=k_N\).
|
\eqref{eq:tail-direction}, \eqref{eq:next-tail-direction}, the displayed
|
||||||
|
nonzero first column of \(J_N(0)\), and \(M_Nk_{N+1}=k_N\).
|
||||||
The stronger last-row assertion follows from
|
The stronger last-row assertion follows from
|
||||||
\eqref{eq:row-relation}.
|
\eqref{eq:row-relation}.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
@ -421,39 +560,154 @@ can vanish.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
The proof is an exact differential-gauge calculation in
|
Write \(p_n=\widehat Q_{n-1}\) for \(n\ge1\). We use coefficient
|
||||||
\(\Q(n,z)\). The nonterminating tail
|
induction, because normalization at \(z=0\) alone
|
||||||
|
would not select a unique solution of the fourth-order equation. To expose
|
||||||
|
the matrix-to-scalar bridge, write
|
||||||
\[
|
\[
|
||||||
\F43\left(
|
\mathcal L_n(t)=t(t+2n-1)^3
|
||||||
\begin{matrix}n,n+\frac16,n+\frac12,n+\frac56\\
|
-z(t+n)(t+n+\tfrac16)(t+n+\tfrac12)(t+n+\tfrac56)
|
||||||
2n,2n,2n
|
=\sum_{j=0}^4c_jt^j
|
||||||
\end{matrix};z\right)
|
|
||||||
\]
|
\]
|
||||||
has a \(4\times4\) Euler companion system. Direct simplification gives
|
and define, for operator polynomials with coefficients on the left,
|
||||||
\[
|
\[
|
||||||
\mathcal C_n(z)\,[-zM(2n+1,-z/(1-z))]
|
\Theta Q=z\partial_zQ+tQ.
|
||||||
-\theta[-zM(2n+1,-z/(1-z))]
|
|
||||||
-[-zM(2n+1,-z/(1-z))]\mathcal C_{n+1}(z)=0.
|
|
||||||
\]
|
\]
|
||||||
The transformed seed \(-zC(-z/(1-z))\) is a horizontal adjoint row.
|
The four horizontal components are reconstructed from the first by
|
||||||
Eliminating its other three coordinates from the horizontal equation
|
|
||||||
produces exactly
|
|
||||||
\[
|
\[
|
||||||
\left[
|
\pi_0=1,\qquad
|
||||||
\theta(\theta-2n)^3
|
\pi_3=\frac{c_4}{c_0}t,\qquad
|
||||||
-z(\theta-n)(\theta-n-\tfrac16)
|
\pi_2=\frac{c_3}{c_4}\pi_3-\Theta\pi_3,\qquad
|
||||||
(\theta-n-\tfrac12)(\theta-n-\tfrac56)
|
\pi_1=\frac{c_2}{c_4}\pi_3-\Theta\pi_2.
|
||||||
\right]\widehat Q_N=0.
|
|
||||||
\]
|
\]
|
||||||
The analytic solution normalized at \(z=0\) is the terminating
|
The remaining horizontal equation is the direct factorization
|
||||||
\(\F43\) in \eqref{eq:qhat}.
|
\[
|
||||||
|
\begin{aligned}
|
||||||
|
\Theta\pi_1+1-\frac{c_1}{c_4}\pi_3
|
||||||
|
={}&-\frac{72}{n(2n+1)(6n+1)(6n+5)z}\bigl[
|
||||||
|
t(t-2n)^3\\
|
||||||
|
&\hspace{4em}
|
||||||
|
-z(t-n)(t-n-\tfrac16)
|
||||||
|
(t-n-\tfrac12)(t-n-\tfrac56)\bigr].
|
||||||
|
\end{aligned}
|
||||||
|
\]
|
||||||
|
Let
|
||||||
|
\[
|
||||||
|
\mathcal C_n(z)=
|
||||||
|
\begin{pmatrix}
|
||||||
|
0&1&0&0\\
|
||||||
|
0&0&1&0\\
|
||||||
|
0&0&0&1\\
|
||||||
|
-c_0/c_4&-c_1/c_4&-c_2/c_4&-c_3/c_4
|
||||||
|
\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
The propagation of the reconstructed row is the following sixteen-entry
|
||||||
|
identity:
|
||||||
|
\begin{equation}\label{eq:full-gauge}
|
||||||
|
\mathcal C_n[-z\mathcal M(2n+1,-z/(1-z))]
|
||||||
|
-\theta[-z\mathcal M(2n+1,-z/(1-z))]
|
||||||
|
-[-z\mathcal M(2n+1,-z/(1-z))]\mathcal C_{n+1}=0.
|
||||||
|
\end{equation}
|
||||||
|
Finally, direct contraction with the displayed matrix gives
|
||||||
|
\begin{equation}\label{eq:matrix-scalar-bridge}
|
||||||
|
\sum_{r=0}^3\pi_r(t)
|
||||||
|
\left[-z\mathcal M(2n+1,-z/(1-z))\right]_{r+1,1}
|
||||||
|
=d_0(t)+zd_1(t).
|
||||||
|
\end{equation}
|
||||||
|
These are identities in \(\Q(n,z)(t)\). The factors depending on the
|
||||||
|
integer \(n\) are nonzero for \(n\ge1\); no value is obtained by dividing
|
||||||
|
at \(z=0\), because the verifier cross-multiplies first and the reconstructed
|
||||||
|
base functions have removable limits there. The mandatory
|
||||||
|
sparse-polynomial verifier checks every
|
||||||
|
reconstruction equation, the closing factorization, and
|
||||||
|
\eqref{eq:full-gauge}--\eqref{eq:matrix-scalar-bridge} by cross
|
||||||
|
multiplication. For any reconstructed horizontal row these identities give
|
||||||
|
\begin{equation}\label{eq:terminating-step}
|
||||||
|
p_{n+1}
|
||||||
|
=\bigl(d_0(\theta)+zd_1(\theta)\bigr)p_n,
|
||||||
|
\end{equation}
|
||||||
|
where
|
||||||
|
\[
|
||||||
|
d_0(t)=
|
||||||
|
\frac{72(2n+1)^2(2n-t)^3}{n(6n+1)(6n+5)}
|
||||||
|
\]
|
||||||
|
and
|
||||||
|
\[
|
||||||
|
d_1(t)=-\frac{P(n,t)}{n(2n+1)(6n+1)(6n+5)}
|
||||||
|
\]
|
||||||
|
with
|
||||||
|
\begin{align*}
|
||||||
|
P(n,t)={}&-5n-76n^2+1404n^3+4360n^4+4320n^5+1440n^6\\
|
||||||
|
&+(5+127n-1760n^2-6536n^3-7632n^4-3024n^5)t\\
|
||||||
|
&+(-51+659n+3086n^2+4500n^3+2232n^4)t^2\\
|
||||||
|
&+(-72-432n-864n^2-576n^3)t^3.
|
||||||
|
\end{align*}
|
||||||
|
Thus \eqref{eq:terminating-step} is the scalar form of the displayed
|
||||||
|
matrix recurrence; no differential-equation uniqueness is used below.
|
||||||
|
|
||||||
For completeness, the CAS certificate does not rely only on this
|
Let
|
||||||
differential equation. It computes the actual one-step scalar operator
|
\[
|
||||||
and verifies its generic coefficient identity, its \(k=0\) normalization,
|
h_{n,k}=
|
||||||
and the separate top boundary \(k=n+1\). Every remainder simplifies
|
\frac{(-n)_k(-n-\frac16)_k(-n-\frac12)_k(-n-\frac56)_k}
|
||||||
identically to zero. This proves the statement for all \(n\), not merely
|
{(1-2n)_k^3k!}
|
||||||
for sampled values.
|
\quad(0\le k\le n),
|
||||||
|
\qquad
|
||||||
|
\nu_n=\frac{576n^2(2n+1)^2}{(6n+1)(6n+5)}.
|
||||||
|
\]
|
||||||
|
For \(n\ge1\), clearing the displayed nonzero denominators gives exactly
|
||||||
|
\begin{align}
|
||||||
|
d_0(0)&=\nu_n,\label{eq:term-constant}\\
|
||||||
|
d_0(k)+d_1(k-1)\frac{h_{n,k-1}}{h_{n,k}}
|
||||||
|
&=\nu_n\frac{h_{n+1,k}}{h_{n,k}}
|
||||||
|
\qquad(1\le k\le n),\label{eq:term-generic}\\
|
||||||
|
d_1(n)&=-\nu_n
|
||||||
|
\frac{(n+\frac76)(n+\frac32)(n+\frac{11}{6})}
|
||||||
|
{8(2n+1)^3}.\label{eq:term-top}
|
||||||
|
\end{align}
|
||||||
|
The base row is not assumed: from the first component of \(C\),
|
||||||
|
\[
|
||||||
|
q_0(x)=\frac{18}{x}+\frac{159}{4},\qquad
|
||||||
|
Q_0(x)=xq_0(x)=18+\frac{159}{4}x,
|
||||||
|
\]
|
||||||
|
and therefore
|
||||||
|
\[
|
||||||
|
p_1(z)=(1-z)Q_0\!\left(-\frac{z}{1-z}\right)
|
||||||
|
=18\left(1-\frac{77}{24}z\right).
|
||||||
|
\]
|
||||||
|
Direct application of the four displayed \(\pi_r\) operators gives the
|
||||||
|
four base identities
|
||||||
|
\begin{equation}\label{eq:base-horizontal-row}
|
||||||
|
-zC\!\left(-\frac{z}{1-z}\right)
|
||||||
|
=\left.(\pi_0(\theta)p_1,\pi_1(\theta)p_1,
|
||||||
|
\pi_2(\theta)p_1,\pi_3(\theta)p_1)\right|_{n=1}.
|
||||||
|
\end{equation}
|
||||||
|
The fourth base equation is also direct:
|
||||||
|
\[
|
||||||
|
\left[
|
||||||
|
\theta(\theta-2)^3
|
||||||
|
-z(\theta-1)(\theta-\tfrac76)
|
||||||
|
(\theta-\tfrac32)(\theta-\tfrac{11}{6})
|
||||||
|
\right]p_1=0.
|
||||||
|
\]
|
||||||
|
Equivalently, if \(H_1=-zC(-z/(1-z))\), then all four components of
|
||||||
|
\[
|
||||||
|
\theta H_1+H_1\mathcal C_1=0
|
||||||
|
\]
|
||||||
|
vanish. The mandatory verifier checks both forms independently.
|
||||||
|
Moreover,
|
||||||
|
\[
|
||||||
|
\deg((d_0(\theta)+zd_1(\theta))p_n)\le n+1.
|
||||||
|
\]
|
||||||
|
Equations \eqref{eq:term-constant}--\eqref{eq:term-top} therefore prove,
|
||||||
|
coefficient by coefficient, that the right side of
|
||||||
|
\eqref{eq:terminating-step} is
|
||||||
|
\(\alpha_{n+1}\sum_{k=0}^{n+1}h_{n+1,k}z^k\).
|
||||||
|
Starting from \eqref{eq:base-horizontal-row},
|
||||||
|
\eqref{eq:full-gauge} propagates the horizontal form at every step.
|
||||||
|
This proves \eqref{eq:qhat} and \eqref{eq:normalization} for the actual
|
||||||
|
row \(CG_N\), not merely for a scalar surrogate.
|
||||||
|
The mandatory standalone checker independently expands the cleared
|
||||||
|
identities and rejects any nonzero coefficient.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\begin{corollary}[Positivity at the CM point]\label{cor:positivity}
|
\begin{corollary}[Positivity at the CM point]\label{cor:positivity}
|
||||||
|
|
@ -515,10 +769,19 @@ and therefore
|
||||||
\le10^4\left(\frac um\right)^{i-1}
|
\le10^4\left(\frac um\right)^{i-1}
|
||||||
\left(\frac u{m+1}\right)^{3-j}.
|
\left(\frac u{m+1}\right)^{3-j}.
|
||||||
\]
|
\]
|
||||||
For \(m\ge1\), \(u/m\le5\) and \(u/(m+1)\le5/2\); summing four entries in
|
For \(m\ge1\), \(u/m\le5\) and \(u/(m+1)\le5/2\). Because the exponent
|
||||||
each row gives the deliberately loose uniform bound
|
\(3-j\) is negative when \(j=4\), we use the exact case split
|
||||||
\[
|
\[
|
||||||
\|\mathcal B_m\|_\infty\le4\cdot10^8,\qquad
|
\left(\frac{u}{m+1}\right)^{3-j}\le
|
||||||
|
\begin{cases}
|
||||||
|
(5/2)^{3-j}\le25/4,&j\le3,\\[1mm]
|
||||||
|
1/2,&j=4,
|
||||||
|
\end{cases}
|
||||||
|
\]
|
||||||
|
where the second line follows from \(u/(m+1)=2+1/(m+1)\ge2\).
|
||||||
|
Thus every entry is at most \(7{,}812{,}500\), and summing each row gives
|
||||||
|
\[
|
||||||
|
\|\mathcal B_m\|_\infty\le31{,}250{,}000<4\cdot10^8,\qquad
|
||||||
\|M_0\|_\infty<10^7.
|
\|M_0\|_\infty<10^7.
|
||||||
\]
|
\]
|
||||||
The balancing telescopes:
|
The balancing telescopes:
|
||||||
|
|
@ -531,6 +794,23 @@ It follows that, for \(N\ge1\),
|
||||||
\max_{|x|=1/4}|\mathcal R_{N,r}(x)|
|
\max_{|x|=1/4}|\mathcal R_{N,r}(x)|
|
||||||
\le6\cdot10^{10}(N!)^2(4\cdot10^8)^{N-1}(1/4)^n.
|
\le6\cdot10^{10}(N!)^2(4\cdot10^8)^{N-1}(1/4)^n.
|
||||||
\end{equation}
|
\end{equation}
|
||||||
|
We now verify the analytic hypothesis behind the next step. On
|
||||||
|
\(|x|\le1/4\),
|
||||||
|
\[
|
||||||
|
\left|-\frac{x}{1-x}\right|\le\frac13<1,
|
||||||
|
\]
|
||||||
|
so the series defining \(y\) and its first three Euler derivatives are
|
||||||
|
holomorphic on a neighborhood of the closed disk. Because \(f=O(x)\),
|
||||||
|
the simple pole of \(C\) cancels in \(fC\), so \(\mathcal E_0\) is
|
||||||
|
holomorphic there. Inspection of \eqref{eq:deformed-matrix} shows that
|
||||||
|
each \(M_m\) is holomorphic off \(x=0\) in this disk and has at most a
|
||||||
|
simple pole at \(0\). Hence
|
||||||
|
\(\mathcal R_{N,r}=x^n(\mathcal E_N)_{r,1}\), with \(n=N+1\), is
|
||||||
|
holomorphic on the disk after removing its possible singularity at zero.
|
||||||
|
Proposition~\ref{prop:divisibility} strengthens its order there to at
|
||||||
|
least \(2n\). Therefore
|
||||||
|
\(\mathcal R_{N,r}(x)/x^{2n}\) has a removable singularity at zero and
|
||||||
|
is holomorphic on a neighborhood of the closed disk.
|
||||||
Applying the maximum principle to
|
Applying the maximum principle to
|
||||||
\(\mathcal R_{N,r}(x)/x^{2n}\) gives
|
\(\mathcal R_{N,r}(x)/x^{2n}\) gives
|
||||||
\begin{equation}\label{eq:cauchy}
|
\begin{equation}\label{eq:cauchy}
|
||||||
|
|
@ -552,9 +832,9 @@ Combining this with \eqref{eq:cauchy}, we obtain
|
||||||
\begin{equation}\label{eq:geometric-error}
|
\begin{equation}\label{eq:geometric-error}
|
||||||
\left|\frac{E_{N,r}(x_0)}{q_N(x_0)}\right|
|
\left|\frac{E_{N,r}(x_0)}{q_N(x_0)}\right|
|
||||||
=\left|\frac{\mathcal R_{N,r}(x_0)}{Q_N(x_0)}\right|
|
=\left|\frac{\mathcal R_{N,r}(x_0)}{Q_N(x_0)}\right|
|
||||||
\le C(x_0)\,\beta(x_0)^N,
|
\le K_0\,\beta(x_0)^N,
|
||||||
\end{equation}
|
\end{equation}
|
||||||
where \(C(x_0)<\infty\) and
|
where \(K_0<\infty\) is independent of \(N\) and
|
||||||
\[
|
\[
|
||||||
\beta(x_0)=
|
\beta(x_0)=
|
||||||
\frac{4\cdot10^8}{29}
|
\frac{4\cdot10^8}{29}
|
||||||
|
|
@ -592,9 +872,22 @@ Equation \eqref{eq:CM-value} therefore proves
|
||||||
|
|
||||||
\section{The other three official columns}
|
\section{The other three official columns}
|
||||||
|
|
||||||
For completeness, we recall the exact finite-frame reduction already used
|
All matrices in this section are evaluated at \(x=x_0=1/R\).
|
||||||
to establish convergence of the recurrence. The balanced transfer tends
|
For \(m\ge1\), retain
|
||||||
to
|
\[
|
||||||
|
D_m=\diag(1,m,m^2,m^3),\qquad
|
||||||
|
\mathcal B_m=D_m^{-1}M_mD_{m+1}/(m+1)^2,
|
||||||
|
\]
|
||||||
|
and, for any row \(a\), put
|
||||||
|
\[
|
||||||
|
Z_m(a)=\frac{aG_mD_m}{(m!)^2}.
|
||||||
|
\]
|
||||||
|
Then the balancing gives the exact recurrence
|
||||||
|
\begin{equation}\label{eq:balanced-row-recurrence}
|
||||||
|
Z_{m+1}(a)=Z_m(a)\mathcal B_m.
|
||||||
|
\end{equation}
|
||||||
|
Substitution in the displayed matrix shows, entry by entry, that
|
||||||
|
\(\mathcal B_m-\mathcal S=O(m^{-1})\), where
|
||||||
\[
|
\[
|
||||||
\mathcal S=
|
\mathcal S=
|
||||||
\begin{pmatrix}
|
\begin{pmatrix}
|
||||||
|
|
@ -611,94 +904,255 @@ Q_R(t)={}&R^2t^4-(64R^3-56R^2-4)t^3\\
|
||||||
&+(48R^2-262R+220)t^2-(12R-8)t+1.
|
&+(48R^2-262R+220)t^2-(12R-8)t+1.
|
||||||
\end{aligned}
|
\end{aligned}
|
||||||
\]
|
\]
|
||||||
The quartic is irreducible. Its spectral separation is also exact: on
|
On \(|t|=1\), the cubic coefficient strictly dominates the sum of the
|
||||||
\(|t|=1\), the absolute value of its cubic coefficient exceeds the sum of
|
other four coefficient magnitudes, because
|
||||||
the other coefficient magnitudes, because
|
|
||||||
\[
|
\[
|
||||||
(64R^3-56R^2-4)-(49R^2-250R+213)
|
(64R^3-56R^2-4)-(49R^2-250R+213)
|
||||||
=64R^3-105R^2+250R-217>0.
|
=64R^3-105R^2+250R-217>0.
|
||||||
\]
|
\]
|
||||||
Rouch\'e's theorem therefore places exactly three roots in \(|t|<1\) and
|
To count the roots without an irreducibility or root-finder call, consider
|
||||||
the remaining root \(\rho\) in \(|t|>1\). Hence \(\rho\) is the unique
|
|
||||||
root of maximal modulus.
|
|
||||||
|
|
||||||
We next remove any possible nonvanishing assumption about the denominator.
|
|
||||||
The positivity estimate above and \(Q_N=x_0^nq_N\) give
|
|
||||||
\begin{equation}\label{eq:q-lower}
|
|
||||||
q_N(x_0)\ge
|
|
||||||
18\cdot29^N(N!)^2
|
|
||||||
\left(\frac{1-x_0}{x_0}\right)^{N+1}.
|
|
||||||
\end{equation}
|
|
||||||
The scalar recurrence obtained from the first cyclic coordinate is of
|
|
||||||
Poincar\'e type after the \((N!)^2\) balancing. The discrete
|
|
||||||
Birkhoff--Poincar\'e theorem \([4,\text{ Chapters 3 and 5}]\) applies because
|
|
||||||
the balanced coefficients are rational in \(N\), have full expansions in
|
|
||||||
\(N^{-1}\), and the limiting spectrum is simple. If the coefficient of the
|
|
||||||
\(\rho\)-mode in \(q_N\) were zero, the three-root separation just proved
|
|
||||||
would give, for some \(\tau<1\),
|
|
||||||
\[
|
\[
|
||||||
|q_N(x_0)|\le K_\tau (N!)^2\tau^N.
|
H_s(t)=-(64R^3-56R^2-4)t^3+
|
||||||
|
s\{R^2t^4+(48R^2-262R+220)t^2-(12R-8)t+1\}.
|
||||||
\]
|
\]
|
||||||
This contradicts \eqref{eq:q-lower}. Thus the dominant denominator
|
The strict inequality above gives \(H_s(t)\ne0\) for
|
||||||
coefficient is nonzero by a wholly exact argument.
|
\(|t|=1\), \(0\le s\le1\). Thus the winding number of
|
||||||
|
\(H_s(e^{i\vartheta})\) about zero cannot change with \(s\); at \(s=0\)
|
||||||
|
it is \(3\). Hence \(Q_R=H_1\) has three zeros in \(|t|<1\) and one,
|
||||||
|
counted with multiplicity, in \(|t|>1\). Moreover
|
||||||
|
\[
|
||||||
|
Q_R(1)=-(64R^3-105R^2+274R-233)<0,\qquad
|
||||||
|
\lim_{t\to+\infty}Q_R(t)=+\infty.
|
||||||
|
\]
|
||||||
|
Consequently the unique exterior zero is a simple real number
|
||||||
|
\(\rho>1\).
|
||||||
|
|
||||||
It remains to transfer the first-column result to the other columns. For
|
\begin{lemma}[Explicit dominant-product dichotomy]
|
||||||
\(r\ge1\), put
|
\label{lem:dominant-product}
|
||||||
|
Fix \(\tau\) with
|
||||||
|
\[
|
||||||
|
\max_{\lambda\ne\rho}|\lambda|<\tau<1,
|
||||||
|
\]
|
||||||
|
Then there exist a late index \(m_0\), a linear functional \(\Lambda\) on
|
||||||
|
rows, nonzero scalars \(L_m\) independent of the row, and a left
|
||||||
|
\(\rho\)-eigenvector \(w\) of \(\mathcal S\) such that the following
|
||||||
|
alternatives hold:
|
||||||
|
\begin{align}
|
||||||
|
\Lambda(a)=0&\quad\Longrightarrow\quad
|
||||||
|
\|Z_m(a)\|\le K_a\tau^{m-m_0},\label{eq:exceptional-decay}\\
|
||||||
|
\Lambda(a)\ne0&\quad\Longrightarrow\quad
|
||||||
|
Z_m(a)=\Lambda(a)L_m\bigl(w+o_a(1)\bigr).
|
||||||
|
\label{eq:dominant-asymptotic}
|
||||||
|
\end{align}
|
||||||
|
\end{lemma}
|
||||||
|
|
||||||
|
\begin{proof}
|
||||||
|
Choose an invertible \(P\) with
|
||||||
|
\[
|
||||||
|
P^{-1}\mathcal SP=
|
||||||
|
\begin{pmatrix}\rho&0\\0&A\end{pmatrix},
|
||||||
|
\qquad\operatorname{spr}(A)<1.
|
||||||
|
\]
|
||||||
|
Choose \(\operatorname{spr}(A)<\theta<\tau\). For stable rows define
|
||||||
|
\[
|
||||||
|
\|\beta\|_\theta=\sum_{k=0}^{\infty}
|
||||||
|
\theta^{-k}\|\beta A^k\|_0.
|
||||||
|
\]
|
||||||
|
The finite Jordan identity
|
||||||
|
\[
|
||||||
|
J_\lambda^k=\sum_{\ell=0}^{s-1}
|
||||||
|
\binom{k}{\ell}\lambda^{k-\ell}N^\ell
|
||||||
|
\]
|
||||||
|
gives, for \(\operatorname{spr}(A)<\eta<\theta\),
|
||||||
|
\(\|A^k\|_0\le Ck^2\eta^k\); hence the series converges and
|
||||||
|
\[
|
||||||
|
\|\beta A\|_\theta
|
||||||
|
=\theta\sum_{k=1}^{\infty}\theta^{-k}\|\beta A^k\|_0
|
||||||
|
\le\theta\|\beta\|_\theta.
|
||||||
|
\]
|
||||||
|
Use the dual norm for stable columns.
|
||||||
|
|
||||||
|
Write
|
||||||
|
\[
|
||||||
|
T_m=P^{-1}\mathcal B_mP=
|
||||||
|
\begin{pmatrix}a_m&b_m\\c_m&E_m\end{pmatrix}.
|
||||||
|
\]
|
||||||
|
Then \(a_m\to\rho\), \(b_m,c_m\to0\), and \(E_m\to A\).
|
||||||
|
Choose
|
||||||
|
\[
|
||||||
|
\theta<d_*<\tau<1<a_*<\rho.
|
||||||
|
\]
|
||||||
|
For sufficiently large \(m_0\), a positive \(\epsilon\) makes, for
|
||||||
|
\(m\ge m_0\),
|
||||||
|
\begin{gather}
|
||||||
|
|a_m|\ge a_*,\quad\|E_m\|\le d_*,
|
||||||
|
\quad\|b_m\|,\|c_m\|\le\epsilon,\label{eq:block-bounds}\\
|
||||||
|
d_*+\epsilon<\tau,\quad a_*-\epsilon>1,\quad
|
||||||
|
d_*+\epsilon<a_*-\epsilon,\label{eq:block-separation}\\
|
||||||
|
q:=\frac{d_*}{a_*-\epsilon}
|
||||||
|
+\frac{(d_*+\epsilon)\epsilon}{(a_*-\epsilon)^2}<1.
|
||||||
|
\label{eq:graph-contraction-constant}
|
||||||
|
\end{gather}
|
||||||
|
For stable columns \(\|h\|\le1\), set
|
||||||
|
\[
|
||||||
|
\Psi_m(h)=\frac{E_mh-c_m}{a_m-b_mh}.
|
||||||
|
\]
|
||||||
|
Equations \eqref{eq:block-bounds}--\eqref{eq:block-separation} give
|
||||||
|
\[
|
||||||
|
\|\Psi_m(h)\|
|
||||||
|
\le\frac{d_*+\epsilon}{a_*-\epsilon}<1.
|
||||||
|
\]
|
||||||
|
For two such columns,
|
||||||
|
\[
|
||||||
|
\Psi_m(h)-\Psi_m(k)
|
||||||
|
=\frac{E_m(h-k)}{a_m-b_mh}
|
||||||
|
+\frac{(E_mk-c_m)b_m(h-k)}
|
||||||
|
{(a_m-b_mh)(a_m-b_mk)},
|
||||||
|
\]
|
||||||
|
so \eqref{eq:graph-contraction-constant} gives
|
||||||
|
\[
|
||||||
|
\|\Psi_m(h)-\Psi_m(k)\|\le q\|h-k\|.
|
||||||
|
\]
|
||||||
|
|
||||||
|
For \(M>m\), set \(h_M^{(M)}=0\) and recurse backward by
|
||||||
|
\(h_j^{(M)}=\Psi_j(h_{j+1}^{(M)})\). Then, for \(M'>M\),
|
||||||
|
\[
|
||||||
|
\|h_m^{(M')}-h_m^{(M)}\|\le2q^{M-m}.
|
||||||
|
\]
|
||||||
|
Thus \(h_m=\lim_{M\to\infty}h_m^{(M)}\) exists and satisfies
|
||||||
|
\begin{equation}\label{eq:graph-invariance}
|
||||||
|
h_ma_m+c_m=(h_mb_m+E_m)h_{m+1}.
|
||||||
|
\end{equation}
|
||||||
|
The defining recurrence gives the explicit bound
|
||||||
|
\[
|
||||||
|
\|h_m\|\le
|
||||||
|
\frac{\|E_m\|\|h_{m+1}\|+\|c_m\|}
|
||||||
|
{|a_m|-\|b_m\|}.
|
||||||
|
\]
|
||||||
|
Together with \(\|A\|_\theta/\rho<1\), this gives
|
||||||
|
\[
|
||||||
|
\limsup_{m\to\infty}\|h_m\|
|
||||||
|
\le\frac{\theta}{\rho}\limsup_{m\to\infty}\|h_m\|,
|
||||||
|
\qquad\text{hence}\qquad h_m\to0.
|
||||||
|
\]
|
||||||
|
|
||||||
|
Write
|
||||||
|
\[
|
||||||
|
U_m(a)=Z_m(a)P=(\alpha_m,\beta_m),\qquad
|
||||||
|
\xi_m=\alpha_m-\beta_mh_m,\qquad
|
||||||
|
d_m=a_m-b_mh_{m+1}.
|
||||||
|
\]
|
||||||
|
Using \eqref{eq:graph-invariance} in
|
||||||
|
\(U_{m+1}=U_mT_m\) gives the exact scalar equation
|
||||||
|
\[
|
||||||
|
\xi_{m+1}=d_m\xi_m.
|
||||||
|
\]
|
||||||
|
Define the composed seed functional and product
|
||||||
|
\[
|
||||||
|
\Lambda(a)=\alpha_{m_0}(a)-\beta_{m_0}(a)h_{m_0},\qquad
|
||||||
|
L_m=\prod_{\ell=m_0}^{m-1}d_\ell.
|
||||||
|
\]
|
||||||
|
Both are now explicit, \(\Lambda\) is linear, and
|
||||||
|
\(\xi_m=\Lambda(a)L_m\). Equations
|
||||||
|
\eqref{eq:block-bounds}--\eqref{eq:block-separation} ensure
|
||||||
|
\(d_m\ne0\).
|
||||||
|
|
||||||
|
If \(\Lambda(a)=0\), then \(\alpha_m=\beta_mh_m\) and
|
||||||
|
\[
|
||||||
|
\beta_{m+1}=\beta_m(E_m+h_mb_m),\qquad
|
||||||
|
\|\beta_{m+1}\|<(d_*+\epsilon)\|\beta_m\|
|
||||||
|
<\tau\|\beta_m\|,
|
||||||
|
\]
|
||||||
|
which proves \eqref{eq:exceptional-decay}.
|
||||||
|
|
||||||
|
If \(\Lambda(a)\ne0\), put \(r_m=\beta_m/\xi_m\). Exact substitution
|
||||||
|
gives
|
||||||
|
\[
|
||||||
|
r_{m+1}
|
||||||
|
=\frac{b_m+r_m(E_m+h_mb_m)}{d_m}.
|
||||||
|
\]
|
||||||
|
Here \(b_m/d_m\to0\) and
|
||||||
|
\((E_m+h_mb_m)/d_m\to A/\rho\), whose norm is below one.
|
||||||
|
Enlarge \(m_0\) once more, redefining \(\Lambda\) and \(L_m\) from this
|
||||||
|
new index, so that for some \(q_1<1\),
|
||||||
|
\[
|
||||||
|
\left\|\frac{E_m+h_mb_m}{d_m}\right\|\le q_1
|
||||||
|
\qquad(m\ge m_0).
|
||||||
|
\]
|
||||||
|
Then, for every \(m\ge m_0\),
|
||||||
|
\[
|
||||||
|
\|r_m\|\le q_1^{m-m_0}\|r_{m_0}\|
|
||||||
|
+\sum_{\ell=m_0}^{m-1}q_1^{m-1-\ell}
|
||||||
|
\left\|\frac{b_\ell}{d_\ell}\right\|\longrightarrow0.
|
||||||
|
\]
|
||||||
|
Since \(\alpha_m/\xi_m=1+r_mh_m\to1\),
|
||||||
|
\[
|
||||||
|
U_m(a)=\Lambda(a)L_m\bigl((1,0)+o_a(1)\bigr).
|
||||||
|
\]
|
||||||
|
Multiplying by \(P^{-1}\) proves
|
||||||
|
\eqref{eq:dominant-asymptotic} with
|
||||||
|
\[
|
||||||
|
w=(1,0)P^{-1},\qquad w\mathcal S=\rho w.
|
||||||
|
\]
|
||||||
|
\end{proof}
|
||||||
|
|
||||||
|
No GCD or irreducibility decision is needed to show that all four
|
||||||
|
coordinates of \(w\) are nonzero. Define the polynomial row \(w(t)\) by
|
||||||
\[
|
\[
|
||||||
\begin{aligned}
|
\begin{aligned}
|
||||||
F_r&=[\,\e_1,M_r\e_1,M_rM_{r+1}\e_1,
|
w_1(t)={}&Rt(Rt^2-7)+12R^2t^2+4t^2+44t+10,\\
|
||||||
M_rM_{r+1}M_{r+2}\e_1\,],\\
|
\frac{w_2(t)}2={}&R^2t((48R-27)t-28)
|
||||||
\gamma_{r,k}&=\prod_{\ell=1}^{k}(r+\ell)^2,\\
|
+(194R-108)t+40R-23,\\
|
||||||
C_r&=[\,\e_1,\mathcal B_r\e_1,
|
w_3(t)={}&R^2t((48R-17)t-8)
|
||||||
\mathcal B_r\mathcal B_{r+1}\e_1,
|
+(198R-68)t+71R-32,\\
|
||||||
\mathcal B_r\mathcal B_{r+1}\mathcal B_{r+2}\e_1\,].
|
w_4(t)={}&2R(8+(17+3R)t+4R^2t^2).
|
||||||
\end{aligned}
|
\end{aligned}
|
||||||
\]
|
\]
|
||||||
The balancing telescopes exactly:
|
Direct multiplication gives the exact polynomial identity
|
||||||
\[
|
\[
|
||||||
F_r=D(r)C_r\diag(\gamma_{r,0},\ldots,\gamma_{r,3}),
|
w(t)(tI-\mathcal S)=(Q_R(t),0,0,0).
|
||||||
\qquad
|
|
||||||
C_r\longrightarrow
|
|
||||||
C=[\,\e_1,\mathcal S\e_1,\mathcal S^2\e_1,\mathcal S^3\e_1\,].
|
|
||||||
\]
|
\]
|
||||||
The limiting cyclic frame is nonsingular:
|
At \(t=\rho\), this is a left \(\rho\)-eigenvector. The exterior
|
||||||
|
eigenspace is one-dimensional, so the vector in
|
||||||
|
Lemma~\ref{lem:dominant-product} may be rescaled to \(w(\rho)\), with the
|
||||||
|
inverse rescaling absorbed into \(L_m\). Since \(R>7\) and \(\rho>1\),
|
||||||
|
every displayed grouping is positive. Thus \(w_j(\rho)>0\) for
|
||||||
|
\(j=1,2,3,4\); below we abbreviate \(w_j=w_j(\rho)\).
|
||||||
|
|
||||||
|
Undoing the balancing in \eqref{eq:dominant-asymptotic} gives, whenever
|
||||||
|
\(\Lambda(a)\ne0\),
|
||||||
|
\begin{equation}\label{eq:all-column-asymptotic}
|
||||||
|
aG_m\e_j=(m!)^2m^{-(j-1)}
|
||||||
|
\Lambda(a)L_m\bigl(w_j+o_a(1)\bigr).
|
||||||
|
\end{equation}
|
||||||
|
It remains to verify that the two official rows are not exceptional.
|
||||||
|
The positivity estimate and \(Q_m=x_0^{m+1}q_m\) give
|
||||||
|
\begin{equation}\label{eq:q-lower}
|
||||||
|
\frac{q_m(x_0)}{(m!)^2}
|
||||||
|
\ge18(R-1)\,[29(R-1)]^m.
|
||||||
|
\end{equation}
|
||||||
|
If \(\Lambda(C)=0\), the first coordinate of
|
||||||
|
\eqref{eq:exceptional-decay} would contradict \eqref{eq:q-lower}.
|
||||||
|
Therefore
|
||||||
\[
|
\[
|
||||||
\det C
|
\Lambda(A_1)=S\Lambda(C)\ne0.
|
||||||
=-\frac{4(27R-11)(128R^2-149R-43)}{R^6}\ne0.
|
|
||||||
\]
|
\]
|
||||||
Thus \(F_r\) is invertible for all sufficiently large \(r\). If
|
If \(\Lambda(A_0)=0\), then
|
||||||
\(y_r(a)=aG_r\e_1\), exact inversion of this frame gives
|
\eqref{eq:exceptional-decay}, \eqref{eq:dominant-asymptotic}, and
|
||||||
|
\(|d_m|>1\) for large \(m\) would make the first-column quotient tend
|
||||||
|
to zero, contradicting \eqref{eq:first-column}. Hence
|
||||||
|
\(\Lambda(A_0)\ne0\) as well.
|
||||||
|
|
||||||
|
Because \(w_j>0\), equation \eqref{eq:all-column-asymptotic} first proves
|
||||||
|
that every \(Q_{m,j}\) is nonzero for all sufficiently large \(m\), and
|
||||||
|
only then permits division:
|
||||||
\[
|
\[
|
||||||
aG_r\e_j=r^{-(j-1)}
|
\lim_{m\to\infty}\frac{P_{m,j}}{Q_{m,j}}
|
||||||
\sum_{k=0}^{3}(C_r^{-1})_{k+1,j}
|
=\frac{\Lambda(A_0)}{\Lambda(A_1)}
|
||||||
\frac{y_{r+k}(a)}{\gamma_{r,k}}.
|
=\lim_{m\to\infty}\frac{P_{m,1}}{Q_{m,1}}
|
||||||
|
=\frac{\sqrt{10005}}{\pi}.
|
||||||
\]
|
\]
|
||||||
The same Birkhoff--Poincar\'e theorem supplies a linear dominant functional
|
We conclude:
|
||||||
\(\Lambda\) and an exponent \(\sigma\) such that, for fixed \(k\),
|
|
||||||
\[
|
|
||||||
\frac{y_{r+k}(a)}
|
|
||||||
{(r!)^2\rho^r r^\sigma\gamma_{r,k}}
|
|
||||||
\longrightarrow\Lambda(a)\rho^k.
|
|
||||||
\]
|
|
||||||
Consequently
|
|
||||||
\[
|
|
||||||
\frac{aG_r\e_j}
|
|
||||||
{(r!)^2\rho^r r^{\sigma-(j-1)}}
|
|
||||||
\longrightarrow\Lambda(a)\,\widetilde w_j,\qquad
|
|
||||||
\widetilde w=[1,\rho,\rho^2,\rho^3]C^{-1}.
|
|
||||||
\]
|
|
||||||
An explicit left eigenvector is obtained from the first row of
|
|
||||||
\(R^2\operatorname{adj}(tI-\mathcal S)\). Each of its four coordinate
|
|
||||||
polynomials is coprime to \(Q_R\); hence no coordinate vanishes at \(\rho\).
|
|
||||||
It is a nonzero multiple of \(\widetilde w\), so
|
|
||||||
\(\widetilde w_j\ne0\) for every \(j\). Applying the last limit to
|
|
||||||
\(a=A_0,A_1\), using the exact denominator nonvanishing above, gives
|
|
||||||
\[
|
|
||||||
\lim_{N\to\infty}\frac{P_{N,j}}{Q_{N,j}}
|
|
||||||
=\frac{\Lambda(A_0)}{\Lambda(A_1)}
|
|
||||||
\qquad(j=1,2,3,4).
|
|
||||||
\]
|
|
||||||
Equation \eqref{eq:first-column} evaluates this common ratio. We conclude:
|
|
||||||
|
|
||||||
\begin{theorem}[Ramanujan Challenge Problem 2.8]\label{thm:main}
|
\begin{theorem}[Ramanujan Challenge Problem 2.8]\label{thm:main}
|
||||||
For every official column \(j=1,2,3,4\),
|
For every official column \(j=1,2,3,4\),
|
||||||
|
|
@ -727,29 +1181,42 @@ The proof package contains the following certificates.
|
||||||
File & Exact obligation\\
|
File & Exact obligation\\
|
||||||
\midrule
|
\midrule
|
||||||
\path{p28_full_closure_certificate.wl}
|
\path{p28_full_closure_certificate.wl}
|
||||||
& Authoritative differential gauge; nonterminating tail contiguity;
|
& Optional independent Wolfram cross-check of the differential gauge and
|
||||||
terminating adjoint equation; coefficientwise \(n\)-contiguity;
|
hypergeometric closure.\\
|
||||||
normalization and top boundary; exact spectral and cyclic-frame closure.\\
|
\path{p28_standalone_equations.py}
|
||||||
|
& Mandatory dependency-free expansion of the four cleared Ore
|
||||||
|
factorizations, the tail coefficient equations, the terminating base,
|
||||||
|
generic, and top identities, ascension, and the \(\F32\) equation.\\
|
||||||
|
\path{p28_dominant_product_algebra.py}
|
||||||
|
& Mandatory dependency-free verification of
|
||||||
|
\(\mathcal B_m=\mathcal S+O(m^{-1})\), the characteristic polynomial,
|
||||||
|
the root-separation inequalities, the left-eigenvector identity, and
|
||||||
|
the four positive coordinate rewrites.\\
|
||||||
\path{p28_kernel_contiguity_certificate.sage}
|
\path{p28_kernel_contiguity_certificate.sage}
|
||||||
& Independent coefficient/Ore proof of \(M_Nk_{N+1}=k_N\).\\
|
& Optional independent Sage check of the four displayed
|
||||||
|
factorizations; it performs no Ore division.\\
|
||||||
\path{p28_lattice_hypotheses_certificate.sage}
|
\path{p28_lattice_hypotheses_certificate.sage}
|
||||||
& Rank-one factorization, tail direction, and transformed ODE identities.\\
|
& Optional exact cross-check of the rank-one factorization, tail
|
||||||
|
direction, and transformed ODE identities.\\
|
||||||
\path{p28_convergence_constants.py}
|
\path{p28_convergence_constants.py}
|
||||||
& Exact rational verification of the coefficient bounds,
|
& Exact rational verification of the coefficient bounds,
|
||||||
\(\alpha_{n+1}/\alpha_n\ge29n^2\), and \(\beta(x_0)<1\).\\
|
\(\alpha_{n+1}/\alpha_n\ge29n^2\), and \(\beta(x_0)<1\).\\
|
||||||
\path{all_four_columns_certificate.sage}
|
\path{all_four_columns_certificate.sage}
|
||||||
& Balanced limit, Rouch\'e separation, nonzero eigenvector coordinates,
|
& Optional Sage cross-check of the balanced limit and exterior-root
|
||||||
and invertible cyclic frame.\\
|
algebra; the analytic contraction is proved in Lemma~\ref{lem:dominant-product}.\\
|
||||||
\path{p28_parametric_pade_probe.py}
|
\path{p28_parametric_pade_probe.py}
|
||||||
& Dependency-free finite exact regression of the predicted valuations.\\
|
& Diagnostic finite exact regression of the predicted valuations; it is
|
||||||
|
not used as proof of an all-\(N\) statement.\\
|
||||||
\bottomrule
|
\bottomrule
|
||||||
\end{tabular}
|
\end{tabular}
|
||||||
\end{center}
|
\end{center}
|
||||||
|
|
||||||
The Wolfram certificate performs symbolic identities over
|
The two mandatory algebra checkers use only the standard library's
|
||||||
\(\Q(n,z)\); it uses no numerical samples. The Python constants check uses
|
\texttt{fractions.Fraction}, sparse coefficient dictionaries, and explicit
|
||||||
only the standard library's \texttt{fractions.Fraction}. The SageMath
|
addition, multiplication, differentiation, and determinant expansion.
|
||||||
files are independent exact cross-checks.
|
They invoke no division algorithm, factorizer, root finder, special-function
|
||||||
|
library, or numerical sample. Wolfram Language and SageMath are optional
|
||||||
|
independent cross-checks, not a trust requirement.
|
||||||
|
|
||||||
\section*{References}
|
\section*{References}
|
||||||
\addcontentsline{toc}{section}{References}
|
\addcontentsline{toc}{section}{References}
|
||||||
|
|
@ -758,6 +1225,10 @@ files are independent exact cross-checks.
|
||||||
\item D. V. Chudnovsky and G. V. Chudnovsky,
|
\item D. V. Chudnovsky and G. V. Chudnovsky,
|
||||||
``Approximations and complex multiplication according to Ramanujan,''
|
``Approximations and complex multiplication according to Ramanujan,''
|
||||||
in \emph{Ramanujan Revisited}, Academic Press, 1988, pp.~375--472.
|
in \emph{Ramanujan Revisited}, Academic Press, 1988, pp.~375--472.
|
||||||
|
\item L. Milla,
|
||||||
|
``A detailed proof of the Chudnovsky formula with means of basic
|
||||||
|
complex analysis,'' arXiv:1809.00533v6, 2021,
|
||||||
|
\href{https://arxiv.org/abs/1809.00533}{arXiv:1809.00533}.
|
||||||
\item J. L. Fields,
|
\item J. L. Fields,
|
||||||
``Rational approximations to generalized hypergeometric functions,''
|
``Rational approximations to generalized hypergeometric functions,''
|
||||||
\emph{Mathematics of Computation} \textbf{19} (1965), 606--624,
|
\emph{Mathematics of Computation} \textbf{19} (1965), 606--624,
|
||||||
|
|
@ -767,9 +1238,6 @@ files are independent exact cross-checks.
|
||||||
``Hermite--Pad\'e approximants of generalized hypergeometric
|
``Hermite--Pad\'e approximants of generalized hypergeometric
|
||||||
functions,'' \emph{Russian Acad. Sci. Sb. Math.}
|
functions,'' \emph{Russian Acad. Sci. Sb. Math.}
|
||||||
\textbf{83} (1995), 189--219.
|
\textbf{83} (1995), 189--219.
|
||||||
\item S. Bodine and D. A. Lutz,
|
|
||||||
\emph{Asymptotic Integration of Differential and Difference Equations},
|
|
||||||
Lecture Notes in Mathematics 2129, Springer, 2015, Chapters 3 and 5.
|
|
||||||
\item The Ramanujan Machine,
|
\item The Ramanujan Machine,
|
||||||
\href{https://www.ramanujanmachine.com/ramanujan-challenge/}
|
\href{https://www.ramanujanmachine.com/ramanujan-challenge/}
|
||||||
{Ramanujan Challenge}, Problem 2.8.
|
{Ramanujan Challenge}, Problem 2.8.
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue