For a fixed finite operator family \((O_i)\), start from \(W_0={\operatorname{span}} S\) and iterate
This is an ascending chain. When two consecutive subspaces agree, every generator maps the stable subspace into itself. The stable value is therefore the entire hull of operator words, not just the span of the words tested so far.
Reading the drawing
The horizontal axis is iteration and the vertical axis is subspace dimension. The dashed curve permits only N; the solid curve also permits both chain projectors. Repeated plateau values indicate the checked stopping condition.
Drawing labels and data 17 labels
Read the original labels as selectable text. Tables preserve grid relationships; other short labels are grouped compactly.
- 0
- 1
- 2
- 3
- 4
- 5
- 6
- 0
- 1
- 2
- 3
- 4
- 5
- with \(P_e,P_f\)
- \(N\) only
- iteration \(n\)
- \(\dim W_n\)
Evidence note from the source edition
Exact dimensions for the same mixed seed in Model A. The dashed curve allows only \(N\). The solid curve also admits the two chain projectors. Plateau values are repeated to show the certified stop.
Why the process stops in finite dimensions
If an inclusion is strict, the dimension rises by at least one. It cannot rise beyond \(\dim X\). At equality, invariance and containment of the seeds prove both inclusions between the stable space and the least invariant hull.
What the companion code actually does
The new checker retains exact column bases using rational row reduction. It then verifies that adjoining the images of those bases under every generator does not increase rank. These examples use neither a cutoff on singular values nor a numerical tolerance.
The Lean statement is a mathematical termination and correctness specification. It is not a claim that this Python implementation for maintaining a basis was extracted from Lean or that a particular runtime bound was proved. The original numerical companion and its tolerances remain separate.
Read this as
“No new directions” is a stopping certificate only after checking the full declared operator family. Stopping after a convenient selection of words is not the same test.