Finite exact rational electrovac tensor verification

Inputs. Fix the integral domain $P=\mathbb{Q}[r,y,M,a,q]$ on the ordered variables $(r,y,M,a,q)$ and its field of fractions $K=\mathrm{Frac}(P)$. A run receives a symmetric $4\times 4$ matrix $g=(g_{ij})$ and a covector $A=(A_i)$ with entries in $K$, represented by finite sparse polynomial numerator-denominator pairs, together with a specified polynomial $w\in P$. It also receives the chart hypothesis that $\det g$ is nonzero in $K$ and that on the real open chart under consideration all input denominators are nonzero and $w=\sqrt{\mathrm{\mid }\det g\mathrm{\mid }}>0$. The coordinate derivations are ${\delta }_0={\delta }_3=0$, ${\delta }_1={\mathrm{\partial }}_r$, and ${\delta }_2={\mathrm{\partial }}_y$. The chart hypothesis is input; the procedure does not prove Lorentz signature or check the volume identity. For geometric interpretation use the curvature convention $R(X,Y)Z={\mathrm{\nabla }}_X{\mathrm{\nabla }}_{Y}Z-{\mathrm{\nabla }}_Y{\mathrm{\nabla }}_{X}Z-{\mathrm{\nabla }}_{[X,Y]}Z$, with $R^a{}_{bcd}$ the coefficient of $R({\mathrm{\partial }}_c,{\mathrm{\partial }}_d){\mathrm{\partial }}_b$ and ${\mathrm{Ric}}_{bd}:=R^a{}_{bad}$. Expanding this definition yields the coordinate Ricci schedule in Instruction 3.

Outputs. Return the finite tables of: the sixteen entries of $g{g}^{-1}-I$; the six independent components of $F_{ij}:={\delta }_i{A}_j-{\delta }_j{A}_i$; all sixteen raised components $F^{ij}$; the four Maxwell-density residuals ${\sum }_i{\delta }_i(w{F}^{ij})$; all sixty-four Christoffel entries; the sixteen Ricci entries ${\mathrm{Ric}}_{ij}={\sum }_k({\delta }_k{\mathrm{\Gamma }}^k{}_{ij}-{\delta }_j{\mathrm{\Gamma }}^k{}_{ik})+{\sum }_{k,l}({\mathrm{\Gamma }}^k{}_{kl}{\mathrm{\Gamma }}^l{}_{ij}-{\mathrm{\Gamma }}^k{}_{jl}{\mathrm{\Gamma }}^l{}_{ik});$ the scalar $F_{ij}{F}^{ij}$; the sixteen entries of ${\mathrm{Ric}}_{ij}-2(F_{ik}{F}_j{}^k-\frac{1}{4}{g}_{ij}{F}_{kl}{F}^{kl});$ the scalar curvature and the Ricci-square. For every output rational function, return its numerator-denominator pair, its exact numerator-zero flag, and the finite list of all divisor polynomials used.

Instructions.

1. Represent a polynomial by its finite set of exponent-vector/coefficient pairs. Addition merges equal exponent vectors, multiplication enumerates every pair of input monomials and collects equal exponent vectors, and ${\mathrm{\partial }}_r,{\mathrm{\partial }}_y$ differentiate each monomial by the integer-power rule of For a natural $n\ge 1$ the function $x\mapsto x^n$ is differentiable everywhere with derivative $\iota (n)x^{n-1}$; for $n=0$ it is the constant $1$, with derivative $0$; for a natural $n\ge 1$ the function $x\mapsto x^{-n}$ is differentiable at every $x\mathrm{\ne }0$ with derivative $-\iota (n)x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term. Represent a rational function by $(p,d)$ with $p,d\in P$ and $d\mathrm{\ne }0$. Addition and multiplication use cross-products, and division replaces $(p,d)\mathrm{/}(u,v)$ by $(pv,du)$ only when $u\mathrm{\ne }0$ in $P$. Differentiation uses $(p^{\mathrm{\prime }}d-p{d}^{\mathrm{\prime }},d^2)$.

2. Compute $\det g$ by its twenty-four signed permutation products and form $g^{-1}$ from cofactors divided by $\det g$. Record and check all sixteen entries of $g{g}^{-1}-I$.

3. All indices in this instruction range over $\{0,1,2,3\}$, and $g^{ij}:=(g^{-1}{)}_{ij}$. Compute every $F_{ij}$, then raise indices by $F_j{}^k:={\sum }_l{g}^{kl}{F}_{jl}$ and $F^{ij}:={\sum }_{k,l}{g}^{ik}{g}^{jl}{F}_{kl}$. Compute all four ${\sum }_i{\delta }_i(w{F}^{ij})$. Compute every Christoffel entry by ${\mathrm{\Gamma }}^i{}_{jk}=\frac{1}{2}{\sum }_l{g}^{il}({\delta }_j{g}_{lk}+{\delta }_k{g}_{jl}-{\delta }_l{g}_{jk})$, then all sixteen Ricci entries by the displayed formula, with no symmetry-based component omitted. Compute $F_{ij}{F}^{ij}$, every Einstein residual, $g^{ij}{\mathrm{Ric}}_{ij}$ and $g^{ik}{g}^{jl}{\mathrm{Ric}}_{ij}{\mathrm{Ric}}_{kl}$ by their full finite contractions.

4. Record every polynomial divisor introduced by inversion, division, or a rational derivative in the admissibility list. Do not remove a divisor from that list when a later cancellation removes its factor from the displayed numerator or denominator. Return failure if any required divisor is the zero polynomial or an input denominator is zero.

A zero flag means exactly that the polynomial numerator is the zero element of $P$. No floating-point tolerance, parameter sample, convergence test, or choice of roots is part of the procedure. This is a finite mathematical procedure; its operational correctness, termination, and resource bounds are separate proved claims.