Read-back: HodgeConjecture definition bundle

Ambient conventions used throughout. Fix a natural number $N$ (implicit in every declaration below). Three type abbreviations recur:

• $\mathbb{C}^{N+1}$ (code: Coord N): functions from $\{0,\dots,N\}$ to $\mathbb{C}$, i.e. complex $(N+1)$-vectors $v=(v_0,\dots,v_N)$.
• $\mathcal{A}$ (code: Amb N): the complex Euclidean space indexed by pairs $(i,j)\in\{0,\dots,N\}^2$, i.e. complex $(N+1)\times(N+1)$ matrices $A=(A_{ij})$, carrying the Hermitian inner product $\langle A,B\rangle_{\mathbb C}=\sum_{i,j}\overline{A_{ij}}\,B_{ij}$ (conjugate-linear in the first slot) and the Frobenius norm $\|A\|^2=\sum_{i,j}|A_{ij}|^2$. As a real vector space it is $\mathbb{R}^{2(N+1)^2}$, and its metric is the one induced by this norm.
• $\mathcal{P}$ (code: Poly N): polynomials with complex coefficients in $N+1$ variables $x_0,\dots,x_N$.

In the analytic parts, "smooth" always means $C^\infty$ in the real sense: the smoothness order written ∞ is the element $\top$ of $\mathbb{N}\cup\{\infty\}$ viewed inside $\mathbb{N}\cup\{\infty,\omega\}$, i.e. infinitely differentiable, strictly weaker than real-analytic ($\omega$).

---

proj

For $v\in\mathbb{C}^{N+1}$, $\operatorname{proj}(v)\in\mathcal A$ is the matrix with entries

$$\operatorname{proj}(v)_{ij}=\frac{v_i\,\overline{v_j}}{\ \sum_{k}|v_k|^2\ },$$

where the denominator is the real number $\sum_k |v_k|^2$ cast into $\mathbb C$. For $v\neq 0$ this is the rank-one Hermitian projector $v v^*/\|v\|^2$ onto the line $\mathbb{C}v$; it satisfies $\operatorname{proj}(\lambda v)=\operatorname{proj}(v)$ for every $\lambda\in\mathbb{C}^\times$. For $v=0$ the denominator is $0$ and complex division by zero yields $0$, so $\operatorname{proj}(0)$ is the zero matrix. The function is defined on all of $\mathbb{C}^{N+1}$ with no restriction.

Jmap

For matrices $P,A\in\mathcal A$, $J_P(A)\in\mathcal A$ is the matrix with entries

$$J_P(A)_{ij}=\mathrm{i}\sum_{k}\bigl(A_{ik}P_{kj}-P_{ik}A_{kj}\bigr),\qquad\text{i.e.}\qquad J_P(A)=\mathrm{i}\,(AP-PA)=-\mathrm{i}\,[P,A].$$

It is complex-linear in $A$ for every $P$. Nothing is assumed about $P$ (it need not be a projector), and no property such as $J_P\circ J_P=-\mathrm{id}$ on any subspace is asserted or built in.

cmul

For $P,A\in\mathcal A$ and $z\in\mathbb C$,

$$\operatorname{cmul}_P(z,A)=(\operatorname{Re}z)\,A+(\operatorname{Im}z)\,J_P(A),$$

using real scalar multiplication. It is real-linear in $A$ and real-linear in $z$; for real $z$ it is ordinary scaling $zA$, and for $z=\mathrm{i}$ it is $J_P(A)$. It is not asserted that $\operatorname{cmul}_P(zz',A)=\operatorname{cmul}_P(z,\operatorname{cmul}_P(z',A))$; that would require $J_P^2=-\mathrm{id}$ on the vectors in question.

rinner

For $a,b\in\mathcal A$, $\langle a,b\rangle_{\mathbb R}=\operatorname{Re}\langle a,b\rangle_{\mathbb C}=\sum_{i,j}\bigl(\operatorname{Re}a_{ij}\operatorname{Re}b_{ij}+\operatorname{Im}a_{ij}\operatorname{Im}b_{ij}\bigr)$, the standard real Euclidean inner product on $\mathcal A\cong\mathbb R^{2(N+1)^2}$. It is symmetric and its associated norm is the Frobenius norm.

