FDeriv

Analytic (HasFDerivAt/fderiv) correctness for tape-style SSA/DAG graphs.

NN/Proofs/Autograd/Tape/Core/Soundness.lean proves the global JVP/VJP adjointness law for DAG graphs against the tensor dot product.

This file adds the analytic upgrade (spec-level over ℝ):

• vectorize heterogeneous contexts into Euclidean space;
• assume each node's JVP is the Fréchet derivative of its forward map;
• derive jvp = fderiv and therefore backprop = (fderiv eval)†.

PyTorch correspondence / citations

• backpropVec is the proof-level analogue of a VJP accumulation pass over a dynamic tape. The main theorem backpropVec_eq_adjoint_fderiv corresponds to the slogan “reverse-mode = adjoint of the derivative of the forward map”. https://pytorch.org/docs/stable/autograd.html
• For PyTorch’s functional API perspective (Jacobian/VJP/JVP): see the “functional higher level” autograd docs. https://pytorch.org/docs/stable/autograd.html#functional-higher-level-api

noncomputable def Proofs.Autograd.tensorToVec {s : Spec.Shape} (t : TorchLean.Tensor ℝ s) : Vec s.size

Vectorize a tensor by flattening it (spec flattening order) and then using the Euclidean equivalence.

@[simp]

theorem Proofs.Autograd.tensorToVec_scalar (x : ℝ) (i : Fin Spec.Shape.scalar.size) : (tensorToVec (TorchLean.Tensor.scalar x)).ofLp i = x

The sole coordinate obtained by vectorizing a scalar tensor is the scalar itself.

noncomputable def Proofs.Autograd.vecToTensor {s : Spec.Shape} (v : Vec s.size) : TorchLean.Tensor ℝ s

Inverse of tensorToVec: interpret a vector as a tensor of shape s.

@[simp]

theorem Proofs.Autograd.tensorToVec_vecToTensor {s : Spec.Shape} (v : Vec s.size) : tensorToVec (vecToTensor v) = v

Vectorizing a tensor built from a vector gives the vector back.

@[simp]

theorem Proofs.Autograd.vecToTensor_tensorToVec {s : Spec.Shape} (t : TorchLean.Tensor ℝ s) : vecToTensor (tensorToVec t) = t

The other round trip, so tensorToVec and vecToTensor are mutually inverse.

Having both directions as simp lemmas is what lets the calculus below work entirely in EuclideanSpace and still state its conclusions about tensors.

def Proofs.Autograd.ctxSize : List Spec.Shape → ℕ

Total number of scalar coordinates in a heterogeneous context shape list.

@[reducible, inline]

abbrev Proofs.Autograd.CtxVec (Γ : List Spec.Shape) : Type

A vectorized context containing every entry of a TorchLean.TensorPack ℝ Γ.

def Proofs.Autograd.flattenCtx {Γ : List Spec.Shape} : TorchLean.TensorPack ℝ Γ → CtxVec Γ

Flatten a typed context TorchLean.TensorPack ℝ Γ into one big Euclidean vector.

Unlike PyTorch's dynamically typed saved-tensor array, this is an actual typed isomorphism: shapes are tracked in Γ, so the split points are definitional from ctxSize.

def Proofs.Autograd.unflattenCtx {Γ : List Spec.Shape} : CtxVec Γ → TorchLean.TensorPack ℝ Γ

Inverse of flattenCtx: split a CtxVec Γ back into a TorchLean.TensorPack ℝ Γ.

@[simp]

theorem Proofs.Autograd.unflattenCtx_flattenCtx {Γ : List Spec.Shape} (xs : TorchLean.TensorPack ℝ Γ) : unflattenCtx (flattenCtx xs) = xs

Unflattening a flattened context recovers the original tensor pack.

@[simp]

theorem Proofs.Autograd.flattenCtx_unflattenCtx {Γ : List Spec.Shape} (v : CtxVec Γ) : flattenCtx (unflattenCtx v) = v

