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.
Complex Subspace Realification — Examples
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Complex Norms and Realification
- Complex Subspace Realification
- Complexification, Realification and Real Structures
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The complex line in spanned by exhibits the finite basis conversion explicitly: its real basis is .
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
The complex line through (1,i) has a two-vector real basis
Example
Equip with coordinatewise operations and the norm . Let and with the restricted complex norm. Then is a real normed subspace of with the restricted norm metric, and the ordered real basis list is
Facts & Assumptions
Given: , , , and .
A complex norm is real-valued, separates zero, is homogeneous for every complex scalar, and satisfies the triangle inequality (Complex norm and complex normed space).
The complex coordinate sum norm, including the zero space proves that the coordinate sum of complex moduli is a complex norm on , including .
A complex normed linear subspace makes a complex-linear subspace carry the restricted complex norm.
A complex normed subspace and its finite basis realify states that such a subspace realifies to a real normed subspace with the identical restricted norm metric.
Realification of a complex vector space by restriction of scalars keeps the underlying set and addition and restricts scalar multiplication to the canonical real embedding.
is the real coordinate plane, with coordinate arithmetic gives unique coordinates and the complex coordinate arithmetic.
Linear subspace of a vector space tests a linear subspace by zero containment and closure under addition and scalar multiplication.
Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis defines a basis by linear independence and spanning, and an ordered basis as a finite injective list with basis image.
Linear independence: a finite list is independent when forces every , and a subset is independent when every injective finite list into is independent defines independence of a finite list by requiring every scalar relation equal to zero to have all coefficients zero.
Linear combination of a finite list, and the span as the smallest linear subspace containing defines a linear combination of elements of a set as a finite sum of scalar multiples of elements of that set.
is exactly the set of linear combinations of finite lists of elements of , and identifies the span with the set of finite linear combinations.
In a vector space, scalar multiplication distributes over vector and scalar addition and associates with scalar multiplication (Vector space over a field).
A finite linearly independent list is injective and has a linearly independent image (Finite sums re-indexed along an injection, with a zero term deleted, and concatenated; and the closure properties of linear independence: an independent list is injective and never , its sublists are independent, a list is independent exactly when it is injective with linearly independent image, and every subset of a linearly independent set is linearly independent).
On , addition and scalar multiplication are pointwise (The complex coordinate sum norm, including the zero space).
For any vector , scalar multiplication by zero gives (In any vector space , , , , and forces or ).
Verification
The coordinate sum norm on is a complex norm by [F2] and [F1]. The set contains zero because by [F15]. The vector-space laws [F12] give and , so is closed under addition and complex scalar multiplication; [F7] makes it a complex-linear subspace. The restricted norm inherits separation, full complex homogeneity, and the triangle inequality, so it gives the complex normed subspace in [F3].
If for , the pointwise coordinate operations of [F14] give first coordinate . Uniqueness of the real and imaginary coordinates in [F6] implies , so the list is linearly independent by [F9].
Applying [F4] to this complex normed subspace gives the real normed subspace and the identical restricted norm metric.
For , [F6] gives using coordinatewise scalar multiplication [F14] and the vector-space laws [F12]. Thus every element of is a real linear combination of the displayed list. Conversely, by taking and by taking ; since is a complex-linear subspace by step 1.1 and real scalars act through the canonical embedding [F5], every real linear combination of and belongs to . The two inclusions and [F10]–[F11] show that the list spans .
By steps 2.2 and 1.2 the list is spanning and linearly independent. By [F13] it is injective with linearly independent image, and step 2.2 says that image spans; hence [F8] makes it an ordered real basis.