ramanujan-challenge/experiments/ramanujan_28/submission/ADVERSARIAL_AUDIT.md

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 (
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:

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