Three Axioms for the Motive: Constructive Reverse Mathematics Meets Grothendieck's Universal Cohomology (Paper 50, Lean 4 Formalization)

Mazur, Birch–Swinnerton-Dyer, and Hodge — all encode the same logical pattern: continuous data over a complete field (where zero-testing requires the Limited Principle of Omniscience) secretly descends to discrete algebraic data (decidable in Bishop-style constructive mathematics). We call this pattern "de-omniscientizing descent." Calibrating all five conjectures against the constructive hierarchy BISH ⊂ BISH+MP ⊂ BISH+LPO ⊂ CLASS reveals that Grothendieck's conjectural category of numerical motives is logically specified by exactly three axioms: (1) decidable equality on morphism spaces — equivalently, Standard Conjecture D; (2) algebraic spectrum — endomorphisms satisfy monic Z-polynomials; (3) Archimedean polarization — a positive-definite inner product on the real fiber, which exists over R (where u(R) = ∞) but is obstructed over Q_p by the u-invariant u(Q_p) = 4. The motive category is the initial Decidable Polarized Tannakian (DPT) category equipped with a Weil cohomology functor. From these three axioms: Standard Conjecture D is exactly the axiom that collapses LPO-dependent homological equality to BISH-decidable numerical equality (Theorem A, zero sorries); the Weil Riemann Hypothesis reduces to a single cancellation step (Theorem B, one-line Lean proof, zero sorries); and the subcategory of CM elliptic motives — all 13 rational CM j-invariants from the 9 maximal and 4 non-maximal imaginary quadratic orders of class number 1 — is unconditionally BISH-decidable, with four bridge lemmas (Lieberman, Damerell, Shimura-Taniyama, Lefschetz (1,1)) bypassing every obstruction (Theorem C, zero sorries). The failure boundary is sharp: CM abelian varieties of dimension ≥ 4 require open conjectures. The Lean 4 formalization over Mathlib comprises 8 files (2214 build targets), compiling with 0 errors and 2 principled sorries, using 46 custom axioms (25 True-valued placeholders for upstream results). Theorems A, B, and C carry zero sorries. This is Paper 50 in the Constructive Reverse Mathematics series.