And the reverse round trip, so a saved-tensor context and one flat gradient vector are the same data. This is what makes it legitimate to differentiate the whole graph as a single map Vec (ctxSize Γ) → Vec n and then read the result back per parameter.

noncomputable def Proofs.Autograd.castVec {n m : ℕ} (h : n = m) : Vec n → Vec m

Cast a Vec n to Vec m along an equality, by reindexing coordinates.

@[simp]

theorem Proofs.Autograd.castVec_apply {n m : ℕ} (h : n = m) (v : Vec n) (i : Fin m) : (castVec h v).ofLp i = v.ofLp (Fin.cast ⋯ i)

Coordinates of a cast vector are the coordinates of the original at the cast index.

@[simp]

theorem Proofs.Autograd.castVec_ofLp {n m : ℕ} (h : n = m) (v : Vec n) (i : Fin m) : (castVec h v).ofLp i = v.ofLp (Fin.cast ⋯ i)

castVec reindexes the coordinate function stored under the WithLp wrapper.

@[simp]

theorem Proofs.Autograd.castVec_rfl {n : ℕ} (v : Vec n) : castVec ⋯ v = v

Casting along rfl is the identity.

@[simp]

theorem Proofs.Autograd.castVec_add {n m : ℕ} (h : n = m) (u v : Vec n) : castVec h (u + v) = castVec h u + castVec h v

castVec is additive.

@[simp]

theorem Proofs.Autograd.castVec_smul {n m : ℕ} (h : n = m) (r : ℝ) (v : Vec n) : castVec h (r • v) = r • castVec h v

castVec commutes with scalar multiplication; with additivity this makes it linear, which is what allows a cast to be pushed through a derivative without a separate argument each time.

@[simp]

theorem Proofs.Autograd.castVec_castVec {n m k : ℕ} (h₁ : n = m) (h₂ : m = k) (v : Vec n) : castVec h₂ (castVec h₁ v) = castVec ⋯ v

Two casts compose into one along the composed equality.

theorem Proofs.Autograd.inner_castVec_castVec {n m : ℕ} (h : n = m) (x y : Vec n) : inner ℝ (castVec h x) (castVec h y) = inner ℝ x y

castVec preserves the Euclidean inner product.

This is the core “cast isometry” lemma used throughout the vectorized graph development.

theorem Proofs.Autograd.inner_castVec_left {n m : ℕ} (h : n = m) (x : Vec n) (y : Vec m) : inner ℝ (castVec h x) y = inner ℝ x (castVec ⋯ y)

A cast on the left of an inner product becomes the inverse cast on the right.

theorem Proofs.Autograd.tensorToVec_dim_apply {n : ℕ} {s : Spec.Shape} (f : Fin n → TorchLean.Tensor ℝ s) (p : Fin n × Fin s.size) : (tensorToVec (TorchLean.Tensor.dim f)).ofLp (finProdFinEquiv p) = (tensorToVec (f p.1)).ofLp p.2

Coordinate characterization of tensorToVec on a tensor .dim n s.

Informally, the vectorization order is the standard product order induced by finProdFinEquiv. No positivity hypothesis on Spec.Shape.size s is needed: the coordinate p.2 : Fin (Spec.Shape.size s) already witnesses it.

theorem Proofs.Autograd.inner_tensorToVec_dim {n : ℕ} {s : Spec.Shape} (a b : Fin n → TorchLean.Tensor ℝ s) : inner ℝ (tensorToVec (TorchLean.Tensor.dim a)) (tensorToVec (TorchLean.Tensor.dim b)) = ∑ i : Fin n, inner ℝ (tensorToVec (a i)) (tensorToVec (b i))

tensorToVec turns dot products on .dim n s into sums of Euclidean inner products over slices.

theorem Proofs.Autograd.dot_eq_inner_tensorToVec {s : Spec.Shape} (a b : TorchLean.Tensor ℝ s) : Spec.dot a b = inner ℝ (tensorToVec a) (tensorToVec b)

Main agreement lemma: tensor dot equals Euclidean inner product of vectorizations.

This is the bridge between Soundness.lean (stated using Spec.dot) and the analytic theorems here (stated using Euclidean inner).