zeros

For a set $S\subseteq\mathcal P$ of polynomials (any polynomials, not necessarily homogeneous), $Z(S)=\{v\in\mathbb{C}^{N+1}:\ Q(v)=0\ \text{for all } Q\in S\}$, the common zero locus in affine space $\mathbb{C}^{N+1}$. Edge cases: $Z(\varnothing)=\mathbb{C}^{N+1}$; the origin belongs to $Z(S)$ iff every $Q\in S$ has zero constant term.

ProjVariety

A "projective variety" $X$ (in the sense of this bundle) consists of a set of polynomials $\mathrm{eqs}_X\subseteq\mathcal P$ together with a proof that every $Q\in\mathrm{eqs}_X$ is homogeneous of some degree $d_Q\in\mathbb N$ (the degree may vary from polynomial to polynomial). Homogeneous of degree $d$ means every monomial in the support of $Q$ has total degree $d$; in particular the zero polynomial is homogeneous of every degree, and nonzero constants are homogeneous of degree $0$ and are allowed in $\mathrm{eqs}_X$. The set $\mathrm{eqs}_X$ may be empty, infinite, or not an ideal; no irreducibility, reducedness or nonemptiness is part of the structure.

cone

$\operatorname{cone}(X)=\{v\in\mathbb{C}^{N+1}:\ v\neq 0\ \text{and}\ Q(v)=0\ \text{for all }Q\in\mathrm{eqs}_X\}$: the affine cone over $X$ with the origin removed. It is stable under $\mathbb{C}^\times$-scaling. It is empty if, for instance, $\mathrm{eqs}_X$ contains a nonzero constant or contains $x_0,\dots,x_N$.

pts

$\operatorname{pts}(X)=\operatorname{proj}(\operatorname{cone}(X))=\{\,vv^*/\|v\|^2:\ v\in\operatorname{cone}(X)\,\}\subseteq\mathcal A$: the set of rank-one Hermitian projectors onto lines in the cone. This is the model of the point set of the projective variety used everywhere below (integration, tangent spaces, vanishing of forms). It is empty iff the cone is empty, and since $v\ne0$ on the cone the junk value $\operatorname{proj}(0)=0$ never occurs here.

vanishing

$\mathcal I(X)=\{Q\in\mathcal P:\ Q(v)=0\ \text{for all } v\in\operatorname{cone}(X)\}$: all polynomials (homogeneous or not) vanishing on the punctured cone. It always contains $0$ and $\mathrm{eqs}_X$. If the cone is empty, $\mathcal I(X)=\mathcal P$ (every polynomial).

jacobianForm

For $Q\in\mathcal P$ and $v\in\mathbb{C}^{N+1}$, $dQ_v:\mathbb{C}^{N+1}\to\mathbb C$ is the complex-linear map

$$dQ_v(u)=\sum_{i=0}^{N}\frac{\partial Q}{\partial x_i}(v)\;u_i,$$

where $\partial Q/\partial x_i$ is the formal partial derivative and $u\mapsto u_i$ the $i$-th coordinate projection. This is the differential of $Q$ at $v$; it is defined for every $v$, including $v=0$ and $v\notin\operatorname{cone}(X)$.

tangentCone

For $v\in\mathbb{C}^{N+1}$ (any $v$, not only points of the cone),

$$T^{\mathrm{Zar}}_v(X)=\bigcap_{Q\in\mathcal I(X)}\ker(dQ_v)\ \subseteq\ \mathbb{C}^{N+1},$$

a complex-linear subspace: the Zariski tangent space at $v$ of the affine cone, computed with all polynomials vanishing on the punctured cone (not just $\mathrm{eqs}_X$). If the cone is empty then $\mathcal I(X)=\mathcal P$ and the intersection is $\{0\}$ (take $Q=x_i$). Because the cone is $\mathbb{C}^\times$-stable, each homogeneous component of a $Q\in\mathcal I(X)$ again lies in $\mathcal I(X)$, and Euler's identity then gives $dQ_v(v)=0$; consequently $v\in T^{\mathrm{Zar}}_v(X)$ whenever $v\in\operatorname{cone}(X)$, so $\dim_{\mathbb C}T^{\mathrm{Zar}}_v(X)\ge 1$ on the cone.

