What does this research mean for the field?

Deciding membership in ker(Frob − I) on ℓ-adic cohomology is equivalent to LPO(ℚ_ℓ). Novelty: ClaimNovelty.NOVEL_FINDING. Consensus alignment: ConsensusAlignment.NEUTRAL.

What question did this study set out to answer?

This research aims to evaluate the logical strength of the Tate Conjecture and its relationship with LPO in algebraic geometry.

February 20, 2026Open Access

The Tate Conjecture and LPO: Galois-Invariance, Cycle Verification, and Standard Conjecture D as a Decidability Axiom (Paper 46, Constructive Reverse Mathematics Series)

Key Points

This research aims to evaluate the logical strength of the Tate Conjecture and its relationship with LPO in algebraic geometry.
Application of constructive reverse mathematics (CRM) to the Tate Conjecture.
Establishment of four theorems classifying components that require LPO and those compatible with BISH.
Proof of cycle verification using intersection pairing and algebraic cycles.
Formalization in Lean 4 with documented axioms and results.
T1 establishes the equivalence between Galois-invariance and LPO in cohomology contexts.
T2 confirms decidability of numerical equivalence of algebraic cycles within BISH.
T3 reveals a limitation on polarization in certain dimensions due to u-invariants.
T4 demonstrates that Homological equivalence requires LPO and connects it to BISH-decidable numerical equivalence.

Abstract

Paper 46 of the Constructive Reverse Mathematics series. We apply CRM to calibrate the logical strength of the Tate Conjecture for smooth projective varieties over finite fields. We establish four theorems (T1–T4) that classify which components require LPO and which are BISH-compatible. T1 (Galois-Invariance ↔ LPO): Deciding membership in ker (Frob − I) on ℓ-adic cohomology is equivalent to LPO (ℚ_ℓ). The forward direction encodes a scalar a ∈ ℚ_ℓ into a vector where Galois-invariance decides a = 0 ∨ a ≠ 0. T2 (Cycle Verification in BISH): Given a finite complementary basis, numerical equivalence of algebraic cycles is decidable in BISH — requiring only finitely many integer equality tests via the intersection pairing. No omniscience of any kind is needed. Full proof using Int. decEq and Fintype. decidableForallFintype. T3 (Polarization Obstruction): The Poincaré pairing on V = H^2r_ét (X, ℚ_ℓ (r) ) cannot be anisotropic in dimension ≥ 5, because the u-invariant of ℚ_ℓ is 4. This permanently blocks the polarization strategy over ℓ-adic fields. T4 (Standard Conjecture D as Decidability Axiom): T4a shows that deciding homological equivalence (cycle class equality in ℚ_ℓ-cohomology) requires LPO (ℚ_ℓ). T4b shows that Grothendieck's Standard Conjecture D converts homological equivalence to BISH-decidable numerical equivalence. SCD is precisely the axiom that de-omniscientizes the morphism spaces of the motivic category, converting LPO-dependent ℓ-adic zero-testing to decidable integer arithmetic. The Lean 4 / Mathlib formalization comprises 6 source files (771 lines), compiles with zero errors, zero warnings, and zero sorry. 21 custom axioms, all explicitly documented. Theorems T1 and T2 are full proofs; T3 and T4 derive consequences from explicitly documented axioms. Classical. dec does not appear; decidability in T2 and T4b derives from integer decidability and SCD, not from classical omniscience. Code is distributed exclusively via this Zenodo record.

Mark Helpful

Bookmark

Relay

View Full Paper