noncomputable def Proofs.Autograd.appendVec {m n : ℕ} (a : Vec m) (b : Vec n) : Vec (m + n)

Concatenate two Euclidean vectors using Fin.append.

@[simp]

theorem Proofs.Autograd.flattenCtx_nil : flattenCtx TorchLean.TensorPack.nil = 0

The empty context flattens to the zero vector of the zero-dimensional space.

@[simp]

theorem Proofs.Autograd.flattenCtx_cons {s : Spec.Shape} {ss : List Spec.Shape} (x : TorchLean.Tensor ℝ s) (xs : TorchLean.TensorPack ℝ ss) : flattenCtx (TorchLean.TensorPack.cons x xs) = appendVec (tensorToVec x) (flattenCtx xs)

Flattening a cons concatenates the head tensor's coordinates in front of the tail's.

This is the layout convention the whole file depends on: parameters appear in context order, so a gradient vector can be split back apart by Fin.castAdd / Fin.natAdd alone.

@[simp]

theorem Proofs.Autograd.appendVec_ofLp_castAdd {m n : ℕ} (a : Vec m) (b : Vec n) (i : Fin m) : (appendVec a b).ofLp (Fin.castAdd n i) = a.ofLp i

Left half of a concatenation reads from the first vector.

@[simp]

theorem Proofs.Autograd.appendVec_ofLp_natAdd {m n : ℕ} (a : Vec m) (b : Vec n) (i : Fin n) : (appendVec a b).ofLp (Fin.natAdd m i) = b.ofLp i

Right half of a concatenation reads from the second vector.

theorem Proofs.Autograd.castVec_appendVec_assoc {m n p : ℕ} (a : Vec m) (b : Vec n) (c : Vec p) : castVec ⋯ (appendVec (appendVec a b) c) = appendVec a (appendVec b c)

Reassociating concatenated vectors only changes their finite-index representation.

theorem Proofs.Autograd.appendVec_cast_right {m n p : ℕ} (h : n = p) (a : Vec m) (b : Vec n) : appendVec a (castVec h b) = castVec ⋯ (appendVec a b)

Casting the right block of a concatenation is the same as casting the full vector.

theorem Proofs.Autograd.inner_append {m n : ℕ} (a c : Vec m) (b d : Vec n) : inner ℝ (appendVec a b) (appendVec c d) = inner ℝ a c + inner ℝ b d

Inner product of concatenated vectors splits as a sum of inner products.

theorem Proofs.Autograd.dotList_eq_inner_flattenCtx {Γ : List Spec.Shape} (x y : TorchLean.TensorPack ℝ Γ) : TensorPack.dotList x y = inner ℝ (flattenCtx x) (flattenCtx y)

TensorPack.dotList equals Euclidean inner product of flattenCtx.

This shows that the “context inner product” used in tape soundness is exactly the Euclidean inner product on the vectorized context representation.

noncomputable def Proofs.Autograd.castCtxVec {Γ₁ Γ₂ : List Spec.Shape} (h : Γ₁ = Γ₂) : CtxVec Γ₁ → CtxVec Γ₂

Cast a vectorized context along an equality of shape lists (reindexing coordinates).

@[simp]

theorem Proofs.Autograd.castCtxVec_rfl {Γ : List Spec.Shape} (v : CtxVec Γ) : castCtxVec ⋯ v = v

Casting a vectorized context along rfl is the identity.

@[simp]

theorem Proofs.Autograd.castCtxVec_cast {Γ₁ Γ₂ Γ₃ : List Spec.Shape} (h₁ : Γ₁ = Γ₂) (h₂ : Γ₂ = Γ₃) (v : CtxVec Γ₁) : castCtxVec h₂ (castCtxVec h₁ v) = castCtxVec ⋯ v

Context casts compose. Together with castCtxVec_rfl this keeps the casts introduced by graph composition from piling up in the goal.

