Read-back: HodgeConjecture.existsUnique_cycleClass

Shape of the statement

For every choice of natural numbers $N, n, p$ with $p \le n$, and every pair of "projective varieties" $X, Z$ in the sense defined below (both living in the same ambient $\mathbb{P}^N$-model), if

• $X$ is "nonsingular of dimension $n$" (definition below),
• the cone of $Z$ is contained in the cone of $X$ (as subsets of $\mathbb{C}^{N+1}$),
• $Z$ is "irreducible" (definition below), and
• the "dimension" of $Z$ equals $n - p$ (natural-number subtraction; harmless here because $p \le n$),

then there exists a unique element $c$ of the complex vector space $H^{2p}(X)$ (the custom cohomology defined below) such that $c$ "is a cycle class of $Z$" in the custom sense $\mathrm{IsCycleClass}_X(Z, n, p, c)$ spelled out below. Uniqueness means: any $c'$ in $H^{2p}(X)$ satisfying the same property is equal to $c$ as an element of the quotient space $H^{2p}(X)$ (i.e. two closed representatives of $c$ and $c'$ differ by an element of the "exact forms" submodule). Nothing else is asserted; in particular $c$ ranges over the whole complex vector space $H^{2p}(X)$ with no rationality, integrality or Hodge-type condition in the statement.

Everything below unfolds the custom notions to Mathlib primitives.

Ambient objects

• Coordinates. $\mathrm{Coord}_N := \mathbb{C}^{N+1}$ (functions $\{0,\dots,N\}\to\mathbb{C}$).
• Polynomials. $\mathrm{Poly}_N :=$ polynomials over $\mathbb{C}$ in the $N+1$ variables $x_0,\dots,x_N$.
• Ambient space. $\mathrm{Amb}_N := \mathbb{C}^{(N+1)\times(N+1)}$, the space of $(N+1)\times(N+1)$ complex matrices with the $\ell^2$ (Hilbert–Schmidt/Frobenius) inner product $\langle A,B\rangle = \sum_{i,j}\overline{A_{ij}}B_{ij}$; it is a complex inner-product space of real dimension $2(N+1)^2$.
• Projection map. $\pi:\mathbb{C}^{N+1}\to \mathrm{Amb}_N$,

$$\pi(v)_{ij} = \frac{v_i\,\overline{v_j}}{\sum_k |v_k|^2}.$$

For $v\neq 0$ this is the rank-one Hermitian projector onto the line $\mathbb{C}v$; it is constant on complex lines through $0$. For $v=0$ the denominator is $0$ and division by zero in $\mathbb{C}$ returns $0$, so $\pi(0)$ is the zero matrix (this case never arises below, since cones exclude $0$).

• $J$-map. For matrices $P,A$: $J_P(A) := i\,(AP - PA) = i[A,P]$.
• Real inner product. $\langle a,b\rangle_{\mathbb{R}} := \operatorname{Re}\langle a,b\rangle$ on $\mathrm{Amb}_N$.
• Zero set. For a set $S$ of polynomials, $\mathcal{Z}(S) := \{v\in\mathbb{C}^{N+1} : Q(v)=0 \text{ for all } Q\in S\}$.

"Projective varieties" and their attributes

A ProjVariety $X$ over $N$ is a set $E_X$ of polynomials (no finiteness assumed) together with a proof that every $Q\in E_X$ is homogeneous of some degree $d_Q\in\mathbb{N}$ (each polynomial may have its own degree; degree $0$, i.e. constants, including nonzero constants, is allowed; the zero polynomial counts as homogeneous). Nothing else is recorded.

• Cone. $C_X := \{v\in\mathbb{C}^{N+1} : v\neq 0,\ v\in\mathcal{Z}(E_X)\}$, the nonzero common zeros of $E_X$. It may be empty (e.g. if $E_X$ contains a nonzero constant).
• Points. $\mathrm{pts}_X := \pi(C_X)\subseteq \mathrm{Amb}_N$, the set of rank-one projectors onto lines of the cone (a model of the projective variety inside matrix space).
• Vanishing set. $I_X := \{Q\in\mathrm{Poly}_N : Q(v)=0 \text{ for all } v\in C_X\}$; all polynomials (homogeneous or not) vanishing on the cone. If $C_X=\emptyset$ then $I_X$ is all polynomials.
• Jacobian form. For $Q$ and $v$: the $\mathbb{C}$-linear map $dQ_v:\mathbb{C}^{N+1}\to\mathbb{C}$, $u\mapsto\sum_i \frac{\partial Q}{\partial x_i}(v)\,u_i$.
• Tangent cone. For any $v\in\mathbb{C}^{N+1}$ (not only $v\in C_X$),

