When is passing from real algebraic geometry to the complexification genuinely unavoidable?

Many results in real algebraic geometry are proved by passing from a real variety to its complexification , then studying the action of complex conjugation on . For example, one often regards

$X(\mathbb R)$

as the fixed-point locus of conjugation on

$X(\mathbb C)$.

This appears in results such as Harnack-type inequalities, Smith–Thom inequalities, Rokhlin’s complex orientation formula, and the topology of real algebraic curves and surfaces.

My question is about the extent to which this passage to the complex picture is merely a powerful technique, as opposed to something genuinely unavoidable.

More precisely:

Are there theorems in real algebraic geometry whose standard proofs essentially require complex algebraic geometry, complex topology, Hodge theory, or complexification? And is there any precise sense in which one can say that a theorem about “cannot be proved purely over ”?

I realize that “cannot be proved purely over ” is not automatically a well-defined mathematical statement, since a proof can often be rewritten in different languages. So I would also be interested in answers explaining whether there is a formal framework in which this question makes sense.

For instance, I would like to understand examples such as:

1. Harnack’s inequality for real plane curves;

2. the Smith–Thom inequality comparing and ;

3. Rokhlin’s complex orientation formula;

4. restrictions on real algebraic surfaces coming from the topology or Hodge theory of the complexification;

5. classifications of real curves or real K3 surfaces that use the complex period or lattice picture.

Are these examples best viewed as genuinely complex-geometric theorems with real consequences, or are there known purely real proofs of them?