Main result
For a finite typed smooth circuit whose primal trace is available, reverse each input-port occurrence, transpose the local derivative at the saved primal value, and add cotangents at shared sources. Each legal schedule computes the same forward map and its cotangent pullback. We present the proof, its coherent 2-categorical factorization, a base-change law for finite aggregation, and an executable three-node implementation.
The double-column manuscript contains the complete arguments, figures, protocol details, and references. Its standalone UTF-8 LaTeX source accompanies the PDF as an explicitly indexed text attachment. The replication archive contains the runner, verifier, datasets with checksums, and both full runs' serial evidence.
Circuits, schedules and lenses
Let \(C:X\to Y\) be a finite acyclic circuit with smooth primitives \(f_v\). The dependency graph retains each input and boundary output port as an occurrence. A wire can feed several ports, including multiple ports of the same primitive. Given a forward value \(x\) and an output seed \(\bar y\), the dual sends cotangents from each consumer to its source, using \(Df_v^*\) for each local operation. A wire with several consumers adds their contributions. A wire with none receives zero.
Distributed pullback. Any legal evaluation delivering every contribution exactly once computes \(DF_C(x)^*\bar y\), independently of placement when the communication implements the declared wire maps.
For the proof, propagate an arbitrary tangent \(\dot x\) forward. Pair the terminal tangents with the boundary cotangent. Moving each pairing through a primitive is the identity \[ \langle \bar z,Df_v\,\dot w\rangle =\langle Df_v^*\,\bar z,\dot w\rangle . \] At a shared wire, linearity collects the occurrence-level pairings into one with the sum of cotangents. A reverse induction eliminates the internal pairings and leaves the boundary input. Equality for every \(\dot x\) identifies the pullback. For example the adjoint of a replication map \(\Delta(x)=(x,\ldots,x)\) is summation, and the adjoint of addition duplicates the cotangent.
A schedule is a linear extension of the event order. Form a locally groupoidal 2-category with typed boundaries as objects and scheduled circuits as 1-cells. Give two schedules of the same underlying circuit a unique invertible 2-cell. A rescheduling can be generated by adjacent swaps of incomparable events. To obtain a target linear extension, move its first element to the front of the current extension. Every crossed element is incomparable, since either possible strict comparison would violate one of the extensions. Then induct on the remaining suffix.
Gluing composes circuits, concatenation composes schedules, and disjoint union supplies the symmetric monoidal structure. Two parallel coherence composites agree by uniqueness of the schedule comparison. Mapping a circuit to the reverse lens \((F_C,x\mapsto DF_C(x)^*)\) preserves composition and tensor by the chain and product rules. It sends each schedule 2-cell to an identity and factors through the category of unscheduled circuits. Each schedule fiber in a hom-groupoid is nonempty and has exactly one arrow between any two objects. Its nerve is contractible. The forgetful map therefore induces an equivalence on homotopy-coherent nerves after passing from the hom-groupoids to their mapping spaces. This construction retains schedule identifications and quotients swap histories.
For a finite map \(u:I\to J\), reindexing on module families has left and right adjoints given by finite sums and products over the fibers. A pullback square with upper and lower horizontal maps \(a,b\) gives \(b^*\Sigma_u\cong\Sigma_{u'}a^*\) by the corresponding fiber bijections. The comparison commutes with the fold that sums reverse contributions and is compatible with pasting. For smooth vector-bundle programs over a context manifold, vertical differentiation, transpose and finite sums commute with restriction. Compatible local programs and their local duals consequently glue in the sheaf semantics, also viewed in the \(0\)-truncated part of the associated infinity-topos of sheaves of spaces.
SGD and the two baselines
For a batch \(I\) of \(B\) independent uniform draws, let \(\ell_i\) be multiclass softmax cross-entropy and \(\lambda=10^{-4}\) in the experiments. The dual returns \[ g_I(\theta)=B^{-1}\sum_{i\in I}\nabla\ell_i(\theta)+\lambda\theta . \] This is an unbiased estimator of the regularized empirical gradient. Under \(L\)-smoothness along the update and a per-example variance trace bounded by \(\sigma^2\), a step \(\eta\le 1/L\) has conditional expected descent bounded by \[ \mathbb E[F(\theta-\eta g_I)\mid\theta]\le F(\theta)-\frac{\eta}{2}\|\nabla F(\theta)\|^2 +\frac{L\eta^2\sigma^2}{2B}. \] The proof combines the smoothness inequality with the minibatch variance bound \(\sigma^2/B\). If the sampling kernel and update rule are fixed, rescheduling preserves the one-step Markov kernel and, by coupling on common draws, the finite-horizon law of optimizer states.
The real-coded genetic algorithm evaluates eight candidates on a common minibatch, keeps two elites, and generates offspring through affine crossover and block-scaled Gaussian mutation. It uses forward queries only.
The boosting rule learns additive coefficient blocks on a finite dictionary of scalar feature atoms. On the tanh network it uses the same initial hidden representation as a frozen-feature SGD control. For the uniform distribution \(u\) on batch positions, its weights solve \[ q_\tau=\arg\max_{q\in\Delta_B} \{\langle q,\ell\rangle-\tau\,\mathrm{KL}(q\|u)\},\qquad q_{\tau,a}=\frac{e^{\ell_a/\tau}}{\sum_b e^{\ell_b/\tau}} . \] At the resulting expected loss, these weights uniquely maximize Shannon entropy. The coordinator sends weighted logit residuals and \(q_\tau\); each worker computes the score of its best weak atom. The coordinator selects the block with maximal squared gradient divided by its positive diagonal surrogate coefficient, then applies a damped block update. Uniform boosting uses the same dictionary and update with uniform weights.
Three-QEMU-guest evaluation
Two QEMU guests own model and feature shards; the third owns the labels, loss and updates. Guest TCP runs over emulated e1000 interfaces. The host handles virtual Ethernet and writes serial logs. The loss coordinator pairs backward requests with the exact forward tape on each worker. The tasks are stratified Iris with RBF landmarks, a new split of the 1,797-row UCI digits file with RBF landmarks and with a 32-unit tanh MLP, and balanced subsets of pooled Fashion-MNIST. Across each of five seeds, the three main optimizers each have three validation configurations. Each configuration spends 384 forward queries of 48 examples, including genetic candidate evaluations. The budget allows different backward work and numbers of independently drawn batches.
| Workload | SGD accuracy | Genetic accuracy | Entropy boost accuracy | Uniform boost accuracy |
|---|---|---|---|---|
| Iris RBF | 96.67% | 90.00% | 96.00% | 96.67% |
| Digits RBF | 95.38% | 43.75% | 93.21% | 93.48% |
| Digits MLP | 96.09% | 26.41% | 88.21% | 87.83% |
| Fashion linear | 78.24% | 33.87% | 72.95% | 72.78% |
SGD gave the lowest mean test negative log likelihood on each workload. Entropy weighting had mixed accuracy effects and raised mean test log loss relative to uniform boosting on all four tasks. Frozen SGD scored 88.91% on Digits MLP, compared with 96.09% for full SGD. In the reference deployment, the genetic baseline used the fewest application bytes and had the shortest training time at the selected configurations. These observations apply to fixed splits, model classes, hyperparameter grids and forward-query budgets on one emulated LAN.
The maximum absolute discrepancy in the distributed directional derivative checks was \(3.83\times10^{-11}\). Two independent full runs with fresh guests reproduced the numeric results and application-byte counts exactly. Each worker logged 87,460 forward requests, 28,808 full reverse requests and 30,720 boosting-statistics requests. Each endpoint's counts reconcile with the independently reconstructed application protocol totals. The verifier permits machine-dependent timing and Ethernet frame counts.
References and responsibility
- Cockett et al., Reverse Derivative Categories.
- Cruttwell et al., Categorical Foundations of Gradient-Based Learning.
- Utke et al., Toward Adjoinable MPI.
- Lurie, Higher Topos Theory.
- Bottou, Curtis and Nocedal, Optimization Methods for Large-Scale Machine Learning.
- Warmuth, Glocer and Vishwanathan, Entropy Regularized LPBoost.
The commissioning researcher is the responsible contributor under the anonymous byline. An AI coding and writing assistant developed the manuscript and software, executed and compared the two cluster runs, and prepared the artifacts under the researcher's direction.