IsNonsingular

For $n\in\mathbb N$, "$X$ is nonsingular of dimension $n$" means: for every $v\in\operatorname{cone}(X)$, $\dim_{\mathbb C}T^{\mathrm{Zar}}_v(X)=n+1$ (exactly). This is the only content; no separate assertion that $X$ has dimension $n$ in any other sense is made. If the cone is empty the condition holds vacuously for every $n$.

tangent

For $P\in\mathcal A$, $T_P(X)$ is the real-linear subspace of $\mathcal A$ spanned by the union, over all $v\in\mathbb{C}^{N+1}$ with $v\in\operatorname{cone}(X)$ and $\operatorname{proj}(v)=P$, of the images

$$D\!\operatorname{proj}_v\bigl(T^{\mathrm{Zar}}_v(X)\bigr),$$

where $D\!\operatorname{proj}_v:\mathbb{C}^{N+1}\to\mathcal A$ is the real Fréchet derivative of $\operatorname{proj}$ at $v$ and $T^{\mathrm{Zar}}_v(X)$ is regarded as a real subspace. (A supremum of subspaces is the span of their union, so the result is a subspace even if the individual images were not nested.) Junk/edge cases: if $P\notin\operatorname{pts}(X)$ no $v$ qualifies and $T_P(X)=\{0\}$. The Fréchet derivative returns the zero map at points where $\operatorname{proj}$ is not differentiable, but $\operatorname{proj}$ is a rational function with nonvanishing denominator away from $v=0$, and $v=0$ is excluded by the cone condition, so this junk value does not arise. Since $\operatorname{proj}$ is constant along $\mathbb{C}^\times v$, $D\!\operatorname{proj}_v$ kills $v$ and $\mathrm{i}v$; in particular the real dimension of $T_P(X)$ is at most $2\dim_{\mathbb C}T^{\mathrm{Zar}}_v(X)-2$ for each contributing $v$ (given $v\in T^{\mathrm{Zar}}_v(X)$ noted above).

IsIrreducible

"$X$ is irreducible" means: $\operatorname{cone}(X)\neq\varnothing$, and for all sets $S_1,S_2\subseteq\mathcal P$ of polynomials (arbitrary, not required homogeneous), if $\operatorname{cone}(X)\subseteq Z(S_1)\cup Z(S_2)$ then $\operatorname{cone}(X)\subseteq Z(S_1)$ or $\operatorname{cone}(X)\subseteq Z(S_2)$.

dim

$$\dim X=\Bigl(\min\{\dim_{\mathbb C}T^{\mathrm{Zar}}_v(X):\ v\in\operatorname{cone}(X)\}\Bigr)\;\dot-\;1\ \in\mathbb N,$$

the minimum over the punctured cone of the Zariski tangent dimension, minus one, using truncated natural-number subtraction ($a\dot- b=\max(a-b,0)$). The infimum of a nonempty set of naturals is its least element, so for nonempty cone the minimum is attained; by the remark under tangentCone it is then $\ge1$ and no truncation occurs. If the cone is empty, the infimum of the empty set of naturals is $0$ and $0\dot-1=0$, so $\dim X=0$. Note this is the minimum, not the maximum, of tangent dimensions, and it is not defined via chains of subvarieties.

regPts

$\operatorname{regPts}(X)=\operatorname{proj}\bigl(\{v\in\operatorname{cone}(X):\ \dim_{\mathbb C}T^{\mathrm{Zar}}_v(X)=\dim X+1\}\bigr)\subseteq\operatorname{pts}(X)$: the projectors of those cone points at which the Zariski tangent dimension attains its minimum over the cone. Empty iff the cone is empty; if the cone is nonempty this set is nonempty (the minimum is attained).

Form

A "$k$-form" $\omega$ (code: Form N k) is an arbitrary function assigning to each point $P\in\mathcal A$ a continuous, real-multilinear, alternating map $\omega_P:\mathcal A^k\to\mathbb C$. No continuity or smoothness in $P$ is built into the type. For $k=0$, $\omega_P$ is just a complex number, so $0$-forms are arbitrary functions $\mathcal A\to\mathbb C$. The set of $k$-forms is a complex vector space under pointwise operations (scaling the complex values).

