Main result
This manuscript extends the correctness argument of Huot, Staton, and Vákár from set-valued relations on diffeological plots to spaces of witnesses in a comma ∞-category. The resulting lifting is stable under changes of parameter base in a smooth ∞-topos. Its first-order connected-plot specialization gives the original tangent comparison. The companion CertJet compiler lowers typed differentiable lambda programs to stack code in Lean 4. A TCP runtime evaluates user-supplied objectives and their forward derivatives with that code.
Higher categorical gluing
Let \(F\colon\mathcal C\to\mathcal W\) preserve finite products, with both categories cartesian closed and \(\mathcal W\) admitting pullbacks. Form \[ \mathcal G_F=\mathcal C\times_{\mathcal W}\operatorname{Fun}(\Delta^1,\mathcal W), \] where the map from the arrow category takes the codomain. An object is \((A,R,\rho\colon R\to F A)\). The mapping space to \((B,S,\sigma)\) is \[ \operatorname{Map}_{\mathcal C}(A,B) \times_{\operatorname{Map}_{\mathcal W}(R,FB)} \operatorname{Map}_{\mathcal W}(R,S). \] This records the path exhibiting preservation of a witness and all higher paths between such data. When \(F\) is the identity on spaces, maps from \((*,*,\mathrm{id})\) to \((*,BG,!)\) form the space \(BG\), even though the underlying base map is unique.
Products use the two component products. The exponential has base \(B^A\) and witness \(F(B^A)\times_{(FB)^R} S^R\). The map from \(F(B^A)\) is adjoint to evaluation along \(\rho\). Mapping into this pullback and currying gives the exponential adjunction. Colimits are computed on bases and witnesses. A map out of the colimit is a limit of the corresponding mapping-space pullbacks. Lists are coproducts of finite powers. Finitely branching polynomial datatypes are coproducts over finite tree shapes of products of their node-label objects. Their algebra-map spaces are contractible by induction on tree height, because specifying each map and its path to the composite of lower-height maps is a contractible extension.
If both categories are ∞-toposes and \(F\) is accessible and left exact, the gluing is an ∞-topos. Accessibility and the colimit formula give presentability. Finite limits are componentwise. The projections jointly reflect equivalences, so universality and disjointness of colimits and effectiveness of groupoid objects follow componentwise. In the relative construction over \(B\), all formulas are computed in slices. Pullback preserves slice exponentials by the adjunction for dependent sum and the projection formula. For an effective epimorphism \(U\to B\), slice descent and the comma pullback formula identify \(\mathcal G_{F_B}\) with the limit of the gluing categories over the Čech nerve.
Smooth jet graph and specialization
In the ∞-topos of sheaves of spaces on the smooth Cartesian site, let \(L\) represent the real line and take \(K=L\). For a chart \(U\), a generalized point of \(L^K\) is a smooth function \(f(u,t)\) on \(U\times\mathbb R\). Sending it to \((f,\partial_t f)\) defines a morphism \(j\colon L^K\to(L\times L)^K\) natural in \(U\). Use \(F(A,B)=A^K\times B^K\) and the graph of \(j\) as the scalar witness. A smooth primitive \(p\) lifts to \[ p_D((x_i,v_i)_i)=\left(p(x),\sum_i\partial_i p(x)v_i\right) \] by the chain rule. Interpret the typed constructors in the gluing. The projections preserve products, variants, arrows and folds, so the projected terms are the primal and forward-AD interpretations. At a function type, the exponential witness expresses preservation of related arguments.
For a nonempty connected diffeological probe, pass to the full subcategory with monomorphism witnesses over the discrete sets of plots. Objects are ordinary relations, and a morphism is a pair preserving the relation. Products and exponentials remain monic. Sums and list powers have disjoint tags on connected plots, so they also remain monic. Taking the probe to be \(\mathbb R\) recovers the gluing of Huot, Staton, and Vákár. At first-order types the interpreted spaces are countable disjoint unions of Euclidean spaces. The lifted spaces identify canonically with tangent bundles. Each tangent vector is represented by a curve, so the witness equation identifies the lifted function with the ordinary tangent map on all first-order values.
For a finite Weil algebra with nilpotent ideal \(\mathfrak m\), a primitive is prolonged by finite Taylor evaluation on \(\mathfrak m\). Taylor substitution and nilpotence prove functoriality. The same gluing lifts the full grammar. For a square-zero algebra with tangent module \(V\), the linear continuations \(z\mapsto zv\) give the corresponding continuation representation by evaluation at \(1\). The paper also gives the example \([\mathbb R^2/C_m]\) with rotation action. A generalized curve is a finite principal bundle and an equivariant map. Lift the curve direction along the locally diffeomorphic bundle projection to differentiate that map. The squared norm has lifted derivative \(2\langle x,v\rangle\), and the jet witness retains the automorphisms of the constant zero curve.
Lean compiler and distributed evaluation
The source grammar has reals, unit, empty, products, sums, functions, and lists with right fold. It supports closures, dynamic variants and lists, and scalar costs formed by arbitrary well-typed compositions in the grammar. The stack code carries indices for the environment and input and output stacks. The Lean theorem lower_correct states that lowering any source term into an arbitrary typed continuation and running it equals evaluating the source term and pushing the result before the same continuation. Its proof is structural induction, including closure capture, typed branch selection, and the list recursor. The specialized theorem compile_correct gives preservation for the empty-stack compiler entry point.
The theorem fundamental lifts any primitive-preserved scalar relation to terms of every type. At arrows it quantifies over related arguments, at sums it compares matching payloads, and at lists it inducts on the list relation. Instantiating with the graph of a jet operator and applying compiler preservation gives compiled_jet_sound. The theorem is conditional on local differential laws. The manuscript proves the real primitive interpretation using the chain rule. Lean also proves an exact polynomial instance by computing coefficients through independent Cauchy convolution. An exact closure example reduces to primal value \(25\) and directional derivative \(10\) at a designated input and direction.
For a supplied scalar cost, choose real leaf coordinates in the context. The CLI also accepts a separate cost body that binds the original expression before type checking. A whole coupled objective can occupy a single sample, while empirical risk is the mean of several sample costs. Jobs are indexed by samples and coordinate directions. A worker checks the stack artifact and executes the code with the appropriate seed. For lawful exact primitives, the returned tangent for job \((i,j)\) is \(D\ell_i(\theta)e_j\). Linearity of the finite sum identifies the reduced array with the gradient. Lean's total_schedule proves independence of finite shard partition and permutation for an associative, commutative exact reduction. The binary64 runtime restores a fixed input order before reduction. The Lean selector choose returns the base or one of the scored trials and has a nonincrease theorem for a sound comparison. The optimizer tests finitely many rates along the negative gradient and accepts a strict measured improvement.
The Lean guarantees apply to typed instructions, lawful jet models, and the specified reduction and score laws. The bytecode codec, TCP coordinator, and binary64 math library are exercised by the reproducibility suite. The runtime uses a forward coordinate sweep, finite-dimensional optimization, and first-order wire values. Higher-order terms can be compiled and used inside a scalar cost in the source. The finite Weil-jet and ∞-topos results are mathematical results in the PDF.
Execution evidence
Lean 4.19.0 builds the package. The axiom audit reports only the standard Lean dependencies propext and Quot.sound where used. The suite used three separate TCP workers on one Linux x86-64 host. It contains 25 small architecture cases spanning MLP, CNN, ResNet, RNN, GRU, LSTM, encoder and decoder transformers, vision transformers, graph convolution, selective state spaces, a gated-delta attention hybrid, dense and fixed-route sparse mixtures, diffusion U-Net and DiT, VAE, both GAN objectives, Real NVP, flow matching, CLIP-style contrastive learning, Conformer, and recommendation models. A separate higher-order case matches an analytic derivative through a captured closure, sum matching, and a runtime list fold. Every case matched the one-worker reduction and accepted four strictly improving steps. Across 935 coordinate checks, the largest scaled discrepancy from the independent source interpreter's central differences was \(6.62\times10^{-10}\).
The attachment contains the complete PDF, LaTeX, Lean code, TCP runtime, deterministic example generator, and raw measurements. Prepared for anonymous review. The work used AI-assisted drafting and implementation.
Selected references
- Huot, Staton, and Vákár. Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing.
- Huot, Staton, and Vákár. Higher Order Automatic Differentiation of Higher Order Functions.
- Vákár and Smeding. CHAD.
- Lurie. Higher Topos Theory.
- Shah. Recollements and stratification.
- Baez and Hoffnung. Convenient Categories of Smooth Spaces.
- Bauer, Burke, and Ching. Tangent ∞-categories and Goodwillie calculus.