ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Complexifying a real polynomial space gives the same degree bound with complex coefficients

Example

Let $R [x]_{\leq d}$ be the real vector space of real polynomials of degree at most $d$ and $C [x]_{\leq d}$ the complex vector space of complex polynomials of degree at most $d$ , for a fixed $d \geq 0$ . Then

$C \otimes_{R} R [x]_{\leq d} ≅ C [x]_{\leq d}, z \otimes p ⟼ z p,$

and the canonical embedding $ι p = 1 \otimes p$ becomes the inclusion $R [x]_{\leq d} \subseteq C [x]_{\leq d}$ . Complexification does not raise the degree bound; it only replaces real coefficients by complex ones.

Facts & Assumptions

Given: The real vector space $V = R [x]_{\leq d}$ and the complex vector space $W = C [x]_{\leq d}$ .

[L1]

The complexification $V_{C} = C \otimes_{R} V$ carries the scalar action $z \cdot (w \otimes v) = (z w) \otimes v$ and the real-linear embedding $ι v = 1 \otimes v$ (Complexification as $C \otimes_{R} V$ with its canonical real-linear embedding).

[L2]

The map $Φ : C \otimes_{R} V \to V \oplus i V$ , $Φ (z \otimes v) = z (v, 0)$ , is a complex-linear isomorphism with inverse $Ψ (v + i w) = 1 \otimes v + i \otimes w$ (The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic).

[L3]

A real-linear map $f : V \to W$ into a complex vector space extends to a unique complex-linear map $F : V_{C} \to W$ with $F (z \otimes v) = z f (v)$ (Complexification is initial for real-linear maps into complex vector spaces, and is unique up to unique isomorphism).

Verification

technique · direct

1.1given

The monomials $1, x, \dots, x^{d}$ form a real basis of $R [x]_{\leq d}$ and a complex basis of $C [x]_{\leq d}$ .

1.2L1L3

The real-linear inclusion $f : R [x]_{\leq d} ↪ C [x]_{\leq d}$ extends by [L3] to a unique complex-linear map $F$ with $F (z \otimes p) = z p$ ; by the scalar action of [L1] this is the map $z \cdot (1 \otimes p) \mapsto z f (p)$ on the tensor model.

2.1L2step 1.1step 1.2

By [L2], every element of $C \otimes_{R} R [x]_{\leq d}$ is $1 \otimes p + i \otimes q$ with $p, q \in R [x]_{\leq d}$ , and $F$ sends it to $p + i q \in C [x]_{\leq d}$ ; the monomial images $F (1 \otimes x^{j}) = x^{j}$ are the complex basis of step 1.1, so $F$ is a complex-linear isomorphism.

3.1step 1.2step 2.1

Degree bound: $p + i q$ has degree at most $d$ because $p$ and $q$ do, so no degree bound is lost; the embedding $ι p = 1 \otimes p$ maps to $p$ itself, the inclusion of the real polynomials.

4.1step 2.1step 3.1∎

Steps 1.2 through 3.1 identify the complexification with $C [x]_{\leq d}$ and the canonical embedding with the inclusion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Keith Conrad, Complexification (notes) (standard reference, not scraped)