ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

A singular matrix has a polar decomposition with visibly nonunique isometric factors

Example

For

$T = (\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array}),$

one has the polar factor $U = (\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array})$ and two distinct orthogonal choices

$S_{1} = (\begin{array}{cc} 1 & 0 \\ 0 & 1 \end{array}), S_{2} = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array}),$

with

$T = S_{1} U = S_{2} U .$

Facts & Assumptions

Given: The singular matrix $T$ above on $R^{2}$ with the standard inner product.

[L1]

The polar decomposition exists, and uniqueness of the isometric factor fails in general when the operator is singular (Every endomorphism has a polar decomposition T = SU with U non-negative and S an isometry on the orthogonal complement of ker T, and S is unique exactly when T is invertible).

Verification

technique · direct

1.1

Because $T^{*} T = T$ , the non-negative square root is $U = T$ . Also $S_{1}$ and $S_{2}$ are both orthogonal because $S_{1}^{T} S_{1} = S_{2}^{T} S_{2} = I$ .

L1algebra

2.1

Direct multiplication gives $S_{1} U = U = S_{2} U = T$ , while $S_{1} \neq S_{2}$ . Hence this singular operator has more than one polar isometric factor, exactly as [L1] allows.

L1step 1.1algebra∎

Depends on

Used by

FALSE: The isometry in the polar decomposition is unique even for singular operators False statement

Dependency tree · two levels

9 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

Sheldon Axler, Linear Algebra Done Right, fourth edition (standard reference, not scraped)