The Tate Conjecture as a Parametric Proposition: A Machine-Checked Lean 4 Interface without Axioms

The Tate conjecture stated in Lean 4 as a proposition over an explicit structure TateSetting (replacing four earlier user-declared axioms), carrying hosts, cycle-class types, Galois invariants in étale cohomology and a cycle class map. Proved for every setting: the statement is exactly surjectivity of the cycle class map, and the fourfold-surfaces case is the codimension-2 statement. Not proved: the Tate conjecture or any case of it. The Lean development builds in CI (green on the commit archived here) with no sorry and no user-declared axioms. Source: https://github.com/BenFrohman/TateConjecture at commit f7235b3ba96d81a281d60d70cfb2ff1e98fa5ab5.