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

Abstract: 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 \ge 0$, the Hodge Conjecture asserts that the rational cohomology classes of type $(p,p)$, denoted $\operatorname{Hdg}^{2p}(X, \mathbb{Q}) = H^{2p}(X, \mathbb{Q}) \cap H^{p,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 $\Delta_d$ yields the orthogonal Helmholtz–Hodge decomposition $\mathbb{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 $\mathfrak{sl}_2(\mathbb{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 $c_{\mathrm{floor}} \coloneqq \lambda_{\min}(Q|_{P^{2p}}) > 0$. For any class $\alpha \in \operatorname{Hdg}^{2p}(X, \mathbb{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 $\sum \nu_j [Z_j]$ with Lelong numbers $\nu_j > 0$, and a diffuse residual current $R$ with $\nu(R, x) \equiv 0$. The spectral coercivity bound $Q(H(R), H(R)) \ge c_{\mathrm{floor}} \|H(R)\|_{L^2}^2$ ensures that $[R] = 0 \in H^{2p}(X, \mathbb{C})$. The exact current discrepancy is regularized by the Green potential $\psi = G(T^+ - T^-)$ via $T^+ - T^- = \alpha + dd^c \psi$. By Poincaré duality, the integer intersection matrix $\mathbf{M} \in \operatorname{Mat}_{m \times m}(\mathbb{Z})$ is non-degenerate, and Cramer's rule shows that the coefficients $\nu_j$ are rational. Since topological torsion vanishes over $\mathbb{Q}$, the cycle class map $\operatorname{cl}_{\mathbb{Q}}: \mathcal{Z}^p(X) \otimes_{\mathbb{Z}} \mathbb{Q} \to \operatorname{Hdg}^{2p}(X, \mathbb{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