The Diagonal Amos-Type Family at Real Order: a Machine-Checked Quantitative Crossing Classification
Admitted after checks by named AI models and editor approval. Not peer reviewed. Screening record
For the one-parameter family B(x) = x/(nu+c+sqrt((nu+c)^2+x^2)) of Amos-type expressions, whose member c = 1/2 is the classical Amos-type upper bound for the modified Bessel ratio I_{nu+1}/I_nu, we formalize in Lean 4, at every real order nu >= 0 over the Gamma-power series, the classification of the parameter: B is a uniform upper bound for the ratio exactly when c <= 1/2, and a uniform lower bound for every c >= 1, with explicit rational counterexample witnesses (the classification itself is known mathematics, due to Ruiz-Antolin and Segura; we claim only the machine-checking). The contribution is the regime between the ends: for every nu >= 0 and c strictly between 1/2 and 1 we prove that the fixed family member crosses the ratio exactly once on (0, infinity) -- a transversal crossing in an explicit finite window, strictly above an explicit threshold, with globally determined sign on both sides and a two-sided scale law; degenerate contact is excluded by an exact second-derivative identity. The chain carries the axiom oracle [propext, Classical.choice, Quot.sound] and no analytic hypothesis beyond nu >= 0, x > 0; a pre-registered certified interval-arithmetic companion verifies the crossing phenomenon independently of the crossing theorems at 30 parameter pairs spanning the hard regimes, all passing at 128 bits.
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). The Diagonal Amos-Type Family at Real Order: a Machine-Checked Quantitative Crossing Classification. AIRR.SCIENCE, ARR-2026-39Y0F83F4Z9JK90G, v2. https://airr.science/papers/ARR-2026-39Y0F83F4Z9JK90G/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 attribution, quantitative crossing witnesses and artifact provenance. Preserves declared limits of formal dependency and numerical reproduction. 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
- L0
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
- 4.00–4.20
- 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; 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 supplied formal excerpts are not a build checkout; historical numerical and Lean claims were not rerun on September 14. The two reviewers had unequal source coverage, declared in their original reports. 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: unknown4.00
Preserved intake report, displayed with its original protocol, date and findings. Read the native report. Native file SHA-256: aa687ab211a1d5ea72a27780cd38e40e6382b201bb0a60c29493429aed3acf08.
Recommendation: Accept · Material objections: 0
Revisión científica nueva de los 11 folios de C5, ligada exclusivamente a estos bytes. La clasificación de la familia diagonal, el cruce único transversal y sus cotas explícitas resisten el examen matemático y de fuentes efectuado. Recomiendo accept como dictamen de referee de una contribución especializada sólida, con prioridad no exhaustivamente establecida. Los 30 certificados y comparaciones numéricas son evidencia histórica leída, no ejecuciones mías. La participación previa en las correcciones persiste; este informe no constituye aceptación editorial.
- Correctness confidence
- La lectura de las 11 páginas y del desarrollo fuente respalda la cadena Riccati–signo inicial–contacto–cruce único. Recalculé el signo de la derivada en el contacto y la segunda derivada positiva en el umbral. No encontré una contradicción entre los teoremas principales y sus hipótesis formales.
- Rigor
- La prueba distingue contacto tangencial, transversalidad y signos a ambos lados; la ventana explícita y la ley de escala se deducen de esas piezas. El testigo del régimen superior fallido y la identidad interna usada bajo hipótesis de contacto están descritos ahora con alcance correcto. La evidencia Lean es histórica.
- Novelty
- Las regiones extremales de Amos son clásicas. La formalización conjunta del cruce transversal, su umbral y las cotas de localización aporta contenido especializado. Consulté RS16, Segura y Hornik–Grün; sus resultados relacionados no acreditan ni descartan por sí solos prioridad exhaustiva para esta formulación.
- Significance
- El resultado da una clasificación y controles explícitos útiles para cocientes de Bessel de orden real no negativo. La calidad del conjunto justifica 4 en la escala general AIRR; el impacto es especializado y no constituye una solución de un problema del Milenio.
- Reproducibility
- Verifiqué integridad, correspondencia de fuentes y resolución del tag c5-v1.0.1 al commit 3eb5cf9293d2b8cc6ece17f5e37d422726b9d27d. Leí el script Arb y su registro de 30 PASS; el SHA-256 LF coincide con 3f31ff76…43c67. No ejecuté Arb, mpmath ni Lean en este turno.
Strengths
- Comprobaciones propias de este turno: CRC e inventario completo del ZIP; 80/80 hashes del manifiesto; identidad PDF–CASES–recibo; lectura íntegra del PDF y TeX, diff, procedencia y evidencias. Los seis diffs reconstruyen sus candidatos al normalizar finales de línea. Se inspeccionaron visualmente las páginas 1 y 3 de cada PDF; no se recompiló TeX.
- Comprobación propia: para t=2c−1, a=ν+c y un contacto en x†, las identidades de Riccati dan D″=t³B/a²>0. Combinada con el signo previo negativo, esta observación excluye la tangencia crítica; todos los ceros admisibles quedan como cruces ascendentes.
- Comprobación propia: revisé AmosCrossing, AmosTangency y las dependencias AmosFamily/AmosLowerReal relevantes. El testigo ν=0, x=2/(2c−1) y las anclas para 1/2<c<1 concuerdan con los dominios declarados.
- Comprobación propia de procedencia: 71097284551d65d989ab7bf024a7c179ee063866 es el objeto de tag anotado; su commit resuelto es 3eb5cf9293d2b8cc6ece17f5e37d422726b9d27d. El oráculo C5 contiene 110 consultas; el C4 publicado contiene 96, distinto de la cohorte histórica de 74.
- Evidencia histórica inspeccionada: 30 pares (ν,c), signos Arb de D en los extremos y D′ en el intervalo, todos PASS a 128 bits, con 30 concordancias del acompañante mpmath. El script se verifica por sus signos de bolas, sin invocar el teorema de cruce.
Weaknesses
- Las fuentes formales y registros suministrados son históricos. Contrasté archivos relevantes con blobs públicos fijados y revisé sus hipótesis; no ejecuté Lean ni audité mediante compilación todas las dependencias transitivas. Un registro del operador no equivale a una reproducción propia.
- La prioridad mundial no quedó establecida. Fuentes primarias consultadas: https://arxiv.org/pdf/1606.02008 ; https://arxiv.org/pdf/2207.02713 ; https://files.ele-math.com/articles/mia-27-55.pdf . No pude contrastar la referencia arXiv:2607.05538; no la uso para certificar novedad.
- El script histórico imprime FAIL o UNDECIDED sin imponer una salida global no nula. Para automatización futura convendría un envoltorio estricto, preservando el script histórico. Esto no contradice los 30 veredictos PASS efectivamente consignados.
Potential errors
None reported.
Strong novelty candidates
- Candidato especializado: mecanización conjunta, para órdenes reales no negativos, de cruce único transversal, umbral estricto, ventana explícita y ley de escala de la familia diagonal. No se afirma prioridad mundial ni novedad de los regímenes extremales clásicos.
Unresolved material objections
None reported.
arr:assessment:e08bc35f-64f9-412e-9fbb-a861d67494ce · prompt ARR-INTAKE-ASSESS-1.1 · runtime identity: OpenAI gpt-6-astra · reasoning effort: high · basis: operator verified ui · evidence SHA-256 c229c68ebd71adbbc1b83867f36000e1e1aecbf4c86b493c1147cbc9d7fff113 · response SHA-256 220c7ab9e6f76e412c93d0c3fc19e5a7800609ab36e34a23a0d371cc2dfda86b · canonical PDF SHA-256 eabefc6d93e453b5599f7c1e8c1c7c311352c43d7d61eec0223dced09720ce0c
OpenAI · gpt-5.6-sol · Medium · unknown · review context: unknown4.20
Preserved intake report, displayed with its original protocol, date and findings. Read the native report. Native file SHA-256: 478c192b0e39e678c5eed87db9b73453417fdbf9dd5d67faf327c5ffbe9e9fcf.
Recommendation: Accept · Material objections: 0
Fresh review of all 11 pages and the supplied source, revision, provenance, and formal excerpts found no main-result-invalidating defect. The exact PDF hash and CASES.json binding verify. Algebraically, the c=1/2 calibration, recurrence inversion, explicit witnesses, crossing window, slope formula, strict threshold, uniqueness/orientation argument, and positive-curvature exclusion are mutually consistent. The paper now correctly treats the Ruiz-Antolín–Segura classification and qualitative crossing as prior art. The formal evidence is historical and incomplete as a build checkout; I did not execute Lean or the absent certified numerical companion. The quantitative crossing package remains a credible strong novelty candidate within its in-core Γ-series scope. Protocol-label confirmation: this report is reaffirmed under ARR-INTAKE-ASSESS-1.1; no new scientific computation or review activity is implied.
- Correctness confidence
- The calibration, recurrence-derived lower bound, crossing window, slope threshold, first-crossing logic, and tangency exclusion form a coherent proof. Supplied Lean declarations match the stated ν≥0, x>0 and 1/2<c<1 hypotheses.
- Rigor
- The paper sharply separates classical classification, candidate-new quantitative results, exact formal statements, certified historical numerics, and paper-level remarks. Edge cases, parameter ranges, and the non-exported curvature identity are disclosed precisely.
- Novelty
- The diagonal family, sharp endpoint regimes, and qualitative crossing are prior art. The credible novelty is the complete quantitative package: unique transversal crossing, explicit threshold and window, orientation, scale law, and formal tangency exclusion.
- Significance
- This is a strong specialized result in certified special-function inequalities and formal analysis, but its present impact is narrower than a broad field-level advance and it does not address a Millennium problem.
- Reproducibility
- The exact PDF, source, diff, provenance, and historical Lean excerpts are pinned and manifest-verified. I did not run Lean, and the interval-arithmetic companion and its transcript are referenced in the repository but are not distributed in this ZIP.
Strengths
- The theorem hypotheses and definitions are explicit: real order ν≥0, x>0, real c, and the Γ-power-series Bessel object rather than an unidentified external library function.
- The proof architecture exposes the load-bearing steps: calibrated Riccati nullcline, recurrence inversion, finite sign witnesses, crossing derivatives, and exclusion of threshold tangency.
- Prior art is handled candidly: the family, endpoint classification, Turán inequality, and qualitative crossing are not presented as new mathematics.
- The distinction among exact Lean statements, historical certified computation, ordinary verification, and paper-level remarks is unusually clear.
Weaknesses
- The supplied formal files are historical excerpts with imports not included as a buildable checkout, so the claimed 8175-job build and axiom output were not independently reproduced here.
- The certified 30-pair interval companion is described in detail but its script and transcript are absent from this package, preventing a local certificate rerun.
- The result is confined to the in-core Γ-series definition at ν≥0 and is not formally identified with a general external special-functions object.
- The distributed revision.diff records the bounded correction patch but does not reconstruct final paper.tex byte-for-byte after disclosed post-Astra edits and line-ending normalization.
Potential errors
- A residual risk lies in the unexecuted transitive formal dependencies: reading the displayed declarations cannot substitute for rebuilding the pinned repository.
- The literature-priority statement for the complete quantitative crossing package is prudent but not supported by an exhaustive independent search in this assessment.
- No algebraic counterexample was found to the displayed threshold, curvature identity, or scale law; the latter correctly weakens a strict lower threshold to a non-strict bound.
Strong novelty candidates
- The unconditional unique-crossing theorem with global bilateral orientation for every ν≥0 and 1/2<c<1 appears materially stronger than the cited qualitative crossing observation.
- The exact no-critical-contact identity and its use to convert a weak crossing threshold into a strict one are strong reusable contributions.
- The constructive location window and two-sided scale law provide quantitative information not visibly supplied by the cited endpoint-classification literature.
Unresolved material objections
None reported.
arr:assessment:28e5f7c1-1440-470f-bd12-e95727a28202 · prompt ARR-INTAKE-ASSESS-1.1 · runtime identity: OpenAI gpt-5.6-sol · reasoning effort: medium · basis: operator verified ui · evidence SHA-256 abbd2c526fa6e322bf7709b7f12924ab12ba0b2bbb6af7e3ee72bf942f531fcb · response SHA-256 05a5635ac73bcab8caf519bfce8754406c7c23d3869da9eb1e859257751b7fcf · canonical PDF SHA-256 eabefc6d93e453b5599f7c1e8c1c7c311352c43d7d61eec0223dced09720ce0c
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.