$$T_X(v) := \bigcap_{Q\in I_X}\ker(dQ_v)\ \subseteq\ \mathbb{C}^{N+1},$$

a complex subspace (the Zariski tangent space of the affine cone at $v$, computed from the full vanishing set $I_X$, not from $E_X$).

• IsNonsingular $n$. $X$ is nonsingular of dimension $n$ iff for every $v\in C_X$, $\dim_{\mathbb{C}} T_X(v) = n+1$. This is vacuously true when $C_X=\emptyset$.
• Tangent space at a point. For $P\in\mathrm{Amb}_N$,

$$\mathcal{T}_X(P) := \sum_{\substack{v\in C_X\\ \pi(v)=P}} D\pi_v\big(T_X(v)\big)\ \subseteq\ \mathrm{Amb}_N,$$

the real subspace spanned by the images of the tangent cones $T_X(v)$ (viewed as real subspaces) under the real Fréchet derivative $D\pi_v:\mathbb{C}^{N+1}\to\mathrm{Amb}_N$ of $\pi$ at $v$, summed over all $v$ in the fibre of $\pi$ over $P$ lying in the cone. If no such $v$ exists (in particular if $P\notin\mathrm{pts}_X$) this is the zero subspace. ($\pi$ is smooth away from $0$, so for $v\in C_X$ this is the genuine derivative; it kills the direction $\mathbb{C}v$ since $\pi$ is constant on complex lines.)

• IsIrreducible. $X$ is irreducible iff $C_X\neq\emptyset$ and for all sets of polynomials $S_1,S_2$ (arbitrary, not necessarily homogeneous): if $C_X\subseteq\mathcal{Z}(S_1)\cup\mathcal{Z}(S_2)$ then $C_X\subseteq\mathcal{Z}(S_1)$ or $C_X\subseteq\mathcal{Z}(S_2)$.
• Dimension.

$$\dim X := \Big(\inf\{\dim_{\mathbb{C}} T_X(v) : v\in C_X\}\Big) \;\dot{-}\; 1,$$

