TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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 stabilised power splits the space into its kernel and image

Statement

Let $T$ be an endomorphism of a finite-dimensional vector space $V$ . If $m \geq 0$ and $\ker T^{m} = \ker T^{m + 1}$ , then $V = \ker T^{m} \oplus im T^{m} .$

Facts & Assumptions

Given: An endomorphism $T$ of a finite-dimensional vector space $V$ and $m \geq 0$ with $\ker T^{m} = \ker T^{m + 1}$ .

[L1]

Once consecutive kernels agree at $m$ , every later kernel equals $\ker T^{m}$ (Kernel and rank sequences of powers stabilise once equality occurs).

[L2]

Rank-nullity gives $\dim V = \dim \ker S + \dim im S$ for an endomorphism $S$ (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[L3]

For two subspaces, $V = U \oplus W$ exactly when $V = U + W$ and $U \cap W = {0}$ (Internal direct sum $V = ⨁_{i < n} U_{i}$ : the sum is everything and each summand meets the sum of the others only in $0_{V}$ ).

Proof

technique · direct

1.1

If $x \in \ker T^{m} \cap im T^{m}$ , write $x = T^{m} y$ ; then $T^{2 m} y = 0$ , so [L1] gives $y \in \ker T^{m}$ and hence $x = 0$ .

L1algebra

2.1

By [L2] applied to $T^{m}$ , the dimensions of $\ker T^{m}$ and $im T^{m}$ sum to $\dim V$ ; with the zero intersection from step 1.1, their sum is therefore all of $V$ .

step 1.1L2algebra

3.1

Fact [L3] now gives the asserted internal direct sum, including $m = 0$ and $V = 0$ .

step 1.1step 2.1L3∎

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: 67 results over 20 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.

Sources

S. Axler, Linear Algebra Done Right, 4th ed., Result 8.4 (standard reference, not scraped)