VanishesOn

For a $k$-form $\omega$, "$\omega$ vanishes on $X$" means: for every $P\in\operatorname{pts}(X)$ and every $k$-tuple $(v_0,\dots,v_{k-1})$ of vectors of $\mathcal A$ with every $v_i\in T_P(X)$, one has $\omega_P(v_0,\dots,v_{k-1})=0$. Nothing is required at $P\notin\operatorname{pts}(X)$, nor on tuples with some entry outside $T_P(X)$. For $k=0$ the tuple is empty and the condition reads $\omega_P=0$ for all $P\in\operatorname{pts}(X)$. If $\operatorname{pts}(X)=\varnothing$ every form vanishes on $X$.

IsClosedForm

"$\omega$ is closed (relative to $X$)" means: $\omega$ is $C^\infty$ as a map from $\mathcal A$ to the space of alternating maps, and the exterior derivative $d\omega$ vanishes on $X$ in the sense of VanishesOn. Here $d\omega$ is Mathlib's exterior derivative on the flat space $\mathcal A$, built from the real Fréchet derivative:

$$(d\omega)_P(v_0,\dots,v_k)=\sum_{i=0}^{k}(-1)^i\,\bigl(D\omega_P\,[v_i]\bigr)(v_0,\dots,\widehat{v_i},\dots,v_k),$$

where $D\omega_P[v]$ is the directional derivative of $P\mapsto\omega_P$ in direction $v$. At a point where $\omega$ is not differentiable the Fréchet derivative is the zero map and $(d\omega)_P=0$; this junk value cannot occur here because smoothness of $\omega$ on all of $\mathcal A$ is demanded. Note closedness is only required along the tangent spaces at points of $X$, not $d\omega=0$ on $\mathcal A$; and the smoothness is required on all of $\mathcal A$.

IsExactForm

Defined by cases on the degree. A $0$-form $\omega$ is "exact" iff $\omega$ is $C^\infty$ and $\omega$ vanishes on $X$ (i.e. $\omega_P=0$ for all $P\in\operatorname{pts}(X)$). A $(k+1)$-form $\omega$ is "exact" iff $\omega$ is $C^\infty$ and there exists a $C^\infty$ $k$-form $\alpha$ on $\mathcal A$ such that $\omega-d\alpha$ vanishes on $X$ (vanishes on all $(k+1)$-tuples of vectors of $T_P(X)$, at all $P\in\operatorname{pts}(X)$). No condition is placed on $\alpha$ beyond smoothness on $\mathcal A$. Equality $\omega=d\alpha$ is not required, only agreement along tangent tuples of $X$.

closedForms

$Z^k(X)$ is the complex-linear span, inside the space of $k$-forms, of the set of closed forms. A span is a subspace regardless of whether the generating set is; here the generating set is itself stable under complex linear combinations (smoothness, exterior differentiation and the vanishing condition are all compatible with complex scaling of values), so the span coincides with the set of closed forms, but the definition takes the span in any case.

exactForms

$B^k(X)$ is the complex-linear span of the set of exact $k$-forms (as defined above), again a subspace of the space of $k$-forms by construction. It is not asserted that $B^k(X)\subseteq Z^k(X)$.

Cohomology

$H^k(X)$ is the image of $Z^k(X)$ under the quotient map \{\text{k-forms}\}\to\{\text{k-forms}\}/B^k(X); as a set, its elements are the classes $\omega+B^k(X)$ with $\omega\in Z^k(X)$. Canonically $H^k(X)\cong Z^k(X)/\bigl(Z^k(X)\cap B^k(X)\bigr)$. It is a complex vector space.

cls

For $\omega\in Z^k(X)$ (an element of the span of closed forms, carried with a proof of membership), $[\omega]\in H^k(X)$ is its class modulo $B^k(X)$, together with the (automatic) witness that this class lies in the image of $Z^k(X)$.

HasType