where the infimum is over a set of natural numbers (so it is a minimum when $C_X\neq\emptyset$, and equals $0$ by Mathlib's convention $\inf\emptyset = 0$ when $C_X=\emptyset$), and $\dot{-}$ is truncated subtraction on $\mathbb{N}$ ($0\dot{-}1 = 0$). So $\dim X = 0$ both when the cone is empty and when the minimum tangent rank is $0$ or $1$.

• Regular points. $\mathrm{reg}_X := \pi\big(\{v\in C_X : \dim_{\mathbb{C}}T_X(v) = \dim X + 1\}\big)$: images of cone points whose tangent-cone rank is exactly $\dim X + 1$. If the minimum rank $m$ over the cone is $\ge 1$, then $\dim X + 1 = m$ and $\mathrm{reg}_X$ is the (nonempty) image of the rank-minimising locus. If $C_X=\emptyset$, $\mathrm{reg}_X=\emptyset$; if $m=0$ then $\dim X+1 = 1\ne m$ and $\mathrm{reg}_X$ could be empty. (For $v$ in a cone, $v$ itself lies in $\ker dQ_v$ for every $Q$ vanishing on the cone, by Euler's relation applied to the homogeneous components, so in fact $m\ge 1$ whenever the cone is nonempty; the definition does not rely on this.)

Forms and the custom cohomology

• $k$-forms. $\Omega^k_N :=$ all functions $\omega:\mathrm{Amb}_N\to \mathrm{Alt}^k_{\mathbb{R}}(\mathrm{Amb}_N;\mathbb{C})$, where the target is the space of continuous real-multilinear alternating maps $(\mathrm{Amb}_N)^k\to\mathbb{C}$. No regularity is built in; forms live on the whole ambient matrix space, not on $X$. A $0$-form is just a function $\mathrm{Amb}_N\to\mathbb{C}$. $\Omega^k_N$ is a complex vector space (scalars act on values).
• Vanishes on $X$. $\omega\in\Omega^k_N$ vanishes on $X$ iff for every $P\in\mathrm{pts}_X$ and every $k$-tuple $(v_1,\dots,v_k)$ with all $v_i\in\mathcal{T}_X(P)$, $\omega_P(v_1,\dots,v_k)=0$. (For $k=0$ this says $\omega(P)=0$ for all $P\in\mathrm{pts}_X$.)
• Exterior derivative. $d\omega\in\Omega^{k+1}_N$ is Mathlib's extDeriv: at each point, the alternating $(k+1)$-form obtained from the real Fréchet derivative of $\omega$, $(d\omega)_P(v_0,\dots,v_k)=\sum_i (-1)^i\,(D\omega_P\cdot v_i)(v_0,\dots,\widehat{v_i},\dots,v_k)$; at points where $\omega$ is not differentiable the derivative is $0$. (It is used only inside "vanishes on $X$" conditions, which are insensitive to nonzero normalisation constants.)
• Smooth. "$\omega$ is smooth" means $C^\infty$ over $\mathbb{R}$ as a map from all of $\mathrm{Amb}_N$ into the normed space of alternating maps.
• IsClosedForm. $\omega\in\Omega^k_N$ is closed for $X$ iff $\omega$ is smooth and $d\omega$ vanishes on $X$ (in the tangential sense above). Note $\omega$ itself is not required to vanish or be anything on $X$; closedness is tested only on $\mathcal{T}_X(P)$ for $P\in\mathrm{pts}_X$.
• IsExactForm. For $k=0$: $\omega$ is smooth and vanishes on $X$. For $k\ge1$: $\omega$ is smooth and there exists a smooth $\alpha\in\Omega^{k-1}_N$ with $\omega - d\alpha$ vanishing on $X$.
• Closed / exact submodules. $\mathcal{C}^k_X := \operatorname{span}_{\mathbb{C}}\{\omega : \omega \text{ closed for } X\}$ and $\mathcal{E}^k_X := \operatorname{span}_{\mathbb{C}}\{\omega : \omega \text{ exact for } X\}$, both complex subspaces of $\Omega^k_N$.
• Cohomology. $H^k(X) :=$ the image of $\mathcal{C}^k_X$ under the canonical quotient map $\Omega^k_N\to\Omega^k_N/\mathcal{E}^k_X$; a complex subspace of that quotient. Its elements are classes $[\omega]$ with $\omega\in\mathcal{C}^k_X$, and $[\omega]=[\omega']$ iff $\omega-\omega'\in\mathcal{E}^k_X$. (Nothing in the definition forces $\mathcal{E}^k_X\subseteq\mathcal{C}^k_X$.)
• Class. For $\omega\in\mathcal{C}^k_X$, $\mathrm{cls}_X(\omega) := [\omega]\in H^k(X)$.

Frames, measures, wedge, pairing, integral

• $J$-frame. Given a real subspace $T\subseteq\mathrm{Amb}_N$, a matrix $P$, and $u=(u_0,\dots,u_{m-1})$ in $\mathrm{Amb}_N$: $u$ is a $J$-frame for $(T,P)$ iff (i) every $u_i\in T$; (ii) $\langle u_i,u_j\rangle_{\mathbb{R}}=\delta_{ij}$ (real orthonormality for $\operatorname{Re}\langle\cdot,\cdot\rangle$); (iii) $\langle u_i, J_P u_j\rangle_{\mathbb{R}} = 0$ for all $i,j$. It is not required that $J_P u_j\in T$, nor that the family span anything. For $m=0$ the empty family is trivially a $J$-frame.
• Chosen frame. $\mathrm{frame}(T,P,d)\in(\mathrm{Amb}_N)^d$ is built as follows. Let $u=(u_0,\dots,u_{\lfloor d/2\rfloor-1})$ be some $J$-frame for $(T,P)$ of length $\lfloor d/2\rfloor$, chosen by Hilbert's $\varepsilon$-operator (Classical.epsilon): if at least one such frame exists, $u$ is an unspecified one of them; if none exists, $u$ is an unspecified arbitrary family in $(\mathrm{Amb}_N)^{\lfloor d/2\rfloor}$ with no properties at all. The choice is a fixed but unknown function of $(T,P,d)$, with no continuity or measurability in $P$. Then, for index $k\in\{0,\dots,d-1\}$:

$$\mathrm{frame}(T,P,d)_k = \begin{cases} u_{k/2} & k \text{ even},\ \lfloor k/2\rfloor<\lfloor d/2\rfloor,\\ J_P\,u_{(k-1)/2} & k \text{ odd},\ \lfloor k/2\rfloor<\lfloor d/2\rfloor,\\ 0 & \text{otherwise (only when } d \text{ is odd and } k=d-1).\end{cases}$$

So the frame is the interleaved family $(u_0, J_Pu_0, u_1, J_Pu_1, \dots)$, with a trailing zero vector when $d$ is odd. In this theorem the frames used have even length ($2n$ and $2(n-p)$), so no zero entry occurs.

• Volume measure. On $\mathrm{Amb}_N$,

$$\mu_d := \frac{\pi^{\lfloor d/2\rfloor}}{\lfloor d/2\rfloor!\; 2^{d}}\ \cdot\ \mathcal{H}^{d},$$

where $\mathcal{H}^d$ is Mathlib's $d$-dimensional Hausdorff measure on the metric space $\mathrm{Amb}_N$ (Hilbert–Schmidt metric), which carries no intrinsic normalisation. For even $d=2m$ the constant is $\pi^m/(m!\,2^{2m})$, i.e. (volume of the unit $d$-ball)$/2^d$, the classical factor that rescales unnormalised Hausdorff measure to Lebesgue measure on $d$-dimensional Euclidean subspaces; for odd $d$ the floor makes the constant differ from that classical factor (odd $d$ does not occur in this theorem). For $d=0$, $\mu_0=\mathcal{H}^0$ is counting measure.

• Wedge value. For $\omega\in\Omega^k_N$, $\eta\in\Omega^l_N$, a point $P$ and a family $f=(f_0,\dots,f_{k+l-1})$:

$$(\omega\wedge\eta)_P(f) := \frac{1}{k!\,l!}\sum_{\sigma\in S_{k+l}}\operatorname{sgn}(\sigma)\ \omega_P\big(f_{\sigma(0)},\dots,f_{\sigma(k-1)}\big)\ \eta_P\big(f_{\sigma(k)},\dots,f_{\sigma(k+l-1)}\big).$$

• Pairing on $X$. For $\omega\in\Omega^k_N$, $\eta\in\Omega^l_N$:

$$\langle\omega,\eta\rangle_X := \int_{P\in\mathrm{pts}_X} (\omega\wedge\eta)_P\big(\mathrm{frame}(\mathcal{T}_X(P),P,k+l)\big)\ d\mu_{k+l}(P)\ \in\mathbb{C},$$

a Bochner integral over the set $\mathrm{pts}_X$ (all points of $X$, singular or not) of the complex number obtained by evaluating $\omega\wedge\eta$ at $P$ on the chosen $J$-frame of $\mathcal{T}_X(P)$ of length $k+l$. By Mathlib's convention the integral is $0$ if the integrand is not integrable (including not almost-everywhere strongly measurable) with respect to $\mu_{k+l}$ restricted to $\mathrm{pts}_X$.

• Integral over $Z$. For $\eta\in\Omega^l_N$:

$$\int_Z\eta := \int_{P\in\mathrm{reg}_Z}\eta_P\big(\mathrm{frame}(\mathcal{T}_Z(P),P,l)\big)\ d\mu_l(P)\ \in\mathbb{C},$$

integrating only over the regular points of $Z$ against $\mu_l$, using $Z$'s own tangent spaces and frames; same $0$-for-non-integrable convention.

The cycle-class property

For $c\in H^{2p}(X)$: $\mathrm{IsCycleClass}_X(Z,n,p,c)$ holds iff

$$\forall\,\omega\in\mathcal{C}^{2p}_X \text{ with } [\omega]=c,\quad \forall\,\eta\in\Omega^{2n-2p}_N \text{ closed for } X:\qquad \langle\omega,\eta\rangle_X = \int_Z\eta .$$

Here $2n-2p$ is natural-number subtraction (equal to $2(n-p)$ because $p\le n$), the pairing uses frames of length $2p+(2n-2p)=2n$ in $\mathcal{T}_X(P)$ against $\mu_{2n}$ on $\mathrm{pts}_X$, and the right-hand side uses frames of length $2(n-p)$ in $\mathcal{T}_Z(P)$ against $\mu_{2(n-p)}$ on $\mathrm{reg}_Z$. The quantifier runs over every closed representative $\omega$ of $c$ (not just one), and over every $\eta$ that is closed for $X$ (smooth on $\mathrm{Amb}_N$ with $d\eta$ vanishing on $X$'s tangent spaces); $\eta$ is then integrated over $Z$ using $Z$'s tangent data.

Full statement, assembled

$$\forall N,n,p\in\mathbb{N},\ p\le n,\ \forall X,Z\ \text{ProjVarieties over } N:\quad \Big[\forall v\in C_X,\ \dim_{\mathbb{C}}T_X(v)=n+1\Big]\ \wedge\ C_Z\subseteq C_X\ \wedge\ Z\ \text{irreducible}\ \wedge\ \dim Z = n-p$$ $$\Longrightarrow\quad \exists!\,c\in H^{2p}(X):\ \forall\,\omega\in\mathcal{C}^{2p}_X,\ [\omega]=c \Rightarrow \forall\,\eta\in\Omega^{2n-2p}_N \text{ closed for } X,\ \langle\omega,\eta\rangle_X=\int_Z\eta .$$

Edge cases, degenerate inputs, junk values

• Nonemptiness forced. Irreducibility of $Z$ includes $C_Z\neq\emptyset$; with $C_Z\subseteq C_X$ this forces $C_X\neq\emptyset$, so the nonsingularity hypothesis on $X$ is not vacuous, $\dim X = (n+1)\dot{-}1 = n$, and $\mathrm{reg}_X = \mathrm{pts}_X$. The hypotheses are jointly satisfiable (e.g. $X$ a linear $\mathbb{P}^n\subseteq\mathbb{P}^N$ cut out by linear forms and $Z$ a linear subspace of dimension $n-p$).
• Natural subtraction. $n-p$ and $2n-2p$ are genuine because $p\le n$. $\dim Z = m\dot{-}1$ with $m$ the minimum tangent rank on $C_Z$; the hypothesis $\dim Z = n-p$ reads $m\dot{-}1 = n-p$, i.e. $m = n-p+1$ when $m\ge1$; if $m$ were $0$ it would force $p=n$ and $\mathrm{reg}_Z$ could be empty (then $\int_Z\eta=0$ for all $\eta$). $\inf\emptyset=0$ does not arise since $C_Z\ne\emptyset$.
• $p=n$. Then $\eta$ is a $0$-form (a smooth function with $d\eta$ vanishing on $X$'s tangents), $\int_Z\eta$ is the integral of $\eta$ over $\mathrm{reg}_Z$ against counting measure $\mu_0$ (a finite sum if $\mathrm{reg}_Z$ is finite; $0$ if $\eta$ is not integrable for counting measure on $\mathrm{reg}_Z$), and $(\omega\wedge\eta)_P(f)=\omega_P(f)\,\eta(P)$.
• $p=0$. $c$ is a class of $0$-forms modulo $\mathcal{E}^0_X$ (smooth functions vanishing on $\mathrm{pts}_X$); $\omega$ is a smooth function whose derivative vanishes on $\mathcal{T}_X(P)$ at points of $X$; frames of length $2n$ are used on both sides ($\dim Z=n$).
• $N=0$. $\mathrm{Amb}_0=\mathbb{C}$, $\pi(v)=1$ for $v\neq0$, so $\mathrm{pts}_X\subseteq\{1\}$; only $n=p=0$ is compatible with tangent rank $1$.
• Frame junk. If for some $P$ no $J$-frame of the required length exists in $\mathcal{T}_X(P)$ (or $\mathcal{T}_Z(P)$), the $\varepsilon$-operator returns an arbitrary family with no orthonormality or membership properties, and the integrand at $P$ is whatever the form gives on that family. Even when frames exist, the choice $P\mapsto\mathrm{frame}(\cdot,P,\cdot)$ is unspecified and need not be measurable; if the resulting integrand fails to be a.e.-strongly measurable or integrable, the Bochner integral is $0$ by convention, on either side of the equation independently.
• Frame ordering/orientation. Evaluation of a top-degree alternating form on the frame depends on the interleaved order $(u_0,J_Pu_0,u_1,J_Pu_1,\dots)$ and on which $J$-frame $\varepsilon$ selects; the definition fixes one such choice per $(T,P,d)$ once and for all.
• Measure normalisation. Both integrals use Hausdorff measure scaled by $\pi^{m}/(m!\,4^{m})$ with $d=2m$; the scale on the left is for $d=2n$ and on the right for $d=2(n-p)$.
• Domain of integration. The pairing integrates over all of $\mathrm{pts}_X$; the right-hand side integrates over $\mathrm{reg}_Z\subseteq\mathrm{pts}_Z\subseteq\mathrm{pts}_X$, the points of $Z$ of minimal tangent rank, using $Z$'s tangent spaces $\mathcal{T}_Z(P)$ (computed from $Z$'s own vanishing set $I_Z$), not $X$'s.
• Forms are ambient. All forms are functions on the entire matrix space $\mathrm{Amb}_N$ with real-multilinear alternating values in $\mathbb{C}$; smoothness is required everywhere on $\mathrm{Amb}_N$, while "closed" and "exact" are tested only tangentially along $X$.
• Cohomology is complex. $H^{2p}(X)$ is a $\mathbb{C}$-vector space (spans over $\mathbb{C}$); the unique $c$ is an element of it, and uniqueness is equality modulo $\mathcal{E}^{2p}_X$.