The next few lemmas are bookkeeping for splitting/concatenating vectorized contexts. They are “obvious” from the list structure of Γ, but it is useful to expose them as named facts so that the calculus proofs later can use them without redoing shape arithmetic.

theorem Proofs.Autograd.ctxSize_append (Γ ss : List Spec.Shape) : ctxSize (Γ ++ ss) = ctxSize Γ + ctxSize ss

ctxSize respects list append (sizes add).

theorem Proofs.Autograd.ctxSize_snoc (ss : List Spec.Shape) (τ : Spec.Shape) : ctxSize (ss ++ [τ]) = ctxSize ss + τ.size

Specialized ctxSize_append for snoc (Γ ++ [τ]).

noncomputable def Proofs.Autograd.snocCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (ctx : CtxVec Γ) (t : Vec τ.size) : CtxVec (Γ ++ [τ])

Append one tensor-vector block to a vectorized context.

theorem Proofs.Autograd.appendVec_snocCtx {s : Spec.Shape} {Γ : List Spec.Shape} {τ : Spec.Shape} (a : Vec s.size) (ctx : CtxVec Γ) (t : Vec τ.size) : appendVec a (snocCtx ctx t) = snocCtx (appendVec a ctx) t

Prefixing a context vector commutes with appending its final tensor block.

noncomputable def Proofs.Autograd.unsnocCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (ctx : CtxVec (Γ ++ [τ])) : CtxVec Γ × Vec τ.size

Inverse of snocCtx: split CtxVec (Γ ++ [τ]) into its prefix and last block.

theorem Proofs.Autograd.unsnocCtx_snocCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (ctx : CtxVec Γ) (t : Vec τ.size) : unsnocCtx (snocCtx ctx t) = (ctx, t)

unsnocCtx (snocCtx ctx t) = (ctx, t).

theorem Proofs.Autograd.snocCtx_unsnocCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (ctx : CtxVec (Γ ++ [τ])) : snocCtx (unsnocCtx ctx).1 (unsnocCtx ctx).2 = ctx

snocCtx (unsnocCtx ctx) = ctx.

noncomputable def Proofs.Autograd.Node.forwardVec {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) : CtxVec Γ → Vec τ.size

Vectorized forward map of a tape Node: CtxVec Γ → Vec (Spec.Shape.size τ).

noncomputable def Proofs.Autograd.Node.jvpVec {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) : CtxVec Γ → CtxVec Γ → Vec τ.size

Vectorized JVP of a tape Node: the node-level forward-mode action on tangents.

noncomputable def Proofs.Autograd.Node.vjpVec {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) : CtxVec Γ → Vec τ.size → CtxVec Γ

Vectorized VJP of a tape Node: pushes a cotangent vector back to the input context.

theorem Proofs.Autograd.Node.correct_inner {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) (ctxV dctxV : CtxVec Γ) (δV : Vec τ.size) : inner ℝ (node.jvpVec ctxV dctxV) δV = inner ℝ dctxV (node.vjpVec ctxV δV)

Vectorized form of Node.correct (adjointness law).

Statement: ⟪jvp(x,dx), δ⟫ = ⟪dx, vjp(x,δ)⟫.

def Proofs.Autograd.Graph.evalVec {Γ ss : List Spec.Shape} (g : Graph Γ ss) (xV : CtxVec Γ) : CtxVec (Γ ++ ss)

Vectorized evaluation of a tape Graph.

Returns a CtxVec (Γ ++ ss) containing the original inputs and all intermediate node outputs.

def Proofs.Autograd.Graph.jvpVec {Γ ss : List Spec.Shape} (g : Graph Γ ss) (xV dxV : CtxVec Γ) : CtxVec (Γ ++ ss)

Vectorized JVP for a whole graph: forward-mode derivative of evalVec.

def Proofs.Autograd.Graph.backpropVec {Γ ss : List Spec.Shape} (g : Graph Γ ss) (xV : CtxVec Γ) (seedV : CtxVec (Γ ++ ss)) : CtxVec Γ

Vectorized reverse-mode accumulation (VJP) for a whole graph.

