Truncated Milnor computation terminates and matches peripheral quotients

Under [A1], the validation stage scans a finite diagram. The degree loop runs from $2$ to $d$, each component traversal visits finitely many undercrossings, and each multiplication, inverse, and truncation in $R_d$ involves only finitely many monomials of degree at most $d$. The output stage scans finitely many index sequences and their finitely many proper subsequences and cyclic permutations. Thus every loop is finite and the procedure terminates.

Use the algorithm's maximal Wirtinger arcs: all consecutive diagram edges through an overpass have one reference meridian and one series. The preliminary symbol substitution therefore preserves every compatible certificate word. At degree one every meridian on component $j$ is conjugate to its root meridian, so its expansion in root symbols is $1+X_j$. This is the initialization $Y_a^{(1)}$. If step 1 inserts a curl, the original underpass-free component had one cyclic arc and the new underpass cuts it into one interval arc. The supported isotopy transports its root, accesses, and all supplied words to that arc; every other arc is transported with the same symbol. Thus the post-curl certificates encode the same based data.

Induct on $\mathrm{\ell }$, starting from step 1.2. Choose free words for the preceding arc approximations, representing the true compatible meridians modulo ${\mathrm{\Gamma }}_{\mathrm{\ell }}G$. Start each component at its root word $x_j$, and follow its maximal arcs. At a nonclosing underpass, conjugate the current incoming word by the preceding over-word, with the sign prescribed by [F2]. Replacing the true over-meridian by a word congruent modulo ${\mathrm{\Gamma }}_{\mathrm{\ell }}G$ changes its conjugation of a meridian only modulo $[G,{\mathrm{\Gamma }}_{\mathrm{\ell }}G]={\mathrm{\Gamma }}_{\mathrm{\ell }+1}G$, by [F7]. Induction along the traversal therefore makes every new arc word a lift of its true meridian modulo ${\mathrm{\Gamma }}_{\mathrm{\ell }+1}G$. Its expansion through degree $\mathrm{\ell }$ uses the over-word only through degree $\mathrm{\ell }-1$: a discrepancy of degree $\mathrm{\ell }$ commutes with the constant term of the conjugated series and first contributes in degree $\mathrm{\ell }+1$. Thus its expansion is exactly the algorithm's update. The lower degrees agree with the preceding pass by the same argument one degree lower. This proves that the output arc series are expansions of explicit compatible lift words, correct in $G\mathrm{/}{\mathrm{\Gamma }}_{d+1}G$. In string-link mode [F4] identifies those lifts uniquely in $F_r\mathrm{/}{\mathrm{\Gamma }}_{d+1}{F}_r$; in closed-link mode only the selected lift words are asserted, without assigning a Magnus expansion to an arbitrary element of the closed-link group. No global string-link presentation is needed.

By [F3], the ordered over-meridian product is the based string-link longitude or the closed blackboard parallel. In closed-link mode, the initial-meridian power removes its self-writhe. Substituting the arc lift words of step 2.1 gives explicit longitude lift words in $G\mathrm{/}{\mathrm{\Gamma }}_{d+1}G$; multiplicativity makes ${\mathrm{\Lambda }}_j$ exactly their expansions through degree $d$. In string-link mode these are the unique bottom-end quotient classes by [F4].

In the arbitrary-choice branch, evaluating the finite transport words gives their actual compatible-coordinate expansions by step 2.1 and [F5]; when step 1 inserted a curl, these words have already been transported through the explicit old-to-new strand-symbol identification of step 1.2. The formulas of [F3] therefore give the actual selected longitude expansion before changing root variables. The actual root meridian is $g_j{x}_j{g}_j^{-1}$, so its series is $1+X_j+R_j$ with $R_j$ of degree at least two. Substitution of two letter systems agreeing through degree $s$ into $R_j$ gives results agreeing through degree $s+1$, since each monomial has at least two letters. Hence the displayed iteration improves the inverse equation by one degree at each pass, starting correctly at degree one. At pass $d$ it solves $Z_j+R_j(Z)=V_j$ exactly in the truncated ring. The same degree argument proves uniqueness, and consequently also the other composition identity. Thus it is the inverse formal change from compatible to actual meridian coordinates. This also agrees with the group-theoretic change on the finite nilpotent quotient: substitution by the conjugates has identity degree-one map and induces an isomorphism on each finite free nilpotent quotient: apply the arbitrary-basing branch of [F4] to the trivial string link, whose compatible endpoint group is $F_r$, with these exact independently conjugated meridians. Its Magnus series satisfies the same unique inverse equations. The corrected-and-substituted series is therefore exactly the longitude expansion in the chosen actual symbols, including independently based endpoints and all supplied relative winding. No full-group free-basis assertion or unrecorded access cancellation is used.

Under the stated axiom branch [A1], for $I=(i_1,\dots ,i_k,j)$ with $k\le d$, [F5] says the coefficient of $X_{i_1}\cdots X_{i_k}$ depends only on the longitude class in $F_r\mathrm{/}{\mathrm{\Gamma }}_{k+1}$ and is independent of the chosen representative. In string-link mode, [F4] identifies that class uniquely via the bottom-end isomorphism. In closed-link mode, [F4] supplies the required component-meridian lift; the procedure uses the based lift determined by its root arcs and traversal. Thus the coefficient read from ${\mathrm{\Lambda }}_j$ is exactly the based coefficient in [F6].

In closed-link mode, each lower coefficient used for ${\mathrm{\Delta }}_I^b$ is computed by the same procedure at its own finite degree; the finite gcd and quotient operation are exactly those in [F6]. Hence the returned indeterminacy and residue candidate are correct for the selected based word-lift data. The theorem asserts no independence of those choices; that is the separate basing theorem.