allaun
39806d4423
Adds the framing that explains the disproportionate machinery: Problem 2.8 was
approached as a test case for an existing pipeline (encoding, exact-arithmetic
verification, excluded-route registry), not as an isolated puzzle. A well-posed
external problem with an objectively checkable answer is a good defect-finding
instrument because it cannot be argued with.
That is why a Coq-and-Lean treatment of leading zeros sits under a pi formula:
absurd overhead for one limit, reasonable for a codec other work depends on.
Same for the mutation testing, authority tags, and impossibility registry.
Notes the congruence with the challenge's own section 1, which presents these
problems as benchmark instruments with structured verification.
Adds 'What the exercise found', since if the problem is an instrument then the
defects it exposed are part of the result:
- defects in the argument, repaired pre-release (false ODE-normalisation
uniqueness, invalid norm-inequality direction, unproved holomorphy in the
maximum-modulus step, Birkhoff-Poincare as a black box, an untied scalar
operator that could have been a surrogate, Q/P vs P/Q orientation)
- defects in the verification machinery -- the failures that let bad results
pass (checks succeeding with the CAS absent, quo_rem trusting a zero
remainder, irreducibility/GCD standing in for arguments)
- defects still open, found during independent replay (run_checks.sh exit-code
inversion, the false assertion at line 107, the Sage 10.9 coercion error
masking it, and the Lean-only radix DFA facing regeneration erasure)
The last group is left open rather than tidied away: a validated tool would not
still be producing these, and the point of running the instrument is that it is.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WY6SfRYvm8zFKMX9GcjS8u
|
||
|---|---|---|
| .. | ||
| certificates | ||
| ADVERSARIAL_AUDIT.md | ||
| ADVERSARIAL_REVIEW_AGAINST_CHALLENGE_RULES.md | ||
| HOW_THE_SOLUTION_WAS_FOUND.md | ||
| NOTATION_AND_BORROWED_TERMINOLOGY.md | ||
| ramanujan_challenge_problem_2_8.zip | ||
| README.md | ||
| run_checks.sh | ||
| solution.pdf | ||
| solution.tex | ||
Ramanujan Challenge, Problem 2.8
This package proves, for each of the four official columns,
[ \lim_{N\to\infty}\frac{P_{N,j}}{Q_{N,j}} =\frac{\sqrt{10005}}{\pi}, \qquad \lim_{N\to\infty}\frac{Q_{N,j}}{P_{N,j}} =\frac{\pi}{\sqrt{10005}}. ]
The first display is the orientation requested in Problem 2.8; the second is its reciprocal consequence.
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.PASS.txt— transcript of a stateless Wolfram Language run (22 exact checks plus the consolidated conclusion).certificates/p28_convergence_constants.pyandcertificates/p28_rank_ode_bound_verifier.py— dependency-free exact rational checks for the fixed-point convergence bound.certificates/p28_kernel_contiguity_certificate.sage,certificates/p28_lattice_hypotheses_certificate.sage, andcertificates/all_four_columns_certificate.sage— independent exact 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
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:
wolframscript -file certificates/p28_full_closure_certificate.wl
The Python checks use only the standard library:
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:
sage certificates/p28_kernel_contiguity_certificate.sage
sage certificates/p28_lattice_hypotheses_certificate.sage
sage certificates/all_four_columns_certificate.sage
To rebuild the manuscript:
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.