For $p,q\in\mathbb N$ and a $k$-form $\omega$, "$\omega$ has type $(p,q)$ on $X$" means: for every $P\in\operatorname{pts}(X)$, every $k$-tuple $(v_0,\dots,v_{k-1})$ with all $v_i\in T_P(X)$, and every $z\in\mathbb C$,

$$\omega_P\bigl(\operatorname{cmul}_P(z,v_0),\dots,\operatorname{cmul}_P(z,v_{k-1})\bigr)=z^{p}\,\bar z^{\,q}\;\omega_P(v_0,\dots,v_{k-1}),$$

where $\operatorname{cmul}_P(z,v)=(\operatorname{Re}z)v+(\operatorname{Im}z)\,\mathrm{i}(vP-Pv)$. No relation between $p+q$ and $k$ is imposed. Edge cases: the quantifier includes $z=0$ and real $z$. At $z=0$ with $k\ge1$ the left side is $0$ by multilinearity while the right side is $0^{p+q}\omega_P(v)$, which equals $\omega_P(v)$ when $p=q=0$ (since $0^0=1$); thus type $(0,0)$ for $k\ge1$ forces $\omega$ to vanish on $X$. For $k=0$ the condition reads $\omega_P=z^p\bar z^q\omega_P$ for all $z$, which for $(p,q)\ne(0,0)$ forces $\omega_P=0$ on $\operatorname{pts}(X)$. If $\operatorname{pts}(X)=\varnothing$ every form has every type.

HasTypeClass

For $p,q\in\mathbb N$ and a class $c\in H^k(X)$, "$c$ has type $(p,q)$" means: there exists $\omega\in Z^k(X)$ with $[\omega]=c$ such that the underlying form $\omega$ has type $(p,q)$ on $X$. (Existential over representatives: one good representative suffices.)

Simplex

A "$k$-simplex" $\sigma$ (code: Simplex N k) is an arbitrary function $\sigma:\mathbb R^{k+1}\to\mathcal A$, defined on all of $\mathbb R^{k+1}=(\{0,\dots,k\}\to\mathbb R)$, with no continuity, smoothness or injectivity built into the type.

Chain

A "$k$-chain" is a finitely supported function from $k$-simplices to $\mathbb Z$, i.e. a formal finite integer combination $\sum_\sigma m_\sigma\,\sigma$ of $k$-simplices.

face

For $i\in\{0,\dots,k+1\}$ and a $(k+1)$-simplex $\sigma:\mathbb R^{k+2}\to\mathcal A$, the $i$-th face $\partial_i\sigma$ is the $k$-simplex $t\mapsto\sigma(t_0,\dots,t_{i-1},0,t_i,\dots,t_k)$, i.e. $\sigma$ restricted to the coordinate hyperplane $\{t_i=0\}$ (with a $0$ inserted at position $i$ of $t\in\mathbb R^{k+1}$).

boundary

For a $(k+1)$-chain $c=\sum_\sigma m_\sigma\sigma$ (sum over the finite support),

$$\partial c=\sum_{\sigma}m_\sigma\sum_{i=0}^{k+1}(-1)^i\,[\partial_i\sigma],$$

the usual simplicial boundary, a $k$-chain. Cancellation between coincident face simplices is by equality of functions $\mathbb R^{k+1}\to\mathcal A$.

IsCycle

A $0$-chain is a cycle unconditionally (the condition is True for every $0$-chain, with no augmentation condition). A $(k+1)$-chain $c$ is a cycle iff $\partial c=0$ as a $k$-chain.

coordSimplex

$\Delta^k=\{t\in\mathbb R^k:\ t_i\ge 0\ \forall i,\ \sum_i t_i\le 1\}$, the standard $k$-simplex in "one-coordinate-dropped" form. For $k=0$, $\mathbb R^0$ is a single point and both conditions are vacuous/true, so $\Delta^0$ is that one point.

affineEmbed

For $t\in\mathbb R^k$, $\iota(t)=(1-\textstyle\sum_i t_i,\ t_0,\dots,t_{k-1})\in\mathbb R^{k+1}$ (the new coordinate is prepended at index $0$). It maps $\Delta^k$ bijectively onto the standard simplex $\{s\in\mathbb R^{k+1}: s_i\ge0,\ \sum s_i=1\}$; for $k=0$ it sends the point to $(1)$.