seedV is a cotangent for the entire Γ ++ ss context (inputs plus intermediates), matching the global tape soundness theorem.

theorem Proofs.Autograd.flattenCtx_cast {Γ₁ Γ₂ : List Spec.Shape} (h : Γ₁ = Γ₂) (xs : TorchLean.TensorPack ℝ Γ₁) : flattenCtx (TorchLean.TensorPack.cast h xs) = castCtxVec h (flattenCtx xs)

flattenCtx commutes with casting a context along a shape-list equality.

theorem Proofs.Autograd.tensorToVec_addSpec {s : Spec.Shape} (a b : TorchLean.Tensor ℝ s) : tensorToVec (a.addSpec b) = tensorToVec a + tensorToVec b

Vectorization is additive: tensorToVec maps addSpec to vector addition.

theorem Proofs.Autograd.flattenCtx_add {Γ : List Spec.Shape} (u v : TorchLean.TensorPack ℝ Γ) : flattenCtx (u.add v) = flattenCtx u + flattenCtx v

flattenCtx maps context addition to vector addition.

theorem Proofs.Autograd.flattenCtx_snoc {Γ : List Spec.Shape} {τ : Spec.Shape} (xs : TorchLean.TensorPack ℝ Γ) (y : TorchLean.Tensor ℝ τ) : flattenCtx (xs.snoc y) = snocCtx (flattenCtx xs) (tensorToVec y)

flattenCtx maps TorchLean.TensorPack.snoc to snocCtx.

theorem Proofs.Autograd.unsnocCtx_flattenCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (w : TorchLean.TensorPack ℝ (Γ ++ [τ])) : unsnocCtx (flattenCtx w) = (flattenCtx w.unsnoc.1, tensorToVec w.unsnoc.2)

flattenCtx maps TorchLean.TensorPack.unsnoc to unsnocCtx.

theorem Proofs.Autograd.Node.forwardVec_flattenCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) (x : TorchLean.TensorPack ℝ Γ) : node.forwardVec (flattenCtx x) = tensorToVec (node.forward x)

The vectorized forward map, evaluated on a flattened context.

theorem Proofs.Autograd.Node.jvpVec_flattenCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) (x dx : TorchLean.TensorPack ℝ Γ) : node.jvpVec (flattenCtx x) (flattenCtx dx) = tensorToVec (node.jvp x dx)

The vectorized JVP, evaluated on flattened contexts.

theorem Proofs.Autograd.Node.vjpVec_flattenCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) (x : TorchLean.TensorPack ℝ Γ) (δ : TorchLean.Tensor ℝ τ) : node.vjpVec (flattenCtx x) (tensorToVec δ) = flattenCtx (node.vjp x δ)

The vectorized VJP, evaluated on a flattened context and a vectorized cotangent.

theorem Proofs.Autograd.Graph.evalVec_flattenCtx {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x : TorchLean.TensorPack ℝ Γ) : g.evalVec (flattenCtx x) = flattenCtx (g.eval x)

The Euclidean graph evaluation is the flattening of the TensorPack evaluation.

theorem Proofs.Autograd.Graph.jvpVec_flattenCtx {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x dx : TorchLean.TensorPack ℝ Γ) : g.jvpVec (flattenCtx x) (flattenCtx dx) = flattenCtx (g.jvpCtx x dx)

The Euclidean graph JVP is the flattening of the TensorPack JVP.

theorem Proofs.Autograd.Graph.backpropVec_flattenCtx {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x : TorchLean.TensorPack ℝ Γ) (seed : TorchLean.TensorPack ℝ (Γ ++ ss)) : g.backpropVec (flattenCtx x) (flattenCtx seed) = flattenCtx (g.backpropCtx x seed)

The Euclidean reverse pass is the flattening of the TensorPack reverse pass.

theorem Proofs.Autograd.Graph.backprop_correct_inner {Γ ss : List Spec.Shape} (g : Graph Γ ss) (xV dxV : CtxVec Γ) (seedV : CtxVec (Γ ++ ss)) : inner ℝ (g.jvpVec xV dxV) seedV = inner ℝ dxV (g.backpropVec xV seedV)

