Termination and separate algebraic resource account for rational tensor verification

The determinant uses $4!=24$ signed permutation products, the inverse table has sixteen entries, the four Maxwell residuals have four coordinate terms each, and every Christoffel, Ricci and contraction table has a fixed finite index range in $\{0,1,2,3\}$. By [F1], all loops therefore make finitely many calls to arithmetic operations on finite-support polynomials.

A sparse sum combines at most $2R$ terms. A sparse product examines at most $R^2$ ordered monomial pairs; differentiating a support of size at most $R$ visits at most $R$ terms. Thus for each of the $K$ polynomial operations the stated upper bound $2R^2+2R$ dominates the coefficient work and insertion count. A sorted support list has at most $R$ entries, so each insertion makes at most $R$ comparisons. Summing over $K$ operations and retaining at most $R$ records for each of the $K$ intermediate results and $N_{\mathrm{i}\mathrm{n}}$ inputs gives the stated operation, insertion and memory bounds.

All integer and rational coefficient operations and all finite list traversals terminate; the schedule has no convergence or data-dependent loop. The finite operation schedule from step 1.1 therefore terminates. The bounds count algebraic operations and records only; they do not bound coefficient bit lengths or elapsed machine time.