ch:graded-modal-dtt: graded substitution vectors

Problem and invariant. Keep subject, subject-type, and triangular declaration dependencies separate. At one-based position $i$, the row has length $i-1$, and substitution retains both the discarded row entry and the choose-and-scale term.

Two representations. A dependent triangle can enforce row lengths statically. The companion uses a recursive row list whose entries are recursive grade lists, then computes the entire $0,1,2,\dots$ length schedule; one record carries both two-component judgment vectors.

First complete version. Implement componentwise addition and scaling, generic position-indexed discard and column choice, triangular substitution, and structural row-length checking. Check modal-first, substitute-twice, vector separation, bad rows, and the nonzero equation $3+2\cdot 4=11$.

Observable result. The run prints eight named PASS lines and ends All 8 Chapter 100 corpus cases passed.

A failing version. First stop incrementing the expected row length. Then, in a separate replay, drop the retained row summand from triangular substitution. Each mutant checks and fails its corresponding shape or $11$-equation oracle. In a third replay, store the subject vector in both judgment fields; the named subject-versus-subject-type separation oracle fails.

Acceptance test. Run all four commands in subappendix E.8; require exact stdout and []. Restore the summand and rerun all commands.

Mathematical boundary. The corpus contains no GrTT terms, universes, typing rules, or saturated-set semantics, so it proves neither preservation, normalization, nor erasure.