Vectorized tape soundness: ⟪jvp, seed⟫ = ⟪dx, backprop seed⟫. It is backprop_correct read through flattenCtx, a bijection carrying dotList to the Euclidean inner product.

structure Proofs.Autograd.NodeFDerivCorrect {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) : Type

Per-node analytic correctness assumption: JVP is the Fréchet derivative.

This is the hypothesis that upgrades the dot-level soundness theorem into an fderiv statement.

• deriv : CtxVec Γ → CtxVec Γ →L[ℝ] Vec τ.size

  The derivative packaged as a continuous linear map.

• hasFDerivAt (xV : CtxVec Γ) : HasFDerivAt node.forwardVec (self.deriv xV) xV

  The forward map has the above derivative everywhere.

• jvp_eq (xV dxV : CtxVec Γ) : node.jvpVec xV dxV = (self.deriv xV) dxV

  The node's JVP function agrees with the packaged derivative.

def Proofs.Autograd.GraphFDerivCorrect {Γ ss : List Spec.Shape} : Graph Γ ss → Type

Graph predicate: every node satisfies NodeFDerivCorrect.

structure Proofs.Autograd.NodeFDerivCorrectAt {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) (xV : CtxVec Γ) : Type

Pointwise per-node analytic correctness.

Used when a node is only differentiable under side conditions at a particular basepoint xV (e.g. inv, sqrt, log, or piecewise ops).

• deriv : CtxVec Γ →L[ℝ] Vec τ.size

  The Fréchet derivative at xV, as a continuous linear map on the flattened context.

• hasFDerivAt : HasFDerivAt node.forwardVec self.deriv xV

  deriv really is the derivative of the node's forward pass at xV.

• jvp_eq (dxV : CtxVec Γ) : node.jvpVec xV dxV = self.deriv dxV

  The node's hand-written JVP agrees with the analytic derivative. This is the field that turns an analysis fact into a statement about the code that actually runs.

def Proofs.Autograd.NodeFDerivCorrect.at {Γ : List Spec.Shape} {τ : Spec.Shape} {node : Node Γ τ} (hn : NodeFDerivCorrect node) (xV : CtxVec Γ) : NodeFDerivCorrectAt node xV

Specialize a global NodeFDerivCorrect proof to a particular basepoint.

This is the common “turn an everywhere-differentiable node into a pointwise differentiable node” adapter used when assembling GraphFDerivCorrectAt proofs.

def Proofs.Autograd.GraphFDerivCorrectAt {Γ ss : List Spec.Shape} : Graph Γ ss → CtxVec Γ → Type

Pointwise graph predicate: every node is differentiable at the actual intermediate values.

Note the recursion uses Graph.evalVec to compute the basepoint for each successive node.

noncomputable def Proofs.Autograd.GraphFDerivCorrect.at {Γ ss : List Spec.Shape} {g : Graph Γ ss} (hg : GraphFDerivCorrect g) (xV : CtxVec Γ) : GraphFDerivCorrectAt g xV

Specialize an everywhere-correct graph proof to a pointwise graph proof, the graph-level analogue of NodeFDerivCorrect.at.

Each node certificate is read at the intermediate value that Graph.evalVec produces there. This is how a globally smooth block feeds a pointwise block such as LayerNorm, and how the global fderiv theorems below are obtained from their pointwise versions.

noncomputable def Proofs.Autograd.Graph.appendCLM (m n : ℕ) : Vec m × Vec n →L[ℝ] Vec (m + n)

Fin.append packaged as a continuous linear map on Euclidean vectors.

noncomputable def Proofs.Autograd.Graph.castCLM {n m : ℕ} (h : n = m) : Vec n →L[ℝ] Vec m

castVec packaged as a continuous linear map (finite-dimensional, hence continuous).

@[simp]

theorem Proofs.Autograd.Graph.castCLM_apply {a b : ℕ} (h : a = b) (v : Vec a) : (castCLM h) v = castVec h v

Graph.castCLM acts by castVec.

