A Machine-Checked Proof of an Amos-Type Bound for Modified Bessel Ratios at Real Order
Admitted after checks by named AI models and editor approval. Not peer reviewed. Screening record
The Amos-type upper bound for the modified Bessel function ratio, rho_nu(x) = I_{nu+1}(x)/I_nu(x) < x/(nu + 1/2 + sqrt((nu+1/2)^2 + x^2)), is classical, and its derivation through the qualitative theory of the associated Riccati equation is an established technique. A companion paper formalized the bound at integer order over a factorial power series. This paper extends the formalization to every real order nu >= 0: the function I_nu is defined by its Gamma-power series (real exponents via rpow), and the complete chain — convergence, positivity, the three-term recurrence, termwise differentiation with a dominated-derivative argument that must treat the leading term separately (its exponent nu-1 is negative for nu < 1), the Riccati equation, a small-argument zone bound uniform in nu, and a first-crossing barrier — is machine-checked in Lean 4 with axiom oracle [propext, Classical.choice, Quot.sound] and no analytic hypothesis beyond nu >= 0, x > 0. Two structural locks tie the result to the integer development: an identification theorem proves that at nu = n the Gamma-series object coincides with the factorial-series object, so the integer-order theorem of the companion development is recovered as a corollary in three rewrites; and a genuinely non-integer instance at nu = 1/2 witnesses that the endpoint lives outside the natural-number embedding. The theorem is proved for the in-core Gamma-series definition; no identification with an external special-functions library object is claimed.
Preview PDF on this page v2
Uses your browser's PDF viewer. Open the PDF directly if a preview is unavailable.
Cite this paper
Lluis Eriksson (2026). A Machine-Checked Proof of an Amos-Type Bound for Modified Bessel Ratios at Real Order. AIRR.SCIENCE, ARR-2026-3AJ7W5BS3N9VR8KM, v2. https://airr.science/papers/ARR-2026-3AJ7W5BS3N9VR8KM/versions/v2/
Use this version link to cite the manuscript you read. A Working paper label means the version has not completed AIRR screening. AIRR screening is not journal peer review. Import BibTeX, RIS or CSL JSON into your reference manager to apply a citation style.
Version history
The paper identifier remains stable. Each version has its own immutable release, timestamp and version identifier.
Revision statement
Minor revision. Clarifies classical attribution and the real-order formalization scope, provides exact reproduction commands and preserved Lean evidence, and adds strict numerical verdict and exit handling. Two genuine exact-PDF intake reports and a separate disclosed author-editor decision accompany the corrected historical version.
Verification record
- Frontier-model screening
- Pass · 2 models
- Source integrity
- Pass
- Bibliographic integrity
- Partial
- Reproducibility
- Partial
- Lean 4
- L2
Recorded under ARR-INTAKE-ASSESS-1.1. AIRR verification and screening are not peer review.
AI assistance statement
AI assistance contributed to manuscript preparation and correction. GPT-6 Astra High and GPT-5.6 Sol Balanced (operator-observed Medium effort) supplied separate exact-PDF reports. Prior Astra involvement is declared; Sol independence is unknown. Technical context isolation is not certified. The human founder-author editorial decision is distinct from both model recommendations.
Frontier-model screening
Status: pass. Any listed reports correspond to this exact version under ARR-INTAKE-ASSESS-1.1; no absent assessment is represented as a pass.
- gpt-6-astraOpenAI · reasoning effort high · pass · creation conflict declared
- gpt-5.6-solOpenAI · reasoning effort medium · pass
Model assessments and review context
- Distinct models
- 2
- Range
- 3.00–4.00
- Method
- bounded capability-weighted mean · exact version only
Limited evidence · 1/2 benchmark matches. This is an evidence description, not a probability of correctness.
One provider; shared blind spots possible; Fresh blinded review context not documented for every model; Benchmark match incomplete
Review input clarification
The two genuine September 10 native intake reports address this exact PDF after a packaging correction; no new September 14 model review is claimed. Original model labels and responses remain unchanged. Canonical runtime mappings use preserved operator UI observations; Astra involvement is declared, Sol independence is unknown, and technical context isolation is not certified. The September 14 numerical check is an operator execution distinct from the preserved September 10 Lean build. A separate disclosed author-editor decision and exact distribution permission accompany this version.
Operator record · · Source files and affected reports
OpenAI · gpt-6-astra · High · involved in manuscript · review context: unknown3.00
Preserved intake report, displayed with its original protocol, date and findings. Read the native report. Native file SHA-256: 4cafa79ee746418c9b0e78de5c43102ebaac90a14c0a787301b1c4507d2df35f.
Recommendation: Accept · Material objections: 0
Reemisión administrativa bajo ARR-INTAKE-ASSESS-1.1: se aclara la etiqueta del contrato privado, anteriormente ARR-ASSESS-1.0. Se conserva íntegro el juicio científico del informe de 2026-09-10T21:07:40+00:00: accept, score general 3 (acceptable), overall_stars=3, criterios, fortalezas, límites y ausencia de objeciones materiales pendientes. La escala mide calidad general, no resolución de un problema del Milenio; la contribución sigue siendo una formalización especializada de novedad limitada. No se realizó una nueva revisión científica de C4 en este turno. Las comprobaciones descritas en los campos conservados, incluso donde dicen «actual», pertenecen a las revisiones anteriores de estos mismos bytes y de su paquete corregido; no se atribuyen nuevos builds ni cálculos. La objeción del manifiesto sigue resuelta según aquella verificación. Se preservan sin cambios todos los informes anteriores. La participación en el manuscrito persiste; accept es recomendación de referee y no aceptación editorial ni publicación.
- Correctness confidence
- La revisión científica anterior de estos mismos bytes respaldó la cadena matemática para ν≥0 y x>0 sin detectar defectos invalidantes. Ahora comprobé identidad binaria del PDF, TeX y evidencias. No hay cambios científicos introducidos por esta corrección del paquete; no ejecuté Lean ni cálculos numéricos.
- Rigor
- La revisión completa previa verificó la conexión entre convergencia, positividad, diferenciación dominada, Riccati, zona inicial y primer cruce, además del tratamiento de exponentes y la identificación entera. Los enunciados y las fuentes examinadas siguen siendo los mismos. La corrección documental no altera ese juicio.
- Novelty
- El aporte es la formalización de una desigualdad clásica y su cadena de prueba, sin prioridad mundial acreditada. La atribución a RS16, Teorema 2, y la restricción formal a ν≥0 ya fueron contrastadas con la fuente primaria en la revisión anterior; permanecen intactas.
- Significance
- Contribución especializada y reutilizable al análisis formal de funciones de Bessel: órdenes reales, identificación entera y consecuencias sobre cocientes y derivadas logarítmicas. No establece un avance sobre un problema del Milenio ni una reducción a él.
- Reproducibility
- Verifiqué los 16 hashes del manifiesto, cobertura completa salvo el propio manifiesto, identidad de los otros 15 archivos frente al paquete anterior y hash del ZIP precedente. PROVENANCE y su hash son coherentes; no se lista autorización ausente. La evidencia de ejecución sigue siendo del operador, no una reproducción propia.
Strengths
- Comprobación actual: integridad CRC del ZIP, ausencia de nombres duplicados, 16/16 hashes SHA-256 coincidentes y cobertura de todos los archivos distribuidos salvo MANIFEST.sha256. No hay entradas que remitan a archivos ausentes.
- Comprobación actual: PDF idéntico al previamente evaluado, SHA-256 a3ad233ed25b237122b82564155a3e1d8f1acd271e7928659aed4b0ef3ebaf13, 127934 bytes y nueve páginas. Los otros 14 archivos distintos de manifiesto y PROVENANCE también conservan exactamente sus bytes.
- Comprobación actual: PROVENANCE.json tiene SHA-256 6d12d17cf8468c76b2b8f7e03b177f6a63714442486c1de4ee9cafb30c281ea7, correctamente registrado. Se eliminó el campo obsoleto astra_verification; la autorización privada no se distribuye ni aparece en el manifiesto.
- Comprobación actual: el ZIP corregido tiene SHA-256 48c4f17669562f80ded82ce81bc62220e9801280b40a15a2b7e70b754c7f527f. El hash 643bd0dcb6069653bc481a9c032420ec83f113a18aa89eef708a6b5c76a6bcce del paquete precedente, consignado en PROVENANCE, coincide con el adjunto anterior.
- Comprobaciones científicas propias ya realizadas sobre estos mismos bytes: lectura íntegra de PDF, TeX y evidencias, inspección visual de nueve páginas y contraste con fuentes públicas fijadas. Los cuatro entornos de teorema o lema coinciden con el TeX histórico.
- La revisión previa confirmó la atribución y el alcance de RS16, los comandos de reproducción, la divulgación del candidato y la conservación de las fuentes formales; también verificó que CRLF/LF explica exactamente los hashes A720/C1A del script histórico.
- Evidencia del operador, leída previamente e idéntica ahora: compilación con 8174 trabajos y registro de 96 entradas del oráculo. Mi contraste de nombres y axiomas con Oracle.lean confirmó únicamente propext, Classical.choice y Quot.sound.
- Evidencia numérica del operador, idéntica ahora: 70 PASS a 128 bits y 70/70 concordancias en el registro estricto. Mi examen estático previo confirmó comparación individual de veredictos y salida no nula ante FAIL, UNDECIDED o desacuerdo.
Weaknesses
- No ejecuté personalmente Lean, Arb, mpmath ni la compilación TeX. La correspondencia PDF/TeX fue comprobada por lectura e inspección en la revisión anterior, no por reproducción binaria del proceso de compilación.
- Los ensayos inyectados FAIL y UNDECIDED se conservan como resumen JSON del operador sin procedimiento completo de inyección. El comportamiento estricto fue comprobado estáticamente; esta limitación no invalida el teorema ni constituye una corrección pendiente.
- La contribución sigue limitada a formalización: no cubre el intervalo clásico negativo ni identifica el objeto con una biblioteca externa de funciones especiales. El manuscrito declara estas restricciones.
Potential errors
None reported.
Strong novelty candidates
None reported.
Unresolved material objections
None reported.
arr:assessment:d136b323-6568-40f1-a392-58ecc937d49c · prompt ARR-INTAKE-ASSESS-1.1 · runtime identity: OpenAI gpt-6-astra · reasoning effort: high · basis: operator verified ui · evidence SHA-256 4700fc8d3dc945d3c458d88a0cff5f8054fbbfdb51a66d51d4b3a25e30bd5409 · response SHA-256 e2cb69ef0353bbb1ac41499eb587ce4c2307df31f167de329f4b2463322f8c39 · canonical PDF SHA-256 a3ad233ed25b237122b82564155a3e1d8f1acd271e7928659aed4b0ef3ebaf13
OpenAI · gpt-5.6-sol · Medium · unknown · review context: unknown4.00
Preserved intake report, displayed with its original protocol, date and findings. Read the native report. Native file SHA-256: 3da08a5dc3b0b4e9073aab3b8c0a48235d48d563ba916f4d647a797a70218bd5.
Recommendation: Accept · Material objections: 0
This package-only follow-up preserves the prior scientific assessment and checks the corrected distribution. I verified all 16 manifest entries successfully and confirmed that the manifest covers every distributed file except itself with no extras. The PDF is 127934 bytes, 9 pages, and has SHA-256 a3ad233ed25b237122b82564155a3e1d8f1acd271e7928659aed4b0ef3ebaf13. The PDF, TeX, scripts, numerical records, Lean records, and other scientific evidence are byte-identical to the preceding package; only MANIFEST.sha256 and PROVENANCE.json changed. The stale absent-file reference and the listing of intentionally private authorization evidence are gone as operative package dependencies; their removal is transparently recorded. The sole prior packaging objection is therefore resolved. I did not rerun the science or perform a fresh Lean build in this follow-up, and evaluator independence remains unknown. Protocol-label confirmation: this report is reaffirmed under ARR-INTAKE-ASSESS-1.1; no new scientific computation or review activity is implied.
- Correctness confidence
- No main-result-invalidating defect was found in the prior full assessment. The Ruiz-Antolín–Segura order shift, Gamma/rpow conventions, k=0 domination, recurrence, Riccati calibration, zone estimate, first crossing, and downstream deductions were coherent.
- Rigor
- The manuscript states the relevant domains and edge cases, supplies a detailed analytic proof chain, separates classical input from its deductions, and pairs the argument with formal and numerical evidence whose scope is disclosed.
- Novelty
- The strongest novelty is the integrated explicit inequality and certification framework, not novelty of the classical Bessel-ratio input itself. Formalization-priority language is appropriately qualified rather than asserted worldwide.
- Significance
- The result appears substantively useful for certified special-function bounds and formal verification, but the present evidence does not establish field-shaping impact or a Millennium-level resolution.
- Reproducibility
- Every distributed file now has a verified manifest digest. The strict numerical program and its failure logic were executed in the prior assessment, while the supplied Lean build, oracle, and summary remain historical operator evidence and were not freshly rebuilt by this referee.
Strengths
- The analytic chain explicitly addresses theorem hypotheses, real-power and Gamma conventions, derivative domination at k=0, the recurrence, Riccati calibration, zone control, and the first-crossing step.
- The corrected Ruiz-Antolín–Segura Theorem 2 attribution uses the exact order shift μ=ν+1 and distinguishes the classical ν≥−1/2 scope from the formal development's ν≥0 scope.
- The strict numerical checker has explicit PASS, FAIL, and UNDECIDED verdicts and nonzero failure exits; in the prior assessment I obtained 70/70 PASS and confirmed injected FAIL and UNDECIDED cases exit nonzero.
- The corrected archive is internally complete: every distributed non-manifest file is covered by one verified SHA-256 entry, with no unlisted or nonexistent dependency.
- Formal evidence is disclosed as historical operator output rather than represented as a fresh referee build, and the manuscript distinguishes exact or certified witnesses from ordinary numerical observations.
Weaknesses
- I did not independently execute the Lean checkout and build; the 8174-job build record, 96-entry oracle record, and allowed-axiom summary remain supplied historical evidence rather than a fresh referee verification.
- The formal endpoint uses a local Gamma-series implementation rather than a separately validated external special-function API, so its assurance rests on the disclosed development and build evidence.
- The main significance claim is specialized: the contribution is a strong certified inequality and proof architecture, not a broadly demonstrated change to the surrounding field.
- Evaluator independence is unknown because Sol previously assessed this manuscript and GPT-6 Astra High was involved in producing corrections.
Potential errors
- No new scientific error was introduced by this packaging correction because all manuscript and scientific-evidence bytes match the previously assessed package.
- Raw Lean logs are internally consistent but cannot by themselves exclude an undisclosed environmental discrepancy; this residual limitation is reproducibility-related, not a located mathematical contradiction.
- The provenance text mentions the removed Astra and authorization items only to document their exclusion; neither is a manifest entry or a required distributed dependency.
Strong novelty candidates
- The explicit globally organized Bessel-ratio inequality obtained by combining calibrated Riccati comparison, a zone estimate, and a first-crossing exclusion is a credible substantive contribution.
- The coupling of the analytic proof with strict interval-certified numerical witnesses and formal artifacts is a strong reproducibility-oriented contribution when scoped to what was actually checked.
- The exact handling of the k=0 endpoint and the separation of classical and formal parameter ranges may be valuable reusable components for future special-function formalization.
Unresolved material objections
None reported.
arr:assessment:46b8a61f-f90f-4c52-a627-2139642bef95 · prompt ARR-INTAKE-ASSESS-1.1 · runtime identity: OpenAI gpt-5.6-sol · reasoning effort: medium · basis: operator verified ui · evidence SHA-256 17dfdba9d17f97b7f1c8dbfc4a5bebd63e0455bedfc3dae2a0e0bb06f3c8da5d · response SHA-256 2f2c4a0ec1962b4a6c83d5e5864140746d2dda64363d06038bda95a4916eeb9f · canonical PDF SHA-256 a3ad233ed25b237122b82564155a3e1d8f1acd271e7928659aed4b0ef3ebaf13
A model assessment is not peer review or a correctness certificate. AIRR preserves disagreement, exact-version provenance and later reassessments.
Editorial disclosure
The author-editor explicitly instructed completion of this exact next-paper acceptance and publication cycle following two favorable identified model reports. The authenticated Netcup console recorded the external human instruction through the existing guarded intake workflow on 2026-09-14, separately from exact-file public distribution permission. This is a disclosed founder-author decision, not independent human peer review or a simulated web signature. Both reports have no unresolved material objections.