What question did this study set out to answer?

The research aims to establish a transfer of decidability from characteristic p to characteristic 0 in the context of abelian varieties and Standard Conjecture D.

February 24, 2026Open Access

Decidability Transfer via Specialization: Standard Conjecture D for Abelian Threefolds (Paper 52, Constructive Reverse Mathematics Series)

Puntos clave

The research aims to establish a transfer of decidability from characteristic p to characteristic 0 in the context of abelian varieties and Standard Conjecture D.
Proved the implications between numerical and homological equivalence for abelian varieties of dimension ≤ 3.
Utilized the Fulton specialization map for decidability transfer.
Applied structural properties of the Lefschetz ring and smooth proper base change isomorphism.
Established that all Tate classes for g ≤ 3 are Lefschetz classes.
Demonstrated the validity of the core theorem without custom axioms.
Formalized results in Lean 4 with zero compilation errors and verified theorems.

Resumen

Paper 52 of the Constructive Reverse Mathematics series. We prove that Standard Conjecture D (numerical equivalence implies homological equivalence) for abelian varieties A/Q of dimension g = 6, Agugliaro (2025) constructs non-liftable exotic classes providing explicit counterexamples. The logical transfer architecture is formalized in Lean 4 over Mathlib (4 source files, 369 lines). The bundle compiles with zero errors, zero warnings, and zero sorry's. Both the core theorem (subₗefschetzₙondegenerate) and the main theorem (decidabilityₜransfergₗe₃) use ZERO custom axioms. The three geometric inputs enter as hypotheses, not axioms, making both theorems pure logical implications. In the CRM interpretation, the result demonstrates that BISH-decidable equality on numerical motives over Fₚ transfers to BISH-decidable equality over Q through the Lefschetz operators that survive reduction to characteristic p. Upload Type: software Publication Date: 2026-02-20 Keywords: constructive reverse mathematics Standard Conjecture D decidability transfer specialization map abelian varieties abelian threefolds Tate conjecture Lefschetz ring Rosati involution numerical equivalence homological equivalence Chow groups algebraic geometry constructive mathematics BISH formal verification Lean 4 Mathlib License: Apache License 2. 0 (code) ; CC-BY-4. 0 (paper) Copyright Notice: Copyright (c) 2026 Paul Chun-Kit Lee. Code licensed under Apache 2. 0. Paper licensed under Creative Commons Attribution 4. 0 International (CC-BY-4. 0). Files to Upload: paper52decidabilityₜransfer. zip (contains all files below) paper52decidabilityₜransfer. tex -- LaTeX source paper52decidabilityₜransfer. pdf -- Compiled paper (17 pages) README. md -- Bundle documentation REPRODUCIBILITY. md -- Build and verification details. zenodo. json -- Machine-readable metadata P52DecidabilityTransfer/ -- Lean 4 formalization bundle lean-toolchain -- Lean 4 v4. 29. 0-rc1 lakefile. lean -- Lake build configuration lake-manifest. json -- Pinned Mathlib dependency Papers. lean -- Root import Papers/P52DecidabilityTransfer/ Core/SubLefschetzNonDegenerate. lean -- 111 lines: core theorem (full proof) Defs/GeometricAxioms. lean -- 88 lines: GeometricData structure Main/DecidabilityTransfer. lean -- 81 lines: 7-step transfer proof Main/AxiomAudit. lean -- 89 lines: axiom verification Notes: AI-assisted formalization using Claude (Anthropic, Opus 4. 6) for Lean 4 code generation under human direction. All mathematical content specified by the author; every theorem verified by the Lean 4 type checker. Built with Lean 4 v4. 29. 0-rc1 and Mathlib. Reproducible via 'lake build' (zero errors, zero sorry, zero custom axioms). Code available exclusively on Zenodo (not hosted on GitHub). Part of the Foundation Relativity series applying constructive reverse mathematics to the Standard Conjectures program. See Paper 50 (Atlas Survey) for series overview.

Leer artículo completoexternamente

Me gusta

Guardar

Ver artículo completo