noncomputable def Proofs.Autograd.Graph.snocCLM {Γ : List Spec.Shape} {τ : Spec.Shape} : CtxVec Γ × Vec τ.size →L[ℝ] CtxVec (Γ ++ [τ])

Continuous linear map version of snocCtx (concatenation + cast).

theorem Proofs.Autograd.Graph.hasFDerivAt_evalVec_and_jvp_at {Γ ss : List Spec.Shape} (g : Graph Γ ss) (xV : CtxVec Γ) : ∀ (a : GraphFDerivCorrectAt g xV), ∃ (D : CtxVec Γ →L[ℝ] CtxVec (Γ ++ ss)), HasFDerivAt g.evalVec D xV ∧ ∀ (dxV : CtxVec Γ), g.jvpVec xV dxV = D dxV

Main induction: evalVec is differentiable at xV, and its derivative agrees with jvpVec.

This is the technical heart of the jvp = fderiv theorem. It is stated pointwise so that graphs involving non-smooth or partial primitives only need differentiability at the values encountered during execution; the everywhere-differentiable version below is its specialization.

Pointwise corollaries. Once HasFDerivAt evalVec = jvpVec is known, jvpVec = fderiv is immediate, and backpropVec = (fderiv evalVec)† follows from the inner-product characterization of the adjoint together with the vectorized tape soundness law backprop_correct_inner.

theorem Proofs.Autograd.Graph.jvpVec_eq_fderiv_at {Γ ss : List Spec.Shape} (g : Graph Γ ss) (xV dxV : CtxVec Γ) : ∀ (a : GraphFDerivCorrectAt g xV), g.jvpVec xV dxV = (fderiv ℝ g.evalVec xV) dxV

Under GraphFDerivCorrectAt, the graph JVP at xV equals the Fréchet derivative of evalVec at xV.

theorem Proofs.Autograd.Graph.backpropVec_eq_adjoint_fderiv_at {Γ ss : List Spec.Shape} (g : Graph Γ ss) (xV : CtxVec Γ) (seedV : CtxVec (Γ ++ ss)) : ∀ (a : GraphFDerivCorrectAt g xV), g.backpropVec xV seedV = (ContinuousLinearMap.adjoint (fderiv ℝ g.evalVec xV)) seedV

Under GraphFDerivCorrectAt, backpropVec at xV is the adjoint of the derivative of evalVec at xV.

theorem Proofs.Autograd.Graph.hasFDerivAt_evalVec_and_jvp {Γ ss : List Spec.Shape} (g : Graph Γ ss) (hg : GraphFDerivCorrect g) (xV : CtxVec Γ) : ∃ (D : CtxVec Γ →L[ℝ] CtxVec (Γ ++ ss)), HasFDerivAt g.evalVec D xV ∧ ∀ (dxV : CtxVec Γ), g.jvpVec xV dxV = D dxV

evalVec is differentiable everywhere and its derivative agrees with jvpVec, for a graph whose nodes carry global NodeFDerivCorrect certificates.

theorem Proofs.Autograd.Graph.jvpVec_eq_fderiv {Γ ss : List Spec.Shape} (g : Graph Γ ss) (hg : GraphFDerivCorrect g) (xV dxV : CtxVec Γ) : g.jvpVec xV dxV = (fderiv ℝ g.evalVec xV) dxV

Under GraphFDerivCorrect, the graph JVP equals the Fréchet derivative fderiv of evalVec.

theorem Proofs.Autograd.Graph.backpropVec_eq_adjoint_fderiv {Γ ss : List Spec.Shape} (g : Graph Γ ss) (hg : GraphFDerivCorrect g) (xV : CtxVec Γ) (seedV : CtxVec (Γ ++ ss)) : g.backpropVec xV seedV = (ContinuousLinearMap.adjoint (fderiv ℝ g.evalVec xV)) seedV

Main analytic theorem: backpropVec equals the adjoint of the derivative of evalVec.

This is the proof-level formalization of “reverse-mode computes a VJP”, stated as an equality of linear maps in a Euclidean space.