ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-11

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.

The rank and solution behaviour of a parameterised matrix change at one exceptional parameter

Example

For $A_{t} = (\begin{array}{cc} 1 & 1 \\ 1 & t \end{array}), b = (\begin{array}{c} 2 \\ 2 \end{array}),$ the real system $A_{t} x = b$ has rank $2$ and the unique solution $(2, 0)$ when $t \neq 1$ , while at $t = 1$ it has rank $1$ and the affine line of solutions $(2 - s, s)$ .

Facts & Assumptions

Given: A real parameter $t$ and the displayed system.

[L1]

Matrix rank is the number of pivots (Row rank equals column rank, and both equal the number of pivots).

[L2]

RREF gives consistency and the free-variable parametrisation (Reduced row echelon form detects consistency and parametrises every solution by the nonpivot variables).

[L3]

The real numbers form a field (The reals form a field).

Verification

technique · cases

1.1

Subtract row $0$ from row $1$ without dividing by the parameter; the augmented matrix becomes $(\begin{array}{ccc} 1 & 1 & 2 \\ 0 & t - 1 & 0 \end{array})$ .

L1L2L3cases

2.1

If $t \neq 1$ , the second row has a pivot, so the rank is $2$ , $y = 0$ , and $x = 2$ .

step 1.1assume-case generic

2.2

If $t = 1$ , the second row is zero, so the rank is $1$ and $y = s$ is free with $x = 2 - s$ .

step 1.1assume-case exceptional

3.1

The alternatives $t = 1$ and $t \neq 1$ are exhaustive and give the stated solution behaviour.

step 2.1step 2.2cases-exhaustive∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

J. Hefferon, Linear Algebra, 4th ed., Ch. One, exercises after §III.2 (standard reference, not scraped)