111 lines
7 KiB
Markdown
111 lines
7 KiB
Markdown
# 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.
|