simplexIntegral

For a $k$-form $\omega$ and a $k$-simplex $\sigma$,

$$\int_\sigma\omega\;=\;\int_{t\in\Delta^k}\ \omega_{\sigma(\iota(t))}\Bigl(D(\sigma\circ\iota)_t(e_0),\dots,D(\sigma\circ\iota)_t(e_{k-1})\Bigr)\,dt,$$

a Bochner integral over $\Delta^k$ with respect to Lebesgue measure on $\mathbb R^k$, where $e_i$ is the $i$-th standard basis vector and $D(\sigma\circ\iota)_t$ is the real Fréchet derivative of $\sigma\circ\iota:\mathbb R^k\to\mathcal A$ at $t$. Junk values: at any $t$ where $\sigma\circ\iota$ is not differentiable the Fréchet derivative is the zero map, so the integrand is $0$ there (for $k\ge1$). If the integrand is not Bochner integrable on $\Delta^k$ (not integrable, or not almost-everywhere strongly measurable), the integral is defined to be $0$. For $k=0$: Lebesgue measure on the one-point space $\mathbb R^0$ has total mass $1$, so $\int_\sigma\omega=\omega_{\sigma(1)}$, the value of the $0$-form at the point $\sigma(1)\in\mathcal A$.

period

For a $k$-form $\omega$ and a $k$-chain $c=\sum_\sigma m_\sigma\sigma$, $\langle\omega,c\rangle=\sum_\sigma m_\sigma\int_\sigma\omega\in\mathbb C$ (with $m_\sigma$ cast to $\mathbb C$; sum over the finite support).

IsSimplexIn

A $k$-simplex $\sigma$ "lies in $X$" iff $\sigma:\mathbb R^{k+1}\to\mathcal A$ is $C^\infty$ on all of $\mathbb R^{k+1}$ and $\sigma(t)\in\operatorname{pts}(X)$ for every $t$ in the standard simplex $\{t_i\ge0,\ \sum_i t_i=1\}\subset\mathbb R^{k+1}$. Constant and otherwise degenerate simplices are allowed; nothing is required of $\sigma$ off the standard simplex except smoothness.

IsChainIn

A $k$-chain $c$ "lies in $X$" iff every simplex in its (finite) support lies in $X$. The zero chain lies in every $X$.

IsRational

A class $c\in H^k(X)$ is "rational" iff for every $\omega\in Z^k(X)$ with $[\omega]=c$ and every $k$-chain $c'$ lying in $X$ that is a cycle, there exists $q\in\mathbb Q$ with $\langle\omega,c'\rangle=q$ (as a complex number). Universal over representatives and over cycles. Edge cases: for $k=0$ every chain is a cycle; the zero chain always qualifies with period $0$; if $\operatorname{pts}(X)=\varnothing$ the only chains in $X$ are the zero chain and every class is rational; if some period is a non-integrable Bochner integral it contributes $0$, which is rational.

IsHodgeClass

For $p\in\mathbb N$ and $c\in H^{2p}(X)$: $c$ is a "Hodge class" iff $c$ is rational (previous item, in degree $2p$) and $c$ has type $(p,p)$ in the sense of HasTypeClass (some representative $\omega\in Z^{2p}(X)$ of $c$ satisfies the HasType identity with $p=q$).

IsJFrame

For a real subspace $T\subseteq\mathcal A$, a point $P\in\mathcal A$, and an $m$-tuple $u=(u_0,\dots,u_{m-1})$ of vectors of $\mathcal A$, "$u$ is a $J$-frame for $(T,P)$" means: (i) every $u_i\in T$; (ii) $\langle u_i,u_j\rangle_{\mathbb R}=\delta_{ij}$ (real orthonormality); (iii) $\langle u_i,J_P(u_j)\rangle_{\mathbb R}=0$ for all $i,j$, including $i=j$. It is not required that $J_P(u_j)\in T$, that $\|J_P(u_j)\|=1$, or that the $J_P(u_j)$ be mutually orthogonal. For $m=0$ the condition holds vacuously.

frame

