# 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.