Correctness of finite rational tensor verification

Each input polynomial has finite support. Addition enumerates and combines a finite set of coefficient terms, multiplication enumerates the finite Cartesian product of the two supports, and monomial differentiation applies the natural-power rule [F6] to each variable factor, returning one term or zero. By [F2] these operations are operations in the integral domain $P$, and by [F1] every operation in the procedure is one of these finite polynomial operations or a finite rational combination of them.

A pair $(p,d)$ with $d\mathrm{\ne }0$ represents $p\mathrm{/}d$ in $K$. By [F3], equality of $(p,d)$ and $(u,v)$ is exactly $pv=ud$. Since $P$ is an integral domain, $p\mathrm{/}d=0$ holds exactly when $p=0$. Thus each cross-product operation represents the corresponding sum, product, quotient or derivative from [F4], and the numerator-zero flag is exact; it is not a numerical tolerance.

The cofactor identity $g\mathrm{adj}(g)=(\det g)I$ follows entrywise from the signed permutation expansion: diagonal entries are the Laplace expansion of $\det g$, while each off-diagonal entry is the same expansion with two equal rows and is zero by pairwise cancellation of permutations. Division by $\det g\mathrm{\ne }0$ in [A1] therefore returns the inverse matrix, and the sixteen inverse residuals are exactly zero.

The formula for $F$ differentiates the input covector and forms the coordinate exterior derivative. The Christoffel schedule is symmetric in its lower indices, hence torsion-free. Substituting the schedule and using $g_{im}{g}^{ml}={\delta }_i^l$ gives $g_{im}{\mathrm{\Gamma }}^m{}_{kj}+g_{jm}{\mathrm{\Gamma }}^m{}_{ki}=\frac{1}{2}({\mathrm{\partial }}_k{g}_{ij}+{\mathrm{\partial }}_j{g}_{ik}-{\mathrm{\partial }}_i{g}_{kj})+\frac{1}{2}({\mathrm{\partial }}_k{g}_{ji}+{\mathrm{\partial }}_i{g}_{jk}-{\mathrm{\partial }}_j{g}_{ki})={\mathrm{\partial }}_k{g}_{ij}\mathrm{.}$ so the connection is metric-compatible. If two such connections differ by $C^a{}_{bc}$, lower the first index with $g$; torsion-freeness makes $C_{abc}=C_{acb}$, and metric compatibility gives $C_{jki}+C_{ikj}=0$. Symmetry in the last two slots turns this into $C_{abc}=-C_{bac}$. These relations imply $C_{abc}=C_{acb}=-C_{cab}=-C_{cba}=C_{bca}=C_{bac}=-C_{abc}$, so the computed connection is unique. Expanding $R({\mathrm{\partial }}_c,{\mathrm{\partial }}_d){\mathrm{\partial }}_b$ by [F5] gives $R^a{}_{bcd}={\mathrm{\partial }}_c{\mathrm{\Gamma }}^a{}_{db}-{\mathrm{\partial }}_d{\mathrm{\Gamma }}^a{}_{cb}+{\mathrm{\Gamma }}^a{}_{ce}{\mathrm{\Gamma }}^e{}_{db}-{\mathrm{\Gamma }}^a{}_{de}{\mathrm{\Gamma }}^e{}_{cb}$; its trace $R^k{}_{ikj}$ is the algorithm's Ricci schedule, using lower-index symmetry of $\mathrm{\Gamma }$. All contractions use the same inverse. By induction over the procedure's finite ordered instruction list, every stored rational pair equals its corresponding coordinate expression.

On the real chart, [A1] makes each rational denominator and each recorded divisor nonzero, so the fraction operations equal ordinary smooth-function operations there. The monomial rule [F6] and quotient rule in [F4] therefore give the chart derivative. Since the polynomial numerator is identically zero exactly when its element of $P$ is zero by [F2]-[F3], a true flag certifies the exact coordinate identity throughout the whole admissible chart, not merely at sampled points. The converse for a chart with fixed parameter values is not asserted: specialization can make a nonzero element of $P$ vanish. Lorentz signature and the volume equation remain separate input hypotheses in [A1].