The \(n\)-step valuation vector (paper (1.8)) \(\vec a^{(n)}(N)_i = v_2\bigl(3\, \mathrm{syr}^{[i]}(N)+1\bigr)\), the integerified offset (design D2) \(\texttt{fnat}\, n\, a = \sum _{m{\lt}n} 3^{\, n-1-m}\, 2^{\, a_{[1,m]}}\), and the load-bearing iteration identity, the paper’s (1.7) multiplied through by \(2^{|a|}\) so it holds in \(\mathbb {N}\): for odd \(N\), with \(a=\vec a^{(n)}(N)\),

(By induction on \(n\); the step is \(2^{a_{n+1}}\mathrm{syr}(\mathrm{syr}^{[n]}N) = 3\, \mathrm{syr}^{[n]}N + 1\).) Together with Lemma 2.1: the valuation vector is the unique tuple with all entries \(\ge 1\) making the affine quotient odd. COMPLETE (judge pass 21, 2026-07-13). valVec_unique (Lemma 2.1 as a hypothesis-guarded iff: divisibility \(\wedge \) odd quotient \(\leftrightarrow \) \(a = \texttt{valVec}\), for tuples with entries \(\ge 1\)) was proved by an external Codex session and judge-verified: statement RATIFIED vs Lemma 2.1 p.14 (RATIFY-2 resolved — the iff matches the paper’s uniqueness claim; the paper’s membership half, \(\vec a^{(n)} \in (\mathbb {N}+1)^n\) itself, is an unformalized one-line companion, consumer-safe since candidate tuples carry the hypothesis by construction); proof route is the paper’s own last-entry induction; dated judge runs 2026-07-13 on syr_iterate_key, valVec_unique, syr_iterate_odd all exactly \([\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}]\).