De Rham Regularization, Spectral Positivity, and the Cycle Class Map in Hodge Theory

We study the surjectivity of the rational cycle class map on compact complex projective algebraic manifolds. For any complex projective manifold X and integer p ≥ 0, the Hodge Conjecture asserts that the rational cohomology classes of type $(p,p)$, denoted Hdg²ᵖ(X, Q) = H²ᵖ(X, Q) ∩ Hp,p(X), are generated by algebraic cycles with rational coefficients. We address this problem by analyzing the relationship between the harmonic projector, the Hodge Green operator, and the regularization of closed positive currents. On the spectral side, the Hodge Laplacian Δd yields the orthogonal Helmholtz–Hodge decomposition I = H + dd^* G + d^*d G, where G is the self-adjoint Green operator. By Kodaira embedding, the ample polarization induces an action of sl₂(C) on cohomology, ensuring Hard Lefschetz isomorphisms and the primitive decomposition. On primitive subspaces, the classical polarization form Q satisfies the Hodge positivity relations, yielding a positive spectral floor cfloor λₘᵢₙ(Q|_P²ᵖ) > 0. For any class α ∈ Hdg²ᵖ(X, Q), the Demailly–Jordan decomposition yields a representation by closed positive currents T = T⁺ - T⁻. By Siu's analyticity theorem, T⁺ decomposes into a discrete combination of integration currents over irreducible algebraic subvarieties ∑ νⱼ [Zⱼ] with Lelong numbers νⱼ > 0, and a diffuse residual current R with ν(R, x) ≡ 0. The spectral coercivity bound Q(H(R), H(R)) ≥ cfloor \|H(R)\|L²² ensures that [R] = 0 ∈ H²ᵖ(X, C). The exact current discrepancy is regularized by the Green potential ψ = G(T⁺ - T⁻) via T⁺ - T⁻ = α + ddᶜ ψ. By Poincaré duality, the integer intersection matrix M ∈ Matm × m(Z) is non-degenerate, and Cramer's rule shows that the coefficients νⱼ are rational. Since topological torsion vanishes over Q, the cycle class map clQ: Zᵖ(X) ⊗Z Q → Hdg²ᵖ(X, Q) is surjective. We also examine extensions to singular projective varieties via the BBDG decomposition theorem and non-Archimedean degenerations on Berkovich spaces. The deductive structure is formalized in Lean 4 with Mathlib (21 verified theorems, 0 sorry, 0 custom unproven axioms) and evaluated numerically with a Rust implementation. Codebase & Verification Suite: https://github.com/yukeins/FormalizacionHodge