Let V be the finitely supported sequences over a field F: the free F-module with basis e₀, e₁, e₂, … The forward shift Sₖ sends eₙ to eₙ₊ₖ. The backward shift Bₖ sends eₙ₊ₖ to eₙ and kills the first k basis vectors.
Sₖ is injective and misses exactly k dimensions. Bₖ is surjective and kills exactly k. And bshift_comp_shift records Bₖ ∘ Sₖ = id — each is a one-sided inverse of the other, on the side that fails.
These are computed, not stipulated. ker_shift shows the kernel is ⊥; ker_trunc identifies the range of Sₖ with the kernel of truncation, which gives an explicit isomorphism from the cokernel onto Fin k →₀ F, whose finrank is k. The same argument on the other side gives the kernel of Bₖ.
Closing that gap is chapter 3's job, and it is a real piece of work rather than a formality: it needs the Hardy space, the Toeplitz operator as a compression of multiplication, and the homotopy invariance of the index.
WP-82 ordered the rungs by field and found the corpus citing rung 33 thirty-one times and rung 28 twice — K-theory and index theory being the one it leaned on least and grounded least. Rung 28 was named the volume with no core.
The file was committed first to book11/, on a placement map that called Volume XI “the algebraic floor”, then to book33/, on the reading that the floor ladder's top rung was 33. Two documents were numbering the same word differently. The rule now is that the rung number is the volume number: index theory is XXVIII, and book33 is reserved for noncommutative geometry. tools/ladder_check.py is what stops the next such move being silent.
sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.