For a real subspace $T\subseteq\mathcal A$, a point $P$, and $d\in\mathbb N$, $\operatorname{frame}(T,P,d)$ is a $d$-tuple of vectors of $\mathcal A$ built as follows. Let $m=\lfloor d/2\rfloor$ and let $u=(u_0,\dots,u_{m-1})$ be an element chosen by Hilbert's $\varepsilon$-operator: if some $m$-tuple is a $J$-frame for $(T,P)$, $u$ is some such $J$-frame (an arbitrary but fixed one when several exist; no orientation or uniqueness is imposed); if no $J$-frame of length $m$ exists, $u$ is an arbitrary, unspecified $m$-tuple of vectors of $\mathcal A$ (the type is nonempty, so the operator returns something, with no properties). Then, for index $k\in\{0,\dots,d-1\}$, the $k$-th vector is $\operatorname{frame}(T,P,d)_k=\begin{cases}u_{\lfloor k/2\rfloor}&\text{if }\lfloor k/2\rfloor<m\text{ and }k\text{ even},\\ J_P\bigl(u_{\lfloor k/2\rfloor}\bigr)&\text{if }\lfloor k/2\rfloor<m\text{ and }k\text{ odd},\\ 0&\text{otherwise (only when $d$ is odd and $k=d-1$)}.\end{cases}$ So the order is $(u_0,\ J_Pu_0,\ u_1,\ J_Pu_1,\ \dots,\ u_{m-1},\ J_Pu_{m-1})$, followed by a single zero vector if $d$ is odd. For $d\in\{0,1\}$, $u$ is the empty tuple and the frame is empty (for $d=0$) or $(0)$ (for $d=1$). The frame depends only on $(T,P,d)$, but through a non-constructive choice; when used pointwise in $P$ below, $P\mapsto\operatorname{frame}(T_P(X),P,d)$ is an arbitrary selection with no measurability or continuity guaranteed.

volMeasure

For $N,d\in\mathbb N$, $\mu_d$ is the measure on $\mathcal A$ (with its Frobenius/Euclidean metric)

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

where $d/2$ is natural-number (floor) division, $c_d$ is cast to $[0,\infty]$, and $\mathcal H^d$ is Mathlib's $d$-dimensional Hausdorff measure (with $d$ cast to $\mathbb R$), which is the un-normalized one: $\mathcal H^d(S)=\lim_{\delta\to0}\inf\{\sum_i(\operatorname{diam}U_i)^d:\ S\subseteq\bigcup U_i,\ \operatorname{diam}U_i\le\delta\}$. The classical normalization that makes Hausdorff measure agree with $d$-dimensional Lebesgue/Riemannian volume on $d$-dimensional Euclidean subspaces and $C^1$ submanifolds is $\omega_d/2^d$ with $\omega_d=\pi^{d/2}/\Gamma(d/2+1)$ the unit-ball volume. For even $d=2m$, $\omega_{2m}/2^{2m}=\pi^m/(m!\,2^{2m})=c_{2m}$, so $\mu_{2m}$ is exactly the classical $2m$-dimensional volume. For odd $d$, $c_d\ne\omega_d/2^d$ (e.g. $d=1$: $c_1=\tfrac12$ while $\omega_1/2=1$, so $\mu_1$ is half of arc length). For $d=0$, $c_0=1$ and $\mathcal H^0$ is counting measure.

wedgeVal

For a $k$-form $\omega$, an $l$-form $\eta$, a point $P$, and an arbitrary $(k+l)$-tuple $f=(f_0,\dots,f_{k+l-1})$ of vectors of $\mathcal A$,

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

the sum running over all permutations of $\{0,\dots,k+l-1\}$, with the first $k$ slots (indices $0,\dots,k-1$) fed to $\omega$ and the last $l$ slots (indices $k,\dots,k+l-1$) fed to $\eta$. The factor $1/(k!\,l!)$ is the inverse in $\mathbb C$ of the nonzero natural number $k!\,l!$. This is the standard wedge normalization under which $dx^1\wedge dx^2$ evaluates to $1$ on $(e_1,e_2)$. Only the scalar value is defined here, not a form; $f$ is not required to be linearly independent.

pairing

For a $k$-form $\omega$ and an $l$-form $\eta$,

