Manuscript and scope
Anonymous author. Version 1.0, 21 October 2026. Full manuscript: paired-tensor-semantics.pdf. Source, LaTeX, build instructions and results: paired-tensor-publication-package-v1.0.zip. This is an extended synopsis.
We give a shape-indexed tensor language, architecture-relative completeness, compiler/numerical contracts and residual symmetries in a presheaf infinity-topos. The finite-graph interpreter is not proof-assistant certified and does not cover all existing framework operators.
The chain-rule foundation follows reverse derivative categories [1] and CHAD [2,3]; see [4] for a separate complexity formalization. Our contribution combines tensor/architecture contracts with observable implementation policies and a reference artifact.
1. Shapes and the meaning of an adjoint
For a finite shape $s=(d_1,\ldots,d_k)$ of positive dimensions, let $T_s=\mathbb R^{\prod_jd_j}$; the empty shape is scalar. Types are $1$, $T_s$, and finite products. The terminal type $1$ is the zero-dimensional vector space. Equip them with Euclidean pairings and retain the dual notation $A^*$ even when coordinates identify it with an equal-shaped array.
A smooth program is $f:U\subseteq A\to B$, with $U$ open and $f$ smooth. Define
$$ \operatorname{jvp}_f(a,v)=Df(a)v, \qquad \operatorname{pb}_f(a,u)=Df(a)^*u. $$
Then $\langle\operatorname{pb}_f(a,u),v\rangle=\langle u,\operatorname{jvp}_f(a,v)\rangle$. The adjoint belongs to the derivative at the input, not to the nonlinear map itself. Parameters and differentiable initial state are explicit input coordinates. First-order correctness also holds for $C^1$ maps; a full iterated reverse-differential structure uses the smooth class.
2. Finite tensor syntax and primitive contracts
A static single-assignment program is a finite list $z_i:=g_i(z_{a_{i1}},\ldots,z_{a_{ir}})$ with earlier-node references, typed input context and output projection/tuple. Its schemas are constants, equal-shape addition and elementwise multiplication, reshape, permutation, fixed gather, sum reduction, concatenation, rank-two matrix multiplication, and elementwise exp, tanh, reciprocal and inverse square root. Broadcasting is explicit. Reciprocal excludes zero; inverse square root requires positivity. Pulling back these open conditions defines the program's admissible open domain.
The finite schemas have arbitrary finite shapes, constants and index lists. No implicit cast or opaque operation is admitted.
For a linear structural map $L$, the reverse is $L^{\mathsf T}$. In particular:
$$ \Delta(x)=(x,x),\quad\operatorname{pb}_{\Delta}(x,(u,v))=u+v, \qquad\operatorname{pb}_{!}(x,0)=0. $$
If $G(x)_j=x_{i_j}$ at fixed indices, repeated indices give
$$ (G^{\mathsf T}u)_k=\sum_{j:i_j=k}u_j. $$
This follows by collecting coefficients in $\langle u,Gv\rangle$. Reshape and permutation reverse by their inverse coordinate arrangements; reduction/broadcast and concatenation/splitting are adjoint pairs.
The numerical primitive pullbacks, with saved primal data, are
$$ \begin{aligned} x+y&\rightsquigarrow(u,u),\\ x\odot y&\rightsquigarrow(u\odot y,u\odot x),\\ AB&\rightsquigarrow(uB^{\mathsf T},A^{\mathsf T}u),\\ \exp x=y&\rightsquigarrow u\odot y,\\ \tanh x=y&\rightsquigarrow u\odot(1-y^2),\\ x^{-1}=y&\rightsquigarrow -u\odot y^2,\\ x^{-1/2}=y&\rightsquigarrow-\tfrac12u\odot y^3. \end{aligned} $$
Scalar differentiation and $D(AB)[H,K]=HB+AK$ with the trace pairing prove these ideal-real rules.
3. Residual semantics and graph correctness
Definition. A mathematical tape contract for $f:U\subseteq A\to B$ is a nonempty finite-dimensional open residual space $R$, smooth maps
$$ F:U\to B\times R,\qquad K:R\times B^*\to A^*, $$
with $K(r,-)$ linear and a proof that
$$ F(a)=(f(a),r_a)\Longrightarrow K(r_a,u)=Df(a)^*u. \tag{1} $$
The terminal residual is allowed. Correctness concerns reachable residuals. A mathematical proof of a contract is not a machine-checked certificate in the implementation.
Theorem 1 (composition). Correct tape contracts compose by
$$ \begin{aligned} F_{gf}(a)&=(c,(r,s)),\quad (b,r)=F_f(a),\quad(c,s)=F_g(b),\\ K_{gf}((r,s),w)&=K_f(r,K_g(s,w)). \end{aligned} $$
Products compose componentwise. The associative and unit identifications are the canonical residual re-associations and terminal factors.
Proof. On reachable residuals, the reverse expression is $Df(a)^*Dg(f(a))^*w=D(g\circ f)(a)^*w$. Product derivatives are block diagonal. Nested evaluation is unchanged by residual re-association. Identity uses $K(*,u)=u$. $\square$
Theorem 2 (finite graph correctness). For every well-typed finite graph $p$ of correct smooth primitives, the tape transformation returns its forward denotation $f$ and a pullback $Df(a)^*u$; the directional transformation returns $Df(a)v$.
Proof. Each instruction extends the current context by $H_i(z)=(z,g_i(\pi_i z))$. Its reverse retains the old context cotangent and adds the primitive contributions into the selected coordinates. Repeated argument positions therefore contribute multiple summands to one coordinate. Induction over these context extensions, followed by the output projection, gives the result by Theorem 1 and the structural rules. The forward chain rule proves the directional statement. $\square$
Parameter tying accumulates into one coordinate. A pairing check alone is insufficient: incorrect maps can be adjoints of each other.
4. Architecture-relative completeness
Definition. Let $\mathcal A$ be the least typed grammar closed under composition, sharing, parallel products/concatenation, and:
1. Dense affine layers and activations generated by the smooth library. 2. Finite fixed-stencil convolutions with fixed stride, padding, dilation and groups; fixed sum/average pooling. 3. Equal-shape residual addition. 4. A fixed finite number $T$ of recurrent steps, with explicitly shared parameters and initial state. 5. Mean/variance normalization with fixed $\epsilon>0$, reduction axes and optional affine parameters. 6. Finite-head scaled dot-product attention with fixed finite sequence lengths and affine projections.
Structural masks specify nonempty allowed key sets and normalize over those sets; no infinite-valued real constants are required. All shapes and structural indices are fixed for a grammar instance.
Theorem 3 (constructive completeness). Every typed $N\in\mathcal A$ admits a finite typed lowering $L(N)$ with equal real denotation. Its tape transformation computes the correct pullback on its admissible domain, including gradients of shared parameters and differentiable initial state.
Proof. Dense maps use contraction and bias broadcast. Convolution gathers finite patches, adds fixed padding constants, reshapes weights and contracts. Stride, dilation and groups modify fixed index selections; pooling adds reduction. Residual and parallel constructions use addition and concatenation. Unfold recurrence $T$ times while retaining one input slot per shared parameter.
For a normalization slice of size $m$,
$$ \mu=m^{-1}\sum_jx_j,\quad c_j=x_j-\mu,\quad v=m^{-1}\sum_jc_j^2,\quad y_j=c_j(v+\epsilon)^{-1/2}. $$
Here $v+\epsilon>0$. Attention uses
$$ S=d^{-1/2}QK^{\mathsf T},\quad P_{ij}=\frac{e^{S_{ij}}}{\sum_\ell e^{S_{i\ell}}},\quad Y=PV, $$
with positive denominators; masks restrict the finite sums to allowed sets and heads use finite parallel composition. These lowerings preserve denotation. Structural induction proves representation and Theorem 2 proves differentiation. $\square$
Completeness is relative to $\mathcal A$; representation size need not be optimal. The artifact implements representative cases, including valid stride-one convolution and one-head attention, rather than every theorem configuration.
5. Nonsmooth rules, dynamic traces and state
Stable-trace proposition. If a terminating execution has an open neighborhood executing the same finite smooth trace with the same discrete choices, its trace pullback is the classical derivative on that neighborhood. It is a finite smooth composition, so Theorem 2 applies. Termination at a point alone does not supply the neighborhood hypothesis.
A declared reverse rule has the type of $K$ but needs a rule label when proof (1) is unavailable. The artifact's ReLU convention is one on positive inputs and zero on nonpositive inputs. It is the derivative on open sign regions and a convention at zero. Classical derivatives, selected subgradients and surrogate gradients carry different claims. Routing boundaries, quantization and max ties need explicit treatment.
A custom-VJP interface permits separate forward/residual and backward definitions [6]; registration is not proof. PyTorch supplies a useful derivative inventory [7]. Opaque calls need domain, derivative and effect contracts; the interpreter rejects them.
For $S\times X\to S\times Y$, differentiable state enters the joint derivative. Stopping a derivative is explicit; optimizers/hooks/mutation need additional semantics. A fixed seed/noise input gives a conditional pathwise program when smooth. Differentiation under expectation requires separate hypotheses; no unbiased-estimator theorem is inferred.
6. Compiler preservation and numerical obligations
Definition. Paired exact refinement preserves represented forward values, reachable residual relations, cotangent zero/addition, and local backward actions. With exact encodings $e$ and related residuals $r,\hat r$, it includes
$$ \widehat F(e_Aa)=(e_Bf(a),\hat r),\qquad \widehat K(\hat r,e_{B^*}u)=e_{A^*}K(r,u). $$
The relations must be stable under the product, projection and accumulation constructors in use.
Theorem 4 (conditional compiler preservation). A type/wiring-preserving translation with such local paired refinements preserves the whole forward/pullback semantics.
Proof. Forward induction relates values and residuals. Reverse topological induction relates cotangents; preservation of zero and addition handles sharing. Apply the local backward contract at each step and the final projection. $\square$
No certified production lowering is implemented. StableHLO specifies operations/execution, while custom calls and reduction order need additional care [5]. Contracts must pin release, dtype, accumulation and exceptions; representable inputs do not ensure exact intermediates.
Theorem 5 (conditional numerical recurrence). Write exact forward states $z_i=H_i(z_{i-1})$ and decoded numerical states $\hat z_i$. Suppose $H_i$ has comparison bound $L_i$ and local forward defect at most $\delta_i$ on the region containing the compared states. For exact local pullback $K_i(z_i,-)$, suppose uniformly there
$$ \begin{aligned} \|K_i(\hat z_i,w)-K_i(\hat z_i,v)\|&\le M_i\|w-v\|,\\ \|K_i(\hat z_i,v)-K_i(z_i,v)\|&\le A_i\|\hat z_i-z_i\|\|v\|, \end{aligned} $$
and numerical local reverse error, including accumulation rounding, is at most $\eta_i$ at the actual arguments. The exact map must be defined on those saved states. For errors $e_i=\|\hat z_i-z_i\|$ and $d_i=\|\hat v_i-v_i\|$,
$$ e_i\le L_ie_{i-1}+\delta_i,\qquad d_{i-1}\le M_id_i+A_ie_i\|v_i\|+\eta_i. $$
Proof. Insert $H_i(\hat z_{i-1})$ for the forward comparison. In the reverse comparison insert $K_i(\hat z_i,\hat v_i)$ and $K_i(\hat z_i,v_i)$, then apply the three assumed bounds and triangle inequality. $\square$
Identical seed placement gives $d_n=0$. Bounds for $A_i$ require derivative regularity beyond mere continuity, for example bounded second derivatives on an appropriate neighborhood. The region, constants and overflow exclusions are not established by our tests. The target is the derivative of the ideal real program, not a classical derivative of discrete floating-point execution.
Exact-function proposition. Equality $f=g$ on an open domain for $C^1$ functions implies equal pullbacks, because their difference quotients agree. Rounded observations need not suffice: $f(x)=0$ and $g(x)=x^2$ both round to integer zero on $(-1/2,1/2)$ but have different derivatives away from zero. Equality at one input also does not determine a derivative.
The artifact adds a concrete compiler counterexample. Removing an identity reshape from one shared branch preserves the real function/pullback but regroups backward additions with contributions $10^{16},-10^{16},1$. NumPy float64 gives gradient 1 before the rewrite and 0 after it. This is a tested numerical difference, not a violation of the real theorem.
7. Residual symmetries and the semantic infinity-topos
Fix finite-dimensional $A,B$ and an open $U_0\subseteq A$. Let $\mathcal C$ be its small poset of open subsets, in a fixed universe. Let $\mathcal I(U)$ be the groupoid of mathematical smooth tape contracts for maps $U\to B$. An arrow between $t=(f,R,F,K)$ and $t'=(f,R',F',K')$ is a diffeomorphism $h:R\to R'$ such that
$$ F'=(\mathrm{id}_B\times h)F,\qquad K'(h(r),u)=K(r,u)\quad\text{for all }r,u. $$
Correctness proofs are treated propositionally. These invertible re-encodings compose, and restriction of $F$ defines a presheaf of groupoids. Diffeomorphisms are a discrete set of arrows. Let $\mathcal O(U)$ be the discrete set of smooth functions $U\to B$. Taking nerves gives $q:\mathcal I\to\mathcal O$ in the presheaf infinity-topos
$$ \mathcal X=\operatorname{Fun}(\mathcal C^{\mathrm{op}},\mathcal S). $$
The indexing category is $\mathcal C$; the semantic topos is $\mathcal X$. Open-cover sheaf descent is not asserted for these groupoids.
For nonempty $U$, every smooth $f$ admits the mathematical tape $R=U$, $F(a)=(f(a),a)$, $K(a,u)=Df(a)^*u$; for empty $U$, use a terminal residual and zero backward map. Thus $q$ is objectwise surjective on components and an effective epimorphism. These mathematical tapes need not be executable finite programs.
Proposition (implementation loops). A homotopy fiber of $q$ can have nontrivial fundamental group.
Proof. For $f=0$, take $R=\mathbb R$, $F(a)=(0,0)$ and $K(r,u)=0$. The nonidentity residual re-encoding $h(r)=-r$ is an involutive automorphism. The fundamental group of a groupoid nerve at an object is its automorphism group. The observation target is discrete, so the loop remains in its homotopy fiber. $\square$
This model retains implementation symmetries but is 1-truncated; higher certificate spaces require a further construction.
8. Policy descent
A policy is a subobject $P\hookrightarrow I$; it respects restriction and implementation isomorphisms. It is observable through $q:I\to O$ if $P\simeq q^*Q$ for a subobject $Q\hookrightarrow O$.
Theorem 6 (effective policy descent). For an effective epimorphism in any infinity-topos and projections $p_1,p_2:I\times_O I\rightrightarrows I$,
$$ P\text{ descends }\Longleftrightarrow p_1^*P\simeq p_2^*P \quad\text{over }I\times_O I. $$
The descended subobject is unique up to unique equivalence.
Proof. Necessity is pullback. Classify $P$ by $I\to\Omega$. Equality of its two restrictions supplies descent data on the kernel pair. Subobject comparisons are unique when they exist, hence the Cech coherences are automatic. Effective epimorphy identifies $O$ with the Cech nerve's colimit, giving the unique factorization $O\to\Omega$. $\square$
This applies standard descent [8]. The internal criterion concerns all generalized elements; global points alone need not suffice. Replace a general observation target by its image when necessary.
Corollary. Exact forward-function observation does not determine a residual-dimension budget. The same constant function and zero pullback have a terminal-residual tape and the one-dimensional tape above. The policy $\dim R=0$ is invariant under residual diffeomorphisms and restrictions but distinguishes this pair in one observation fiber, so it fails descent. Nonemptiness of residual spaces makes the dimension invariant well-defined.
In contrast, every object of $\mathcal I$ already has the correct mathematical pullback. Different correct tapes of one exact smooth function cannot have different mathematical derivatives. False custom backward rules require a larger space of declared, potentially uncertified implementations and an observation retaining their contract/certificate.
9. Artifact and evidence
The reference backend implements NumPy float64 static SSA, explicit saved-value tapes, independent JVP/VJP interpreters, representative architecture lowerings, JSON serialization and identity-reshape elimination. Run python verify.py --output verification-results.json. The recorded environment is Python 3.12.14, NumPy 2.3.5, seed 20261021.
Recorded results: 512 rational scalar DAGs with 2,048 exact value/full-gradient evaluations; all 494 small gather maps with lengths 1 through 4; 249 finite surjections with 6,726 Boolean-policy cases; 201 smooth tensor graphs with 603 directional/adjoint checks; 201 serialization and 201 ordinary rewrite comparisons; and 10 edge checks including the floating-point rewrite counterexample. Maximum normalized adjoint error was $4.30\times10^{-16}$ and relative directional discrepancy $4.45\times10^{-10}$; central-difference step and acceptance threshold were both $2\times10^{-6}$.
The rational coefficient oracle is separate from the floating-point interpreter. Numerical cases include five runs of eight architecture examples, 160 generated DAGs and one structural/reciprocal graph. Finite checks are evidence, not certification of the theorems or numerical bounds.
The builder is trusted Python, not an adversarial sandbox. Nonfinite intermediates and domain violations are rejected. Elementary softmax can overflow. No dynamic-loop engine, higher-order AD, general framework importer, hardware refinement or distributed execution semantics is implemented.
Authorship and automation
The anonymous author authorized preparation and submission. An OpenAI assistant drafted and reviewed the mathematics/code, checked primary sources and ran the tests. No independent referee or proof-assistant verification has occurred. Claims have the stated hypotheses; no exploit implementation is included.
References
[1] Cockett et al. *Reverse Derivative Categories.* CSL 2020. Primary paper.
[2] Vakar and Smeding. *CHAD: Combinatory Homomorphic Automatic Differentiation.* TOPLAS, 2022. DOI; open manuscript.
[3] Lucatelli Nunes and Vakar. *CHAD for Expressive Total Languages.* MSCS 33, 311-426, 2023. Open manuscript.
[4] Smeding and Vakar. *Efficient CHAD.* 2023. Primary manuscript.
[5] OpenXLA. *StableHLO Specification.* Official specification.
[6] JAX authors. *Custom JVPs or VJPs with custom_jvp and custom_vjp.* Official documentation.
[7] PyTorch contributors. *Autograd derivative definitions.* Official source.
[8] Lurie. *Higher Topos Theory.* 2009, Chapter 6, Section 6.2.3. Text. Software sources consulted 21 October 2026.