ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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 worked QR factorisation of an invertible real matrix

Example

The invertible matrix

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

has the QR factorisation

$A = Q R, Q = \frac{1}{\sqrt{2}} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array}), R = (\begin{array}{cc} \sqrt{2} & 1 / \sqrt{2} \\ 0 & 1 / \sqrt{2} \end{array}) .$

Facts & Assumptions

Given: The displayed real matrix $A$ .

[L1]

QR factorisation applies Gram–Schmidt to the columns and requires an upper-triangular factor with positive diagonal (Every invertible real or complex square matrix has a unique factorisation $A = Q R$ with $Q$ orthogonal or unitary and $R$ upper triangular with positive real diagonal).

[L2]

The standard real inner product is the dot product (The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products).

[L3]

Gram–Schmidt preserves successive spans while normalising orthogonal residuals (Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans).

Verification

technique · computation

1.1

The columns are $a_{0} = (1, 1)$ and $a_{1} = (1, 0)$ . By [L2]–[L3], $q_{0} = (1, 1) / \sqrt{2}$ , while $a_{1} - ⟨ a_{1}, q_{0} ⟩ q_{0} = (1 / 2, - 1 / 2)$ normalises to $q_{1} = (1, - 1) / \sqrt{2}$ .

L2L3algebra

2.1

The coefficients are $R_{00} = \sqrt{2}$ , $R_{01} = 1 / \sqrt{2}$ , and $R_{11} = 1 / \sqrt{2}$ , with $R_{10} = 0$ . Thus $R$ is upper triangular with positive diagonal.

step 1.1L1

3.1

Direct multiplication gives $Q R = A$ , and $Q^{T} Q = I$ . This verifies the displayed QR factorisation.

step 1.1step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 54 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.