The Hodge Conjecture and Constructive Omniscience: A Calibration of Algebraic Descent and Archimedean Polarization (Paper 49, Lean 4 Formalization)

Paper 48 Description: Lean 4 formalization and companion paper applying constructive reverse mathematics to the Hodge Conjecture for smooth projective varieties over the complex numbers. The formalization proves five groups of results calibrating the constructive strength of the conjecture. Theorem H1 establishes that deciding Hodge type (r,r) is equivalent to the Limited Principle of Omniscience for the complex numbers (LPO). Theorem H2 shows that deciding rationality of a cohomology class requires LPO, with Markov's Principle needed for the witness search. Theorem H3 demonstrates that Archimedean polarization via the Hodge-Riemann form is positive-definite on (r,r)-classes (available, since the u-invariant u(R)=1) but blind to the rational lattice (periods are transcendental). Theorem H4 proves that numerical equivalence of algebraic cycles is decidable in Bishop's constructive mathematics (BISH), since intersection numbers land in the integers. Theorem H5, the nexus theorem, shows that detecting Hodge classes requires LPO, but the Hodge Conjecture itself reduces detection to BISH plus Markov's Principle by converting the problem from complex cohomology (where equality requires LPO) to rational cohomology (where equality is decidable). Neither polarization nor algebraic descent alone suffices. The Lean 4 bundle builds with zero errors, zero warnings, and zero sorries. All theorems are machine-checked from 28 explicitly documented axioms encoding the cohomology infrastructure and encoding lemmas. Lean 4 v4.29.0-rc1, Mathlib4.