$$\langle\omega,\eta\rangle_X=\int_{P\in\operatorname{pts}(X)}(\omega\wedge\eta)_P\bigl(\operatorname{frame}(T_P(X),P,k+l)\bigr)\ d\mu_{k+l}(P),$$

a Bochner integral of the complex-valued function of $P$ over the set $\operatorname{pts}(X)\subseteq\mathcal A$ with respect to $\mu_{k+l}=c_{k+l}\mathcal H^{k+l}$ restricted to $\operatorname{pts}(X)$. At each $P$ the $(k+l)$-tuple is the $\varepsilon$-chosen frame $(u_0,J_Pu_0,\dots)$ for the real tangent subspace $T_P(X)$ described under frame (arbitrary if no $J$-frame of length $\lfloor(k+l)/2\rfloor$ exists in $T_P(X)$; last entry $0$ if $k+l$ is odd, making the integrand $0$). Junk values: if the integrand is not Bochner integrable — in particular if it is not almost-everywhere strongly measurable, which the pointwise $\varepsilon$-choice does not guarantee, or if $\mathcal H^{k+l}(\operatorname{pts}(X))=\infty$ and the integrand fails to be integrable — the integral is $0$. If $\mathcal H^{k+l}(\operatorname{pts}(X))=0$ the integral is $0$. The value depends on which $J$-frame the choice operator selects (e.g. its sign under reordering).

integralOver

For an $l$-form $\eta$,

$$\int_X\eta=\int_{P\in\operatorname{regPts}(X)}\eta_P\bigl(\operatorname{frame}(T_P(X),P,l)\bigr)\ d\mu_l(P),$$

a Bochner integral over $\operatorname{regPts}(X)$ (the projectors of cone points with minimal Zariski tangent dimension) with respect to $c_l\mathcal H^l$, with the same frame construction and the same junk conventions as in pairing (non-integrable or non-measurable integrand gives $0$; $l$ odd makes the last frame vector $0$ and the integrand $0$). For $l=0$: the frame is empty, $\mu_0$ is counting measure, and $\int_X\eta=\sum_{P\in\operatorname{regPts}(X)}\eta_P$ if that sum is summable (and $0$ otherwise).

IsCycleClass

Given a second projective variety $Z$ in the same ambient $\mathbb{C}^{N+1}$, naturals $n,p$, and a class $c\in H^{2p}(X)$: "$c$ is the cycle class of $Z$ (with parameters $n,p$)" means: for every $\omega\in Z^{2p}(X)$ with $[\omega]=c$, and for every $(2n\dot-2p)$-form $\eta$ on $\mathcal A$ that is closed relative to $X$ (i.e. $\eta$ is $C^\infty$ on $\mathcal A$ and $d\eta$ vanishes on tangent tuples of $X$ at points of $\operatorname{pts}(X)$),

$$\langle\omega,\eta\rangle_X=\int_Z\eta,$$

where the left side is the pairing over $\operatorname{pts}(X)$ of the $(2p+(2n\dot-2p))$-form $\omega\wedge\eta$ against $\mu_{2p+(2n\dot-2p)}$, and the right side is the integralOver of $\eta$ over $\operatorname{regPts}(Z)$ using $Z$'s tangent spaces $T_P(Z)$ and $\mu_{2n\dot-2p}$. The degree $2n\dot-2p$ uses truncated subtraction: if $p>n$ it is $0$, $\eta$ is a smooth $0$-form with $d\eta$ vanishing along $X$, the pairing is of a $2p$-form, and the right side is the counting sum $\sum_{P\in\operatorname{regPts}(Z)}\eta_P$. No hypotheses relate $n$ to $\dim X$, $p$ to $\dim Z$ or to $n-\dim Z$, $Z$ to $X$ (no inclusion $Z\subseteq X$ is required), or require $X$, $Z$ to be nonsingular or irreducible; the closedness of $\eta$ is relative to $X$, not $Z$. If $\operatorname{pts}(X)=\varnothing$ then $H^{2p}(X)$ still exists (all smooth forms are closed and exact), the left side is $0$, and the condition becomes "$\int_Z\eta=0$ for all smooth $\eta$ of the given degree". The condition is universal over representatives $\omega$ of $c$.