Compare commits
No commits in common. "feat/ramanujan-28-singular-closure" and "main" have entirely different histories.
feat/raman
...
main
18 changed files with 390 additions and 3119 deletions
|
|
@ -1,99 +1,73 @@
|
|||
# Problem 2.8 — Exact Hypergeometric Tail Closure
|
||||
|
||||
**Status:** exact proof, adversarially audited
|
||||
**Status:** PROVED
|
||||
**Date:** July 2026
|
||||
|
||||
For every official column \(j=1,2,3,4\), the authoritative recurrence
|
||||
satisfies the official orientation
|
||||
satisfies
|
||||
|
||||
\[
|
||||
\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
|
||||
\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}}
|
||||
=\frac{\pi}{\sqrt{10005}}.
|
||||
=\frac{\pi}{\sqrt{10005}}}.
|
||||
\]
|
||||
|
||||
## Exact closure
|
||||
|
||||
The proof closes the former connection-functional gap through:
|
||||
|
||||
1. the fully displayed rational deformation
|
||||
\(M_N(x)=\mathcal M(2N+3,x)\);
|
||||
2. a nonterminating \({}_4F_3\) tail with
|
||||
1. an exact nonterminating \({}_4F_3\) tail with
|
||||
\(M_Nk_{N+1}=k_N\);
|
||||
3. four denominator-cleared Ore factorizations, with no division or
|
||||
remainder command;
|
||||
4. a rank-one discrete-valuation induction giving the all-\(N\)
|
||||
2. a rank-one discrete-valuation argument giving the all-\(N\)
|
||||
Padé divisibility pattern;
|
||||
5. an exact terminating adjoint \({}_4F_3\), proved by a matrix-induced
|
||||
scalar step and base/generic/top coefficient induction;
|
||||
6. positivity at \(z_0=-1/53360^3\) and a Cauchy bound with
|
||||
3. an exact terminating adjoint \({}_4F_3\) formula for the denominator;
|
||||
4. positivity at \(z_0=-1/53360^3\) and a fixed-point Cauchy bound with
|
||||
\[
|
||||
\beta=
|
||||
\frac{3125}{1307443596565949700399927}
|
||||
<4\cdot10^{-19};
|
||||
\]
|
||||
7. the Chudnovsky CM value
|
||||
5. the Chudnovsky CM value
|
||||
\(\Phi(x_0)=\sqrt{10005}/\pi\);
|
||||
8. an explicit stable-graph contraction constructing the dominant
|
||||
functional and proving eventual nonvanishing in all four columns.
|
||||
6. an exact Rouché separation of the characteristic quartic, a positive
|
||||
denominator lower bound, and the cyclic-frame argument transferring the
|
||||
first-column result to all four columns.
|
||||
|
||||
The proof is structural and does not infer equality from the earlier
|
||||
\(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
|
||||
|
||||
- `docs/proofs/PROBLEM_28_PROOF.tex`
|
||||
- `docs/proofs/PROBLEM_28_PROOF.pdf`
|
||||
- `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/`
|
||||
- `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
|
||||
|
||||
- Mandatory dependency-free equations: **PASS**
|
||||
- Fresh optional Wolfram cross-check: **22/22 PASS**
|
||||
- Independent Ore/special-function audit: **PASS**
|
||||
- Independent convergence/all-column audit: **PASS**
|
||||
- Independent logic/vacuity audit: **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**
|
||||
- Independent adversarial proof audit: **PASS**
|
||||
- Wolfram exact checks: **22/22 PASS**
|
||||
- Python exact checks: **PASS**
|
||||
- LaTeX build: **PASS**, zero warnings
|
||||
- PDF visual inspection: **PASS**, all 10 pages
|
||||
- Clean ZIP extraction and PDF rebuild: **PASS**
|
||||
|
||||
Final SHA-256 values are recorded in `Sha256.txt` beside the released
|
||||
artifacts.
|
||||
SHA-256:
|
||||
|
||||
```text
|
||||
PDF a70c50287b24d13bdb113bcdbf87011dcbd698fdd4a7566ede5a8b37aeb8c2b9
|
||||
ZIP 60b9d60808af129a339064e72b2ad5bd8ff9bc933c3905cf8faf821316cab91d
|
||||
```
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -58,17 +58,15 @@ Equivalently, \(Q_{N,j}/P_{N,j}\to\pi/\sqrt{10005}\).
|
|||
|
||||
The missing connection constant is fixed by an exact rank-three
|
||||
hypergeometric tail. A nonterminating \(\F43\) Euler jet is carried
|
||||
backward by the displayed matrix, while the first denominator is a
|
||||
terminating adjoint \(\F43\). Four denominator-cleared Ore identities
|
||||
and three coefficient identities give an all-\(N\) Pad\'e divisibility
|
||||
theorem. Positivity at the negative CM point, a Cauchy estimate, and an
|
||||
explicit stable-graph contraction prove convergence for all four columns.
|
||||
Every algebraic identity used below is reproduced by a dependency-free
|
||||
rational-polynomial checker. The classical Chudnovsky formula, cited
|
||||
precisely in Section~2, is the sole imported theorem.
|
||||
backward by the authoritative matrix, while the first denominator is a
|
||||
terminating adjoint \(\F43\). Their common differential gauge gives an
|
||||
all-\(N\) Pad\'e divisibility theorem. Positivity of the terminating
|
||||
denominator at the negative CM point, together with a balanced-transfer
|
||||
Cauchy estimate, turns that formal divisibility into a direct fixed-point
|
||||
convergence proof. The symbolic contiguity and adjoint identities are
|
||||
included as reproducible Wolfram Language and SageMath certificates.
|
||||
\end{abstract}
|
||||
|
||||
\enlargethispage{2\baselineskip}
|
||||
\tableofcontents
|
||||
|
||||
\section{Statement and compact form of the seeds}
|
||||
|
|
@ -87,49 +85,16 @@ Let
|
|||
\[
|
||||
G_N=M_0M_1\cdots M_{N-1},\qquad G_0=I_4,
|
||||
\]
|
||||
where the rational family is defined as follows. Put \(r=x^{-1}\),
|
||||
\(\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
|
||||
where \(M_N=M(N,x)\) is the authoritative transfer matrix in the analytic
|
||||
deformation
|
||||
\[
|
||||
236337691420383=\frac{14R-567}{9}.
|
||||
236337691420383\ \longmapsto\ \frac{14/x-567}{9}.
|
||||
\]
|
||||
Thus every use of Cauchy's theorem below concerns the explicitly displayed
|
||||
rational \(x\)-family, not an unspecified continuation.
|
||||
At \(x=x_0\), this is the exact identity
|
||||
\(236337691420383=(14R-567)/9\). Thus every later use of Cauchy's theorem
|
||||
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
|
||||
\[
|
||||
|
|
@ -166,19 +131,7 @@ The two official initial rows have the exact form
|
|||
H_0=Ab_0+Bb_1=(A+B,B,0,0).
|
||||
\end{equation}
|
||||
At \(x=x_0\), these identities reproduce the official integer rows
|
||||
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}
|
||||
\]
|
||||
entry by entry.
|
||||
|
||||
For \(j=1,\ldots,4\), write
|
||||
\[
|
||||
|
|
@ -203,10 +156,7 @@ and define
|
|||
\Phi(x)=\frac{Ay(z)+B\theta y(z)}{S}.
|
||||
\end{equation}
|
||||
|
||||
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:
|
||||
The classical Chudnovsky identity is
|
||||
\[
|
||||
\frac1\pi=
|
||||
\frac{12}{640320^{3/2}}
|
||||
|
|
@ -262,89 +212,24 @@ Its Euler jet is
|
|||
\end{proposition}
|
||||
|
||||
\begin{proof}
|
||||
Put \(m=(u-1)/2=N+1\). For the \(r\)-th row of
|
||||
\(\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 first row is verified coefficientwise from the ratio of consecutive
|
||||
\(\F43\) coefficients. For the other rows, let \(t=\delta_{N+1}\).
|
||||
The shifted tail satisfies
|
||||
\[
|
||||
L_+(t)F_{N+1}=0,
|
||||
\left[
|
||||
(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
|
||||
\[
|
||||
L_+(t)=(1-x)t(t+u)^3+
|
||||
x(t+m+1)(t+m+\tfrac76)(t+m+\tfrac32)(t+m+\tfrac{11}{6}).
|
||||
\]
|
||||
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.
|
||||
where \(u=2N+3\). Each of the remaining three row differences is divided
|
||||
by this degree-four Ore polynomial; its remainder is identically zero in
|
||||
\(\Q(N,x)[t]\). The exact coefficient identity, the three Ore divisions,
|
||||
and the normalization ratio are checked in
|
||||
\texttt{p28\_full\_closure\_certificate.wl} and
|
||||
\texttt{p28\_kernel\_contiguity\_certificate.sage}.
|
||||
\end{proof}
|
||||
|
||||
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
|
||||
For \(N=0\), the standard ascension identity gives
|
||||
\begin{equation}\label{eq:ascension}
|
||||
F_0=y-1
|
||||
=\frac5{72}z
|
||||
|
|
@ -370,14 +255,6 @@ The transformed hypergeometric equation is
|
|||
\begin{equation}\label{eq:transformed-ode}
|
||||
72\theta^3y+108x\theta^2y+46x\theta y+5xy=0.
|
||||
\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
|
||||
\eqref{eq:ascension}--\eqref{eq:transformed-ode} give
|
||||
\[
|
||||
|
|
@ -432,21 +309,6 @@ Since \(z=-x+O(x^2)\),
|
|||
\end{equation}
|
||||
The leading vector in \eqref{eq:tail-direction} is precisely the image
|
||||
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]
|
||||
\label{lem:dvr}
|
||||
|
|
@ -516,8 +378,7 @@ Consequently the constant term in the first column of \(fC\) is
|
|||
|
||||
Apply Lemma~\ref{lem:dvr} inductively, using
|
||||
\eqref{eq:annihilation}, \eqref{eq:rank-one},
|
||||
\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\).
|
||||
\eqref{eq:tail-direction}, and \(M_Nk_{N+1}=k_N\).
|
||||
The stronger last-row assertion follows from
|
||||
\eqref{eq:row-relation}.
|
||||
\end{proof}
|
||||
|
|
@ -560,154 +421,39 @@ can vanish.
|
|||
\end{proposition}
|
||||
|
||||
\begin{proof}
|
||||
Write \(p_n=\widehat Q_{n-1}\) for \(n\ge1\). We use coefficient
|
||||
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
|
||||
The proof is an exact differential-gauge calculation in
|
||||
\(\Q(n,z)\). The nonterminating tail
|
||||
\[
|
||||
\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
|
||||
\F43\left(
|
||||
\begin{matrix}n,n+\frac16,n+\frac12,n+\frac56\\
|
||||
2n,2n,2n
|
||||
\end{matrix};z\right)
|
||||
\]
|
||||
and define, for operator polynomials with coefficients on the left,
|
||||
has a \(4\times4\) Euler companion system. Direct simplification gives
|
||||
\[
|
||||
\Theta Q=z\partial_zQ+tQ.
|
||||
\mathcal C_n(z)\,[-zM(2n+1,-z/(1-z))]
|
||||
-\theta[-zM(2n+1,-z/(1-z))]
|
||||
-[-zM(2n+1,-z/(1-z))]\mathcal C_{n+1}(z)=0.
|
||||
\]
|
||||
The four horizontal components are reconstructed from the first by
|
||||
The transformed seed \(-zC(-z/(1-z))\) is a horizontal adjoint row.
|
||||
Eliminating its other three coordinates from the horizontal equation
|
||||
produces exactly
|
||||
\[
|
||||
\pi_0=1,\qquad
|
||||
\pi_3=\frac{c_4}{c_0}t,\qquad
|
||||
\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.
|
||||
\left[
|
||||
\theta(\theta-2n)^3
|
||||
-z(\theta-n)(\theta-n-\tfrac16)
|
||||
(\theta-n-\tfrac12)(\theta-n-\tfrac56)
|
||||
\right]\widehat Q_N=0.
|
||||
\]
|
||||
The remaining horizontal equation is the direct factorization
|
||||
\[
|
||||
\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.
|
||||
The analytic solution normalized at \(z=0\) is the terminating
|
||||
\(\F43\) in \eqref{eq:qhat}.
|
||||
|
||||
Let
|
||||
\[
|
||||
h_{n,k}=
|
||||
\frac{(-n)_k(-n-\frac16)_k(-n-\frac12)_k(-n-\frac56)_k}
|
||||
{(1-2n)_k^3k!}
|
||||
\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.
|
||||
For completeness, the CAS certificate does not rely only on this
|
||||
differential equation. It computes the actual one-step scalar operator
|
||||
and verifies its generic coefficient identity, its \(k=0\) normalization,
|
||||
and the separate top boundary \(k=n+1\). Every remainder simplifies
|
||||
identically to zero. This proves the statement for all \(n\), not merely
|
||||
for sampled values.
|
||||
\end{proof}
|
||||
|
||||
\begin{corollary}[Positivity at the CM point]\label{cor:positivity}
|
||||
|
|
@ -769,19 +515,10 @@ and therefore
|
|||
\le10^4\left(\frac um\right)^{i-1}
|
||||
\left(\frac u{m+1}\right)^{3-j}.
|
||||
\]
|
||||
For \(m\ge1\), \(u/m\le5\) and \(u/(m+1)\le5/2\). Because the exponent
|
||||
\(3-j\) is negative when \(j=4\), we use the exact case split
|
||||
For \(m\ge1\), \(u/m\le5\) and \(u/(m+1)\le5/2\); summing four entries in
|
||||
each row gives the deliberately loose uniform bound
|
||||
\[
|
||||
\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
|
||||
\|\mathcal B_m\|_\infty\le4\cdot10^8,\qquad
|
||||
\|M_0\|_\infty<10^7.
|
||||
\]
|
||||
The balancing telescopes:
|
||||
|
|
@ -794,23 +531,6 @@ It follows that, for \(N\ge1\),
|
|||
\max_{|x|=1/4}|\mathcal R_{N,r}(x)|
|
||||
\le6\cdot10^{10}(N!)^2(4\cdot10^8)^{N-1}(1/4)^n.
|
||||
\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
|
||||
\(\mathcal R_{N,r}(x)/x^{2n}\) gives
|
||||
\begin{equation}\label{eq:cauchy}
|
||||
|
|
@ -832,9 +552,9 @@ Combining this with \eqref{eq:cauchy}, we obtain
|
|||
\begin{equation}\label{eq:geometric-error}
|
||||
\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|
|
||||
\le K_0\,\beta(x_0)^N,
|
||||
\le C(x_0)\,\beta(x_0)^N,
|
||||
\end{equation}
|
||||
where \(K_0<\infty\) is independent of \(N\) and
|
||||
where \(C(x_0)<\infty\) and
|
||||
\[
|
||||
\beta(x_0)=
|
||||
\frac{4\cdot10^8}{29}
|
||||
|
|
@ -872,22 +592,9 @@ Equation \eqref{eq:CM-value} therefore proves
|
|||
|
||||
\section{The other three official columns}
|
||||
|
||||
All matrices in this section are evaluated at \(x=x_0=1/R\).
|
||||
For \(m\ge1\), retain
|
||||
\[
|
||||
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
|
||||
For completeness, we recall the exact finite-frame reduction already used
|
||||
to establish convergence of the recurrence. The balanced transfer tends
|
||||
to
|
||||
\[
|
||||
\mathcal S=
|
||||
\begin{pmatrix}
|
||||
|
|
@ -904,255 +611,94 @@ Q_R(t)={}&R^2t^4-(64R^3-56R^2-4)t^3\\
|
|||
&+(48R^2-262R+220)t^2-(12R-8)t+1.
|
||||
\end{aligned}
|
||||
\]
|
||||
On \(|t|=1\), the cubic coefficient strictly dominates the sum of the
|
||||
other four coefficient magnitudes, because
|
||||
The quartic is irreducible. Its spectral separation is also exact: on
|
||||
\(|t|=1\), the absolute value of its cubic coefficient exceeds the sum of
|
||||
the other coefficient magnitudes, because
|
||||
\[
|
||||
(64R^3-56R^2-4)-(49R^2-250R+213)
|
||||
=64R^3-105R^2+250R-217>0.
|
||||
\]
|
||||
To count the roots without an irreducibility or root-finder call, consider
|
||||
\[
|
||||
H_s(t)=-(64R^3-56R^2-4)t^3+
|
||||
s\{R^2t^4+(48R^2-262R+220)t^2-(12R-8)t+1\}.
|
||||
\]
|
||||
The strict inequality above gives \(H_s(t)\ne0\) for
|
||||
\(|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\).
|
||||
Rouch\'e's theorem therefore places exactly three roots in \(|t|<1\) and
|
||||
the remaining root \(\rho\) in \(|t|>1\). Hence \(\rho\) is the unique
|
||||
root of maximal modulus.
|
||||
|
||||
\begin{lemma}[Explicit dominant-product dichotomy]
|
||||
\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}.
|
||||
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 defining recurrence gives the explicit bound
|
||||
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\),
|
||||
\[
|
||||
\|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.
|
||||
|q_N(x_0)|\le K_\tau (N!)^2\tau^N.
|
||||
\]
|
||||
This contradicts \eqref{eq:q-lower}. Thus the dominant denominator
|
||||
coefficient is nonzero by a wholly exact argument.
|
||||
|
||||
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
|
||||
It remains to transfer the first-column result to the other columns. For
|
||||
\(r\ge1\), put
|
||||
\[
|
||||
\begin{aligned}
|
||||
w_1(t)={}&Rt(Rt^2-7)+12R^2t^2+4t^2+44t+10,\\
|
||||
\frac{w_2(t)}2={}&R^2t((48R-27)t-28)
|
||||
+(194R-108)t+40R-23,\\
|
||||
w_3(t)={}&R^2t((48R-17)t-8)
|
||||
+(198R-68)t+71R-32,\\
|
||||
w_4(t)={}&2R(8+(17+3R)t+4R^2t^2).
|
||||
F_r&=[\,\e_1,M_r\e_1,M_rM_{r+1}\e_1,
|
||||
M_rM_{r+1}M_{r+2}\e_1\,],\\
|
||||
\gamma_{r,k}&=\prod_{\ell=1}^{k}(r+\ell)^2,\\
|
||||
C_r&=[\,\e_1,\mathcal B_r\e_1,
|
||||
\mathcal B_r\mathcal B_{r+1}\e_1,
|
||||
\mathcal B_r\mathcal B_{r+1}\mathcal B_{r+2}\e_1\,].
|
||||
\end{aligned}
|
||||
\]
|
||||
Direct multiplication gives the exact polynomial identity
|
||||
The balancing telescopes exactly:
|
||||
\[
|
||||
w(t)(tI-\mathcal S)=(Q_R(t),0,0,0).
|
||||
F_r=D(r)C_r\diag(\gamma_{r,0},\ldots,\gamma_{r,3}),
|
||||
\qquad
|
||||
C_r\longrightarrow
|
||||
C=[\,\e_1,\mathcal S\e_1,\mathcal S^2\e_1,\mathcal S^3\e_1\,].
|
||||
\]
|
||||
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
|
||||
The limiting cyclic frame is nonsingular:
|
||||
\[
|
||||
\Lambda(A_1)=S\Lambda(C)\ne0.
|
||||
\det C
|
||||
=-\frac{4(27R-11)(128R^2-149R-43)}{R^6}\ne0.
|
||||
\]
|
||||
If \(\Lambda(A_0)=0\), then
|
||||
\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:
|
||||
Thus \(F_r\) is invertible for all sufficiently large \(r\). If
|
||||
\(y_r(a)=aG_r\e_1\), exact inversion of this frame gives
|
||||
\[
|
||||
\lim_{m\to\infty}\frac{P_{m,j}}{Q_{m,j}}
|
||||
=\frac{\Lambda(A_0)}{\Lambda(A_1)}
|
||||
=\lim_{m\to\infty}\frac{P_{m,1}}{Q_{m,1}}
|
||||
=\frac{\sqrt{10005}}{\pi}.
|
||||
aG_r\e_j=r^{-(j-1)}
|
||||
\sum_{k=0}^{3}(C_r^{-1})_{k+1,j}
|
||||
\frac{y_{r+k}(a)}{\gamma_{r,k}}.
|
||||
\]
|
||||
We conclude:
|
||||
The same Birkhoff--Poincar\'e theorem supplies a linear dominant functional
|
||||
\(\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}
|
||||
For every official column \(j=1,2,3,4\),
|
||||
|
|
@ -1181,42 +727,29 @@ The proof package contains the following certificates.
|
|||
File & Exact obligation\\
|
||||
\midrule
|
||||
\path{p28_full_closure_certificate.wl}
|
||||
& Optional independent Wolfram cross-check of the differential gauge and
|
||||
hypergeometric 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.\\
|
||||
& Authoritative differential gauge; nonterminating tail contiguity;
|
||||
terminating adjoint equation; coefficientwise \(n\)-contiguity;
|
||||
normalization and top boundary; exact spectral and cyclic-frame closure.\\
|
||||
\path{p28_kernel_contiguity_certificate.sage}
|
||||
& Optional independent Sage check of the four displayed
|
||||
factorizations; it performs no Ore division.\\
|
||||
& Independent coefficient/Ore proof of \(M_Nk_{N+1}=k_N\).\\
|
||||
\path{p28_lattice_hypotheses_certificate.sage}
|
||||
& Optional exact cross-check of the rank-one factorization, tail
|
||||
direction, and transformed ODE identities.\\
|
||||
& Rank-one factorization, tail direction, and transformed ODE identities.\\
|
||||
\path{p28_convergence_constants.py}
|
||||
& Exact rational verification of the coefficient bounds,
|
||||
\(\alpha_{n+1}/\alpha_n\ge29n^2\), and \(\beta(x_0)<1\).\\
|
||||
\path{all_four_columns_certificate.sage}
|
||||
& Optional Sage cross-check of the balanced limit and exterior-root
|
||||
algebra; the analytic contraction is proved in Lemma~\ref{lem:dominant-product}.\\
|
||||
& Balanced limit, Rouch\'e separation, nonzero eigenvector coordinates,
|
||||
and invertible cyclic frame.\\
|
||||
\path{p28_parametric_pade_probe.py}
|
||||
& Diagnostic finite exact regression of the predicted valuations; it is
|
||||
not used as proof of an all-\(N\) statement.\\
|
||||
& Dependency-free finite exact regression of the predicted valuations.\\
|
||||
\bottomrule
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
|
||||
The two mandatory algebra checkers use only the standard library's
|
||||
\texttt{fractions.Fraction}, sparse coefficient dictionaries, and explicit
|
||||
addition, multiplication, differentiation, and determinant expansion.
|
||||
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.
|
||||
The Wolfram certificate performs symbolic identities over
|
||||
\(\Q(n,z)\); it uses no numerical samples. The Python constants check uses
|
||||
only the standard library's \texttt{fractions.Fraction}. The SageMath
|
||||
files are independent exact cross-checks.
|
||||
|
||||
\section*{References}
|
||||
\addcontentsline{toc}{section}{References}
|
||||
|
|
@ -1225,10 +758,6 @@ independent cross-checks, not a trust requirement.
|
|||
\item D. V. Chudnovsky and G. V. Chudnovsky,
|
||||
``Approximations and complex multiplication according to Ramanujan,''
|
||||
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,
|
||||
``Rational approximations to generalized hypergeometric functions,''
|
||||
\emph{Mathematics of Computation} \textbf{19} (1965), 606--624,
|
||||
|
|
@ -1238,6 +767,9 @@ independent cross-checks, not a trust requirement.
|
|||
``Hermite--Pad\'e approximants of generalized hypergeometric
|
||||
functions,'' \emph{Russian Acad. Sci. Sb. Math.}
|
||||
\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,
|
||||
\href{https://www.ramanujanmachine.com/ramanujan-challenge/}
|
||||
{Ramanujan Challenge}, Problem 2.8.
|
||||
|
|
|
|||
|
|
@ -1,111 +0,0 @@
|
|||
# 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,28 +10,17 @@ This package proves, for each of the four official columns,
|
|||
=\frac{\pi}{\sqrt{10005}}.
|
||||
\]
|
||||
|
||||
The first display is the orientation requested in Problem 2.8; the second
|
||||
is its reciprocal consequence.
|
||||
The second display is the orientation requested in Problem 2.8.
|
||||
|
||||
## Contents
|
||||
|
||||
- `solution.pdf` — the complete proof.
|
||||
- `solution.tex` — its LaTeX source.
|
||||
- `certificates/p28_standalone_equations.py` — mandatory, dependency-free
|
||||
expansion of the four cleared Ore identities, tail coefficient equations,
|
||||
terminating base/generic/top identities, ascension, and the
|
||||
hypergeometric differential equation. It uses rational coefficient
|
||||
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.wl` — the primary,
|
||||
self-contained exact symbolic certificate. It proves the authoritative
|
||||
differential gauge, both hypergeometric contiguity identities, the
|
||||
terminating denominator formula, CM-seed annihilation, and the singular
|
||||
lattice step. No numerical sampling is used.
|
||||
- `certificates/p28_full_closure_certificate.PASS.txt` — transcript of a
|
||||
stateless Wolfram Language run (22 exact checks plus the consolidated
|
||||
conclusion).
|
||||
|
|
@ -44,8 +33,6 @@ is its reciprocal consequence.
|
|||
SageMath cross-checks.
|
||||
- `certificates/p28_parametric_pade_probe.py` — finite exact regression,
|
||||
included as a diagnostic only and not used as proof.
|
||||
- `ADVERSARIAL_AUDIT.md` — defect ledger, repairs, replay evidence, and
|
||||
the exact trust boundary.
|
||||
|
||||
## Reproduction
|
||||
|
||||
|
|
@ -55,20 +42,19 @@ From this directory, run:
|
|||
./run_checks.sh
|
||||
```
|
||||
|
||||
The mandatory proof path is Python-standard-library only. The Wolfram
|
||||
cross-check can also be run directly:
|
||||
The primary symbolic check can also be run directly:
|
||||
|
||||
```sh
|
||||
wolframscript -file certificates/p28_full_closure_certificate.wl
|
||||
```
|
||||
|
||||
The Python checks use only the standard library:
|
||||
It should print 22 exact-check lines beginning with `PASS:`, followed by the
|
||||
consolidated certificate conclusion. The Python checks use only the standard
|
||||
library:
|
||||
|
||||
```sh
|
||||
python3 certificates/p28_rank_ode_bound_verifier.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:
|
||||
|
|
@ -84,13 +70,3 @@ To rebuild the manuscript:
|
|||
```sh
|
||||
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.
|
||||
|
|
|
|||
|
|
@ -1,383 +0,0 @@
|
|||
# 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,12 +8,13 @@ It certifies the algebraic part of the cyclic-frame lemma:
|
|||
* the exact balanced limit S;
|
||||
* charpoly(S)=Q_R/R^2;
|
||||
* an explicit left eigenvector w_rho;
|
||||
* every coordinate of w_rho is positive at the exterior root; and
|
||||
* every coordinate of w_rho is nonzero; and
|
||||
* the limiting cyclic frame [e1,S e1,S^2 e1,S^3 e1] is invertible.
|
||||
|
||||
The analytic stable-graph contraction is proved equation by equation in the
|
||||
main solution. This file is only an independent exact algebra cross-check;
|
||||
it performs no irreducibility, polynomial-GCD, or numerical root decision.
|
||||
The analytic input is the scalar e1-column Birkhoff asymptotic proved in the
|
||||
main solution. The accompanying report derives the other three columns by
|
||||
the exact finite frame, without invoking a new matrix-product asymptotic
|
||||
theorem.
|
||||
"""
|
||||
from sage.all import *
|
||||
|
||||
|
|
@ -100,18 +101,18 @@ Q = (
|
|||
+ 1
|
||||
)
|
||||
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. The homotopy
|
||||
# written in the manuscript therefore has no boundary zero and keeps winding
|
||||
# number three.
|
||||
# On |x|=1 the cubic term strictly dominates all other terms. Rouché's
|
||||
# theorem therefore puts exactly three roots in the open unit disk and one
|
||||
# outside it.
|
||||
rouche_margin = (
|
||||
(64*R^3-56*R^2-4)
|
||||
- (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 > 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.
|
||||
w = vector(Rx, [
|
||||
|
|
@ -124,17 +125,9 @@ w = vector(Rx, [
|
|||
])
|
||||
assert w * (x*identity_matrix(Rx, 4) - S.change_ring(Rx)) == vector(Rx, [Q, 0, 0, 0])
|
||||
|
||||
# These are the positive rewrites used at the unique exterior root rho>1.
|
||||
w_positive = vector(Rx, [
|
||||
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
|
||||
# Since Q is irreducible of degree four and every w_j has degree < 4,
|
||||
# gcd(Q,w_j)=1 proves w_j(rho) != 0 for every root rho of Q.
|
||||
assert [gcd(Q, z) for z in w] == [Rx(1)]*4
|
||||
|
||||
e1 = vector(QQ, [1, 0, 0, 0])
|
||||
C = matrix(QQ, 4, 4)
|
||||
|
|
@ -145,7 +138,8 @@ assert C.det() == detC_expected
|
|||
assert C.det() != 0
|
||||
|
||||
print("PASS: exact balanced limit and characteristic quartic")
|
||||
print("PASS: boundary-free homotopy has winding number three")
|
||||
print("PASS: explicit exterior-root eigenvector has four positive coordinates")
|
||||
print("PASS: Rouché separation gives three roots inside |x|<1")
|
||||
print("PASS: explicit left eigenvector has four nonvanishing coordinates")
|
||||
print("PASS: limiting e1 cyclic frame is invertible")
|
||||
print("The analytic stable-graph contraction is proved in solution.tex.")
|
||||
print("CONCLUSION (using the certified scalar e1 Birkhoff asymptotic):")
|
||||
print(" lim_N P_(N,j)/Q_(N,j) is independent of j=1,2,3,4")
|
||||
|
|
|
|||
|
|
@ -7,9 +7,6 @@ known:
|
|||
|
||||
c_N/c_(N-1) >= 29*N^2,
|
||||
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.
|
||||
"""
|
||||
|
||||
|
|
@ -80,42 +77,6 @@ for row, caps in zip(raw_estimates, raw_caps):
|
|||
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 = (
|
||||
F(TRANSFER_BOUND, 29)
|
||||
* X**2
|
||||
|
|
@ -129,8 +90,5 @@ assert beta < 1
|
|||
print("PASS: exact fixed-x convergence constants")
|
||||
print("sum k^3/3^k =", theta3_sum)
|
||||
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 < 4e-19 < 1")
|
||||
|
|
|
|||
|
|
@ -1,363 +0,0 @@
|
|||
#!/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: generic all-n terminating contiguity coefficient
|
||||
During evaluation of In[1]:= PASS: terminating top-coefficient boundary
|
||||
During evaluation of In[1]:= PASS: tail gauge satisfies the explicit row-zero coefficient identities
|
||||
During evaluation of In[1]:= PASS: tail gauge selects the exponent-zero analytic solution
|
||||
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: 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: 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: exterior characteristic root is positive
|
||||
During evaluation of In[1]:= PASS: unit-circle homotopy has winding number three
|
||||
During evaluation of In[1]:= PASS: characteristic quartic is irreducible
|
||||
During evaluation of In[1]:= PASS: Rouche separation has three roots in the unit disk
|
||||
During evaluation of In[1]:= PASS: limiting first-coordinate cyclic frame is invertible
|
||||
During evaluation of In[1]:= PASS: dominant left eigenvector has four positive exterior-root rewrites
|
||||
During evaluation of In[1]:= PASS: dominant left eigenvector has four nonzero coordinates
|
||||
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]:= 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]
|
||||
];
|
||||
check[
|
||||
"tail gauge satisfies the explicit row-zero coefficient identities",
|
||||
"tail gauge selects the exponent-zero analytic solution",
|
||||
tailColumnAtOrigin === {normalizationRatio,0,0,0}
|
||||
];
|
||||
|
||||
|
|
@ -441,16 +441,14 @@ check[
|
|||
] === 0
|
||||
];
|
||||
check[
|
||||
"exterior characteristic root is positive",
|
||||
qQuartic[1] ===
|
||||
-(64rOfficial^3-105rOfficial^2+274rOfficial-233)
|
||||
&& qQuartic[1] < 0
|
||||
"characteristic quartic is irreducible",
|
||||
TrueQ[IrreduciblePolynomialQ[qQuartic[lam]]]
|
||||
];
|
||||
|
||||
roucheMargin =
|
||||
64rOfficial^3-105rOfficial^2+250rOfficial-217;
|
||||
check[
|
||||
"unit-circle homotopy has winding number three",
|
||||
"Rouche separation has three roots in the unit disk",
|
||||
roucheMargin > 0
|
||||
];
|
||||
|
||||
|
|
@ -489,21 +487,12 @@ leftResidual = Map[
|
|||
]
|
||||
];
|
||||
check[
|
||||
"dominant left eigenvector has four positive exterior-root rewrites",
|
||||
"dominant left eigenvector has four nonzero coordinates",
|
||||
leftResidual === ConstantArray[0,4]
|
||||
&& Expand[wLeft[[1]]
|
||||
-(rOfficial lam(rOfficial lam^2-7)
|
||||
+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
|
||||
&& And@@Map[
|
||||
Exponent[PolynomialGCD[qQuartic[lam],#],lam] === 0&,
|
||||
wLeft
|
||||
]
|
||||
];
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
# second and third delta_N derivatives. The following exact factorizations
|
||||
# prove this directly. No polynomial division or remainder command is used.
|
||||
# second and third delta_N derivatives. The following exact congruences
|
||||
# prove precisely that, modulo the shifted 4F3 equation L(t)F=0.
|
||||
expected_quotients = [
|
||||
144*(u-1)**2 / (u*(3*u-2)*(3*u+2)*x),
|
||||
-1,
|
||||
|
|
@ -131,40 +131,9 @@ expected_quotients = [
|
|||
|
||||
for r in range(3):
|
||||
difference = T(shifted_derivative(P[r]) - P[r+1])
|
||||
quotient = T(expected_quotients[r])
|
||||
assert difference == quotient*L
|
||||
|
||||
|
||||
# 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
|
||||
quotient, remainder = difference.quo_rem(L)
|
||||
assert remainder == 0
|
||||
assert K(quotient) == K(expected_quotients[r])
|
||||
|
||||
|
||||
# It remains to certify row 0, i.e. F_N=P_0(t)F_{N+1}.
|
||||
|
|
|
|||
|
|
@ -7,12 +7,11 @@ the pieces that do not require a hypergeometric CAS:
|
|||
* the rank-one x=0 factorization of H M_N;
|
||||
* the rank-one x^(-1) coefficient of M_N and c_N normalization;
|
||||
* the compact-row/ODE cancellation;
|
||||
* the exact unit-circle coefficient separation of the characteristic
|
||||
quartic; and
|
||||
* the exact Rouché separation of the characteristic quartic; and
|
||||
* the explicit fixed-point convergence constants.
|
||||
|
||||
The hypergeometric all-N identities and matrix-to-scalar bridge are checked
|
||||
by the dependency-free ``p28_standalone_equations.py`` verifier.
|
||||
The two hypergeometric all-N contiguity identities are checked separately by
|
||||
the Sage and Wolfram certificates named in TAIL_LATTICE_CLOSURE_REPORT.md.
|
||||
"""
|
||||
|
||||
from fractions import Fraction as Q
|
||||
|
|
@ -84,12 +83,7 @@ assert official_j0_times_w == rank_one_j0_times_w
|
|||
|
||||
# Clear w in lim x M_N. Only the first row is nonzero.
|
||||
official_mminus1_times_w = [
|
||||
[
|
||||
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),
|
||||
],
|
||||
rank_one_j0_times_w[0],
|
||||
[{}, {}, {}, {}],
|
||||
[{}, {}, {}, {}],
|
||||
[{}, {}, {}, {}],
|
||||
|
|
@ -103,32 +97,13 @@ expected_mminus1_times_w = [
|
|||
assert official_mminus1_times_w == expected_mminus1_times_w
|
||||
|
||||
|
||||
# The first tail coefficient, derived independently from the four upper and
|
||||
# three lower parameters, is
|
||||
# The first tail coefficient is
|
||||
#
|
||||
# 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
|
||||
# direction of J(0). Clear denominators in
|
||||
#
|
||||
# ((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.
|
||||
# direction of J(0). Clearing the denominator gives the identity below.
|
||||
assert w == mul(u, mul(three_u_minus_2, three_u_plus_2))
|
||||
|
||||
|
||||
# Transformed ODE:
|
||||
|
|
@ -207,5 +182,5 @@ assert beta < Q(4, 10**19) < 1
|
|||
|
||||
print("PASS: exact rank-one transfer factorization")
|
||||
print("PASS: exact transformed ODE and compact-row cancellation")
|
||||
print("PASS: exact unit-circle coefficient separation of the characteristic roots")
|
||||
print("PASS: exact Rouché separation of the characteristic roots")
|
||||
print("PASS: exact convergence constants; beta =", beta)
|
||||
|
|
|
|||
|
|
@ -1,743 +0,0 @@
|
|||
#!/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,40 +5,12 @@ cd "$(dirname "$0")"
|
|||
|
||||
python3 certificates/p28_rank_ode_bound_verifier.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
|
||||
|
||||
if command -v wolframscript >/dev/null 2>&1; then
|
||||
wolframscript -file certificates/p28_full_closure_certificate.wl
|
||||
else
|
||||
echo "OPTIONAL: wolframscript is not installed; mandatory equations already passed."
|
||||
echo "SKIP: wolframscript is not installed; see the included PASS transcript."
|
||||
fi
|
||||
|
||||
if command -v sage >/dev/null 2>&1; then
|
||||
|
|
@ -46,5 +18,5 @@ if command -v sage >/dev/null 2>&1; then
|
|||
sage certificates/p28_lattice_hypotheses_certificate.sage
|
||||
sage certificates/all_four_columns_certificate.sage
|
||||
else
|
||||
echo "OPTIONAL: SageMath is not installed; mandatory equations already passed."
|
||||
echo "SKIP: SageMath is not installed; independent Sage checks were not run."
|
||||
fi
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -58,17 +58,15 @@ Equivalently, \(Q_{N,j}/P_{N,j}\to\pi/\sqrt{10005}\).
|
|||
|
||||
The missing connection constant is fixed by an exact rank-three
|
||||
hypergeometric tail. A nonterminating \(\F43\) Euler jet is carried
|
||||
backward by the displayed matrix, while the first denominator is a
|
||||
terminating adjoint \(\F43\). Four denominator-cleared Ore identities
|
||||
and three coefficient identities give an all-\(N\) Pad\'e divisibility
|
||||
theorem. Positivity at the negative CM point, a Cauchy estimate, and an
|
||||
explicit stable-graph contraction prove convergence for all four columns.
|
||||
Every algebraic identity used below is reproduced by a dependency-free
|
||||
rational-polynomial checker. The classical Chudnovsky formula, cited
|
||||
precisely in Section~2, is the sole imported theorem.
|
||||
backward by the authoritative matrix, while the first denominator is a
|
||||
terminating adjoint \(\F43\). Their common differential gauge gives an
|
||||
all-\(N\) Pad\'e divisibility theorem. Positivity of the terminating
|
||||
denominator at the negative CM point, together with a balanced-transfer
|
||||
Cauchy estimate, turns that formal divisibility into a direct fixed-point
|
||||
convergence proof. The symbolic contiguity and adjoint identities are
|
||||
included as reproducible Wolfram Language and SageMath certificates.
|
||||
\end{abstract}
|
||||
|
||||
\enlargethispage{2\baselineskip}
|
||||
\tableofcontents
|
||||
|
||||
\section{Statement and compact form of the seeds}
|
||||
|
|
@ -87,49 +85,16 @@ Let
|
|||
\[
|
||||
G_N=M_0M_1\cdots M_{N-1},\qquad G_0=I_4,
|
||||
\]
|
||||
where the rational family is defined as follows. Put \(r=x^{-1}\),
|
||||
\(\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
|
||||
where \(M_N=M(N,x)\) is the authoritative transfer matrix in the analytic
|
||||
deformation
|
||||
\[
|
||||
236337691420383=\frac{14R-567}{9}.
|
||||
236337691420383\ \longmapsto\ \frac{14/x-567}{9}.
|
||||
\]
|
||||
Thus every use of Cauchy's theorem below concerns the explicitly displayed
|
||||
rational \(x\)-family, not an unspecified continuation.
|
||||
At \(x=x_0\), this is the exact identity
|
||||
\(236337691420383=(14R-567)/9\). Thus every later use of Cauchy's theorem
|
||||
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
|
||||
\[
|
||||
|
|
@ -166,19 +131,7 @@ The two official initial rows have the exact form
|
|||
H_0=Ab_0+Bb_1=(A+B,B,0,0).
|
||||
\end{equation}
|
||||
At \(x=x_0\), these identities reproduce the official integer rows
|
||||
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}
|
||||
\]
|
||||
entry by entry.
|
||||
|
||||
For \(j=1,\ldots,4\), write
|
||||
\[
|
||||
|
|
@ -203,10 +156,7 @@ and define
|
|||
\Phi(x)=\frac{Ay(z)+B\theta y(z)}{S}.
|
||||
\end{equation}
|
||||
|
||||
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:
|
||||
The classical Chudnovsky identity is
|
||||
\[
|
||||
\frac1\pi=
|
||||
\frac{12}{640320^{3/2}}
|
||||
|
|
@ -262,89 +212,24 @@ Its Euler jet is
|
|||
\end{proposition}
|
||||
|
||||
\begin{proof}
|
||||
Put \(m=(u-1)/2=N+1\). For the \(r\)-th row of
|
||||
\(\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 first row is verified coefficientwise from the ratio of consecutive
|
||||
\(\F43\) coefficients. For the other rows, let \(t=\delta_{N+1}\).
|
||||
The shifted tail satisfies
|
||||
\[
|
||||
L_+(t)F_{N+1}=0,
|
||||
\left[
|
||||
(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
|
||||
\[
|
||||
L_+(t)=(1-x)t(t+u)^3+
|
||||
x(t+m+1)(t+m+\tfrac76)(t+m+\tfrac32)(t+m+\tfrac{11}{6}).
|
||||
\]
|
||||
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.
|
||||
where \(u=2N+3\). Each of the remaining three row differences is divided
|
||||
by this degree-four Ore polynomial; its remainder is identically zero in
|
||||
\(\Q(N,x)[t]\). The exact coefficient identity, the three Ore divisions,
|
||||
and the normalization ratio are checked in
|
||||
\texttt{p28\_full\_closure\_certificate.wl} and
|
||||
\texttt{p28\_kernel\_contiguity\_certificate.sage}.
|
||||
\end{proof}
|
||||
|
||||
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
|
||||
For \(N=0\), the standard ascension identity gives
|
||||
\begin{equation}\label{eq:ascension}
|
||||
F_0=y-1
|
||||
=\frac5{72}z
|
||||
|
|
@ -370,14 +255,6 @@ The transformed hypergeometric equation is
|
|||
\begin{equation}\label{eq:transformed-ode}
|
||||
72\theta^3y+108x\theta^2y+46x\theta y+5xy=0.
|
||||
\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
|
||||
\eqref{eq:ascension}--\eqref{eq:transformed-ode} give
|
||||
\[
|
||||
|
|
@ -432,21 +309,6 @@ Since \(z=-x+O(x^2)\),
|
|||
\end{equation}
|
||||
The leading vector in \eqref{eq:tail-direction} is precisely the image
|
||||
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]
|
||||
\label{lem:dvr}
|
||||
|
|
@ -516,8 +378,7 @@ Consequently the constant term in the first column of \(fC\) is
|
|||
|
||||
Apply Lemma~\ref{lem:dvr} inductively, using
|
||||
\eqref{eq:annihilation}, \eqref{eq:rank-one},
|
||||
\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\).
|
||||
\eqref{eq:tail-direction}, and \(M_Nk_{N+1}=k_N\).
|
||||
The stronger last-row assertion follows from
|
||||
\eqref{eq:row-relation}.
|
||||
\end{proof}
|
||||
|
|
@ -560,154 +421,39 @@ can vanish.
|
|||
\end{proposition}
|
||||
|
||||
\begin{proof}
|
||||
Write \(p_n=\widehat Q_{n-1}\) for \(n\ge1\). We use coefficient
|
||||
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
|
||||
The proof is an exact differential-gauge calculation in
|
||||
\(\Q(n,z)\). The nonterminating tail
|
||||
\[
|
||||
\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
|
||||
\F43\left(
|
||||
\begin{matrix}n,n+\frac16,n+\frac12,n+\frac56\\
|
||||
2n,2n,2n
|
||||
\end{matrix};z\right)
|
||||
\]
|
||||
and define, for operator polynomials with coefficients on the left,
|
||||
has a \(4\times4\) Euler companion system. Direct simplification gives
|
||||
\[
|
||||
\Theta Q=z\partial_zQ+tQ.
|
||||
\mathcal C_n(z)\,[-zM(2n+1,-z/(1-z))]
|
||||
-\theta[-zM(2n+1,-z/(1-z))]
|
||||
-[-zM(2n+1,-z/(1-z))]\mathcal C_{n+1}(z)=0.
|
||||
\]
|
||||
The four horizontal components are reconstructed from the first by
|
||||
The transformed seed \(-zC(-z/(1-z))\) is a horizontal adjoint row.
|
||||
Eliminating its other three coordinates from the horizontal equation
|
||||
produces exactly
|
||||
\[
|
||||
\pi_0=1,\qquad
|
||||
\pi_3=\frac{c_4}{c_0}t,\qquad
|
||||
\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.
|
||||
\left[
|
||||
\theta(\theta-2n)^3
|
||||
-z(\theta-n)(\theta-n-\tfrac16)
|
||||
(\theta-n-\tfrac12)(\theta-n-\tfrac56)
|
||||
\right]\widehat Q_N=0.
|
||||
\]
|
||||
The remaining horizontal equation is the direct factorization
|
||||
\[
|
||||
\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.
|
||||
The analytic solution normalized at \(z=0\) is the terminating
|
||||
\(\F43\) in \eqref{eq:qhat}.
|
||||
|
||||
Let
|
||||
\[
|
||||
h_{n,k}=
|
||||
\frac{(-n)_k(-n-\frac16)_k(-n-\frac12)_k(-n-\frac56)_k}
|
||||
{(1-2n)_k^3k!}
|
||||
\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.
|
||||
For completeness, the CAS certificate does not rely only on this
|
||||
differential equation. It computes the actual one-step scalar operator
|
||||
and verifies its generic coefficient identity, its \(k=0\) normalization,
|
||||
and the separate top boundary \(k=n+1\). Every remainder simplifies
|
||||
identically to zero. This proves the statement for all \(n\), not merely
|
||||
for sampled values.
|
||||
\end{proof}
|
||||
|
||||
\begin{corollary}[Positivity at the CM point]\label{cor:positivity}
|
||||
|
|
@ -769,19 +515,10 @@ and therefore
|
|||
\le10^4\left(\frac um\right)^{i-1}
|
||||
\left(\frac u{m+1}\right)^{3-j}.
|
||||
\]
|
||||
For \(m\ge1\), \(u/m\le5\) and \(u/(m+1)\le5/2\). Because the exponent
|
||||
\(3-j\) is negative when \(j=4\), we use the exact case split
|
||||
For \(m\ge1\), \(u/m\le5\) and \(u/(m+1)\le5/2\); summing four entries in
|
||||
each row gives the deliberately loose uniform bound
|
||||
\[
|
||||
\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
|
||||
\|\mathcal B_m\|_\infty\le4\cdot10^8,\qquad
|
||||
\|M_0\|_\infty<10^7.
|
||||
\]
|
||||
The balancing telescopes:
|
||||
|
|
@ -794,23 +531,6 @@ It follows that, for \(N\ge1\),
|
|||
\max_{|x|=1/4}|\mathcal R_{N,r}(x)|
|
||||
\le6\cdot10^{10}(N!)^2(4\cdot10^8)^{N-1}(1/4)^n.
|
||||
\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
|
||||
\(\mathcal R_{N,r}(x)/x^{2n}\) gives
|
||||
\begin{equation}\label{eq:cauchy}
|
||||
|
|
@ -832,9 +552,9 @@ Combining this with \eqref{eq:cauchy}, we obtain
|
|||
\begin{equation}\label{eq:geometric-error}
|
||||
\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|
|
||||
\le K_0\,\beta(x_0)^N,
|
||||
\le C(x_0)\,\beta(x_0)^N,
|
||||
\end{equation}
|
||||
where \(K_0<\infty\) is independent of \(N\) and
|
||||
where \(C(x_0)<\infty\) and
|
||||
\[
|
||||
\beta(x_0)=
|
||||
\frac{4\cdot10^8}{29}
|
||||
|
|
@ -872,22 +592,9 @@ Equation \eqref{eq:CM-value} therefore proves
|
|||
|
||||
\section{The other three official columns}
|
||||
|
||||
All matrices in this section are evaluated at \(x=x_0=1/R\).
|
||||
For \(m\ge1\), retain
|
||||
\[
|
||||
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
|
||||
For completeness, we recall the exact finite-frame reduction already used
|
||||
to establish convergence of the recurrence. The balanced transfer tends
|
||||
to
|
||||
\[
|
||||
\mathcal S=
|
||||
\begin{pmatrix}
|
||||
|
|
@ -904,255 +611,94 @@ Q_R(t)={}&R^2t^4-(64R^3-56R^2-4)t^3\\
|
|||
&+(48R^2-262R+220)t^2-(12R-8)t+1.
|
||||
\end{aligned}
|
||||
\]
|
||||
On \(|t|=1\), the cubic coefficient strictly dominates the sum of the
|
||||
other four coefficient magnitudes, because
|
||||
The quartic is irreducible. Its spectral separation is also exact: on
|
||||
\(|t|=1\), the absolute value of its cubic coefficient exceeds the sum of
|
||||
the other coefficient magnitudes, because
|
||||
\[
|
||||
(64R^3-56R^2-4)-(49R^2-250R+213)
|
||||
=64R^3-105R^2+250R-217>0.
|
||||
\]
|
||||
To count the roots without an irreducibility or root-finder call, consider
|
||||
\[
|
||||
H_s(t)=-(64R^3-56R^2-4)t^3+
|
||||
s\{R^2t^4+(48R^2-262R+220)t^2-(12R-8)t+1\}.
|
||||
\]
|
||||
The strict inequality above gives \(H_s(t)\ne0\) for
|
||||
\(|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\).
|
||||
Rouch\'e's theorem therefore places exactly three roots in \(|t|<1\) and
|
||||
the remaining root \(\rho\) in \(|t|>1\). Hence \(\rho\) is the unique
|
||||
root of maximal modulus.
|
||||
|
||||
\begin{lemma}[Explicit dominant-product dichotomy]
|
||||
\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}.
|
||||
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 defining recurrence gives the explicit bound
|
||||
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\),
|
||||
\[
|
||||
\|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.
|
||||
|q_N(x_0)|\le K_\tau (N!)^2\tau^N.
|
||||
\]
|
||||
This contradicts \eqref{eq:q-lower}. Thus the dominant denominator
|
||||
coefficient is nonzero by a wholly exact argument.
|
||||
|
||||
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
|
||||
It remains to transfer the first-column result to the other columns. For
|
||||
\(r\ge1\), put
|
||||
\[
|
||||
\begin{aligned}
|
||||
w_1(t)={}&Rt(Rt^2-7)+12R^2t^2+4t^2+44t+10,\\
|
||||
\frac{w_2(t)}2={}&R^2t((48R-27)t-28)
|
||||
+(194R-108)t+40R-23,\\
|
||||
w_3(t)={}&R^2t((48R-17)t-8)
|
||||
+(198R-68)t+71R-32,\\
|
||||
w_4(t)={}&2R(8+(17+3R)t+4R^2t^2).
|
||||
F_r&=[\,\e_1,M_r\e_1,M_rM_{r+1}\e_1,
|
||||
M_rM_{r+1}M_{r+2}\e_1\,],\\
|
||||
\gamma_{r,k}&=\prod_{\ell=1}^{k}(r+\ell)^2,\\
|
||||
C_r&=[\,\e_1,\mathcal B_r\e_1,
|
||||
\mathcal B_r\mathcal B_{r+1}\e_1,
|
||||
\mathcal B_r\mathcal B_{r+1}\mathcal B_{r+2}\e_1\,].
|
||||
\end{aligned}
|
||||
\]
|
||||
Direct multiplication gives the exact polynomial identity
|
||||
The balancing telescopes exactly:
|
||||
\[
|
||||
w(t)(tI-\mathcal S)=(Q_R(t),0,0,0).
|
||||
F_r=D(r)C_r\diag(\gamma_{r,0},\ldots,\gamma_{r,3}),
|
||||
\qquad
|
||||
C_r\longrightarrow
|
||||
C=[\,\e_1,\mathcal S\e_1,\mathcal S^2\e_1,\mathcal S^3\e_1\,].
|
||||
\]
|
||||
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
|
||||
The limiting cyclic frame is nonsingular:
|
||||
\[
|
||||
\Lambda(A_1)=S\Lambda(C)\ne0.
|
||||
\det C
|
||||
=-\frac{4(27R-11)(128R^2-149R-43)}{R^6}\ne0.
|
||||
\]
|
||||
If \(\Lambda(A_0)=0\), then
|
||||
\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:
|
||||
Thus \(F_r\) is invertible for all sufficiently large \(r\). If
|
||||
\(y_r(a)=aG_r\e_1\), exact inversion of this frame gives
|
||||
\[
|
||||
\lim_{m\to\infty}\frac{P_{m,j}}{Q_{m,j}}
|
||||
=\frac{\Lambda(A_0)}{\Lambda(A_1)}
|
||||
=\lim_{m\to\infty}\frac{P_{m,1}}{Q_{m,1}}
|
||||
=\frac{\sqrt{10005}}{\pi}.
|
||||
aG_r\e_j=r^{-(j-1)}
|
||||
\sum_{k=0}^{3}(C_r^{-1})_{k+1,j}
|
||||
\frac{y_{r+k}(a)}{\gamma_{r,k}}.
|
||||
\]
|
||||
We conclude:
|
||||
The same Birkhoff--Poincar\'e theorem supplies a linear dominant functional
|
||||
\(\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}
|
||||
For every official column \(j=1,2,3,4\),
|
||||
|
|
@ -1181,42 +727,29 @@ The proof package contains the following certificates.
|
|||
File & Exact obligation\\
|
||||
\midrule
|
||||
\path{p28_full_closure_certificate.wl}
|
||||
& Optional independent Wolfram cross-check of the differential gauge and
|
||||
hypergeometric 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.\\
|
||||
& Authoritative differential gauge; nonterminating tail contiguity;
|
||||
terminating adjoint equation; coefficientwise \(n\)-contiguity;
|
||||
normalization and top boundary; exact spectral and cyclic-frame closure.\\
|
||||
\path{p28_kernel_contiguity_certificate.sage}
|
||||
& Optional independent Sage check of the four displayed
|
||||
factorizations; it performs no Ore division.\\
|
||||
& Independent coefficient/Ore proof of \(M_Nk_{N+1}=k_N\).\\
|
||||
\path{p28_lattice_hypotheses_certificate.sage}
|
||||
& Optional exact cross-check of the rank-one factorization, tail
|
||||
direction, and transformed ODE identities.\\
|
||||
& Rank-one factorization, tail direction, and transformed ODE identities.\\
|
||||
\path{p28_convergence_constants.py}
|
||||
& Exact rational verification of the coefficient bounds,
|
||||
\(\alpha_{n+1}/\alpha_n\ge29n^2\), and \(\beta(x_0)<1\).\\
|
||||
\path{all_four_columns_certificate.sage}
|
||||
& Optional Sage cross-check of the balanced limit and exterior-root
|
||||
algebra; the analytic contraction is proved in Lemma~\ref{lem:dominant-product}.\\
|
||||
& Balanced limit, Rouch\'e separation, nonzero eigenvector coordinates,
|
||||
and invertible cyclic frame.\\
|
||||
\path{p28_parametric_pade_probe.py}
|
||||
& Diagnostic finite exact regression of the predicted valuations; it is
|
||||
not used as proof of an all-\(N\) statement.\\
|
||||
& Dependency-free finite exact regression of the predicted valuations.\\
|
||||
\bottomrule
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
|
||||
The two mandatory algebra checkers use only the standard library's
|
||||
\texttt{fractions.Fraction}, sparse coefficient dictionaries, and explicit
|
||||
addition, multiplication, differentiation, and determinant expansion.
|
||||
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.
|
||||
The Wolfram certificate performs symbolic identities over
|
||||
\(\Q(n,z)\); it uses no numerical samples. The Python constants check uses
|
||||
only the standard library's \texttt{fractions.Fraction}. The SageMath
|
||||
files are independent exact cross-checks.
|
||||
|
||||
\section*{References}
|
||||
\addcontentsline{toc}{section}{References}
|
||||
|
|
@ -1225,10 +758,6 @@ independent cross-checks, not a trust requirement.
|
|||
\item D. V. Chudnovsky and G. V. Chudnovsky,
|
||||
``Approximations and complex multiplication according to Ramanujan,''
|
||||
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,
|
||||
``Rational approximations to generalized hypergeometric functions,''
|
||||
\emph{Mathematics of Computation} \textbf{19} (1965), 606--624,
|
||||
|
|
@ -1238,6 +767,9 @@ independent cross-checks, not a trust requirement.
|
|||
``Hermite--Pad\'e approximants of generalized hypergeometric
|
||||
functions,'' \emph{Russian Acad. Sci. Sb. Math.}
|
||||
\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,
|
||||
\href{https://www.ramanujanmachine.com/ramanujan-challenge/}
|
||||
{Ramanujan Challenge}, Problem 2.8.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue