ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Square root and absolute value of a matrix

Example

Assume AC. On the two-dimensional complex inner-product space with orthonormal basis $(e_{1}, e_{2})$ let $T = (\begin{array}{cc} 0 & 2 \\ 0 & 0 \end{array})$ , so that $T e_{1} = 0$ and $T e_{2} = 2 e_{1}$ . Then $∣ T ∣ = diag (0, 2)$ ; in particular the positive square root of $diag (1, 4)$ is $diag (1, 2)$ .

Facts & Assumptions

[A1]

For a bounded operator on a nonzero complex Hilbert space, $T^{*}$ is characterised by $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ (The Hilbert-space adjoint of a bounded operator).

[A2]

$∣ T ∣ = (T^{*} T)^{1 / 2}$ , this square root is positive, $∣ T ∣^{2} = T^{*} T$ and $\ker ∣ T ∣ = \ker T$ (Absolute value of a bounded operator).

[A3]

Every bounded positive operator has a unique bounded positive square root, and positivity of a self-adjoint operator is the quadratic-form condition $⟨ C x, x ⟩ \geq 0$ for every $x$ (Positive square root, Order on bounded self adjoint operators, Self-adjoint, positive, unitary and normal operators).

[A4]

AC is the hypothesis of the square-root supplier (The Axiom of Choice).

Verification

technique · direct

Given: The setting of the example, with diagonal operators written in the orthonormal basis and $diag (a, b) e_{1} = a e_{1}$ , $diag (a, b) e_{2} = b e_{2}$ .

1.1

$T^{*} = (\begin{array}{cc} 0 & 0 \\ 2 & 0 \end{array})$ and $T^{*} T = diag (0, 4)$ : indeed $⟨ T e_{1}, e_{1} ⟩ = ⟨ T e_{1}, e_{2} ⟩ = 0$ , $⟨ T e_{2}, e_{1} ⟩ = 2$ , $⟨ T e_{2}, e_{2} ⟩ = 0$ , so the adjoint has the displayed matrix and the product is diagonal with entries $∥ T e_{1} ∥^{2} = 0$ and $∥ T e_{2} ∥^{2} = 4$ .

1.2

$diag (0, 4)$ is self-adjoint and positive, as is $diag (0, 2)$ : for $x = x_{1} e_{1} + x_{2} e_{2}$ one has $⟨ diag (0, 4) x, x ⟩ = 4 ∣ x_{2} ∣^{2} \geq 0$ and $⟨ diag (0, 2) x, x ⟩ = 2 ∣ x_{2} ∣^{2} \geq 0$ .

A1A3

2.1

$diag (0, 2)^{2} = diag (0, 4) = T^{*} T$ , so by uniqueness of the positive square root $∣ T ∣ = (T^{*} T)^{1 / 2} = diag (0, 2)$ .

step 1.1step 1.2A2A3

2.2

Likewise $diag (1, 4)$ is positive with positive square root $diag (1, 2)$ , since $diag (1, 2)^{2} = diag (1, 4)$ and $⟨ diag (1, 2) x, x ⟩ = ∣ x_{1} ∣^{2} + 2 ∣ x_{2} ∣^{2} \geq 0$ , uniqueness again identifying the square root.

step 1.2A3

3.1

Hence $∣ T ∣ = diag (0, 2)$ as claimed, and the positive square root of $diag (1, 4)$ is $diag (1, 2)$ .

step 2.1step 2.2A4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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

John B. Conway, A Course in Functional Analysis, 2nd ed., Chapter IX §3, printed pp.239–243 (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis, §5.3, printed pp.235–245 (standard reference, not scraped)