Analytic upgrade of the runtime link: reverse mode computes (fderiv eval)†

Two independent developments meet in this file.

• The runtime link (Runtime/Link/BackwardGraph.lean) proves that the tape engine's dense reverse pass (Tape.backwardDenseFrom) agrees with the algebraic model's full backpropagation backpropAllCtx, over any commutative semiring carrier and an arbitrary non-differentiable environment Δ.
• The analytic tape model (Tape/Core/FDeriv.lean) proves that reverse-mode accumulation computes the adjoint of the Fréchet derivative of the forward evaluation, over ℝ.

The two developments are stated on different graph types: the algebraic Algebra.Graph (α := α) Δ Γ ss versus the ℝ-monomorphic, environment-free Proofs.Autograd.Graph Γ ss. Their contexts already coincide (TList Γ is by definition Algebra.TList ℝ Γ), and their eval/jvpCtx/backpropCtx recursions mirror each other node for node — what has been missing is the formal connection. This file supplies it:

• The real, environment-free slice. Algebra.Node.toReal / Algebra.Graph.toReal specialize an algebraic graph at α := ℝ and a fixed environment d : Δ to an analytic graph; Node.toAlgebra / Graph.toAlgebra embed an analytic graph back as the Δ := Unit slice, and both round trips are identities on that slice (toAlgebra_toReal and toReal_toAlgebra). The analytic model is therefore exactly the environment-free ℝ slice of the algebraic model. The commutation lemmas toReal_eval, toReal_jvpCtx, toReal_backpropCtx show the specialization preserves all three semantics.
• Input-prefix extraction. TList.takeLeft reads the input (Γ-prefix) block out of a full context, and takeLeft_backpropAllCtx (also in GraphData form) identifies the input block of the full backpropagation with the inputs-only backpropCtx — the missing lemma relating the runtime-facing backpropAllCtx to the proof-facing backpropCtx.
• Vectorization transport. The flattenCtx_* lemmas commute context vectorization with cast/snoc/unsnoc/add, so the TList-level graph semantics coincide with the Euclidean CtxVec semantics: evalVec_flattenCtx, jvpVec_flattenCtx, backpropVec_flattenCtx.
• The composed endpoints. backpropCtx_eq_adjoint_fderiv upgrades the algebraic backpropagation at ℝ to the Fréchet-adjoint characterization, and backwardDenseFrom_compileAux_adjoint_fderiv combines it with the runtime link: the tape model's dense reverse pass on a compiled graph, instantiated at α := ℝ, succeeds with the full backpropagation context, whose input prefix is exactly (fderiv ℝ eval x)† seed. The _at variants assume differentiability only at the actual execution point (GraphFDerivCorrectAt), covering graphs with non-smooth primitives (relu, abs, min/max, log, sqrt, …).

Throughout, "reverse pass" means the exact tape model: the Tape.backwardDenseFrom program of Runtime/Autograd instantiated at the exact carrier α := ℝ. Nothing in this file is a statement about the native Float evaluation or the CUDA execution path; relating those to the exact model is a separate (approximation) concern.

theorem Proofs.Autograd.dotList_eq_algebra_dotList {Γ : List Spec.Shape} (x y : TList Γ) : x.dotList y = Algebra.TList.dotList x y

The analytic context inner product (Spec.dot-based) agrees with the algebraic one (TensorAlgebra.dot-based) at ℝ.

Both recursions are the same sum of per-entry tensor dots; the entries agree by dot_eq_tensorAlgebra_dot.

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

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

theorem Proofs.Autograd.toVecT_addSpec {s : Spec.Shape} (a b : Spec.Tensor ℝ s) : toVecT (a.addSpec b) = toVecT a + toVecT b

Vectorization is additive: toVecT maps addSpec to vector addition.

theorem Proofs.Autograd.flattenCtx_add {Γ : List Spec.Shape} (u v : TList Γ) : 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 : TList Γ) (y : Spec.Tensor ℝ τ) : flattenCtx (xs.snoc y) = snocCtx (flattenCtx xs) (toVecT y)

flattenCtx maps TList.snoc to snocCtx.

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

flattenCtx maps TList.unsnoc to unsnocCtx.

theorem Proofs.Autograd.Node.forwardVec_flattenCtx {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) (x : TList Γ) : node.forwardVec (flattenCtx x) = toVecT (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 : TList Γ) : node.jvpVec (flattenCtx x) (flattenCtx dx) = toVecT (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 : TList Γ) (δ : Spec.Tensor ℝ τ) : node.vjpVec (flattenCtx x) (toVecT δ) = 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 : TList Γ) : g.evalVec (flattenCtx x) = flattenCtx (g.eval x)

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

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

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

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

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

def Proofs.Autograd.Node.toAlgebra {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) : Algebra.Node Unit Γ τ

Embed an analytic node as an algebraic node over ℝ with a trivial environment.

def Proofs.Autograd.Graph.toAlgebra {Γ ss : List Spec.Shape} : Graph Γ ss → Algebra.Graph Unit Γ ss

Embed an analytic graph as an algebraic graph over ℝ with a trivial environment.

def Proofs.Autograd.Algebra.Node.toReal {Δ : Type} {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Δ Γ τ) (d : Δ) : Autograd.Node Γ τ

Specialize an algebraic node at carrier ℝ and a fixed environment d : Δ to an analytic node. The adjointness law transports along dot_eq_tensorAlgebra_dot.

def Proofs.Autograd.Algebra.Graph.toReal {Δ : Type} {Γ ss : List Spec.Shape} : Graph Δ Γ ss → Δ → Autograd.Graph Γ ss

Specialize an algebraic graph at carrier ℝ and a fixed environment to an analytic graph.

@[simp]

theorem Proofs.Autograd.Algebra.Node.toAlgebra_toReal {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Autograd.Node Γ τ) (d : Unit) : node.toAlgebra.toReal d = node

The round trip through the algebraic model is the identity on analytic nodes.

@[simp]

theorem Proofs.Autograd.Algebra.Node.toReal_toAlgebra {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Unit Γ τ) : (node.toReal ()).toAlgebra = node

Specializing an algebraic node with a trivial environment and embedding it back is the identity.

@[simp]

theorem Proofs.Autograd.Algebra.Graph.toAlgebra_toReal {Γ ss : List Spec.Shape} (g : Autograd.Graph Γ ss) (d : Unit) : g.toAlgebra.toReal d = g

The round trip through the algebraic model is the identity on analytic graphs.

@[simp]

theorem Proofs.Autograd.Algebra.Graph.toReal_toAlgebra {Γ ss : List Spec.Shape} (g : Graph Unit Γ ss) : (g.toReal ()).toAlgebra = g

Specializing an algebraic graph with a trivial environment and embedding it back is the identity.

theorem Proofs.Autograd.Algebra.Graph.toReal_eval {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList ℝ Γ) (d : Δ) : (g.toReal d).eval x = g.eval x d

Specialization preserves evaluation.

theorem Proofs.Autograd.Algebra.Graph.toReal_jvpCtx {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x dx : TList ℝ Γ) (d : Δ) : (g.toReal d).jvpCtx x dx = g.jvpCtx x dx d

Specialization preserves the JVP.

theorem Proofs.Autograd.Algebra.Graph.toReal_backpropCtx {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList ℝ Γ) (d : Δ) (seed : TList ℝ (Γ ++ ss)) : (g.toReal d).backpropCtx x seed = g.backpropCtx x d seed

Specialization preserves the reverse pass.

def Proofs.Autograd.Algebra.TList.takeLeft {α : Type} {Γ ss : List Spec.Shape} : TList α (Γ ++ ss) → TList α Γ

Read the input (Γ-prefix) block out of a full context over Γ ++ ss.

theorem Proofs.Autograd.Algebra.TList.cast_cons {α : Type} {s : Spec.Shape} {ss₁ ss₂ : List Spec.Shape} (h : s :: ss₁ = s :: ss₂) (h' : ss₁ = ss₂) (x : Spec.Tensor α s) (xs : TList α ss₁) : cast h (cons x xs) = cons x (cast h' xs)

Push a cast along a cons cell.

theorem Proofs.Autograd.Algebra.TList.takeLeft_append_nil {α : Type} {Γ : List Spec.Shape} (w : TList α (Γ ++ [])) : w.takeLeft = cast ⋯ w

On a context with no intermediates, takeLeft is the cast along Γ ++ [] = Γ.

theorem Proofs.Autograd.Algebra.TList.takeLeft_cast_snoc {α : Type} {Γ ss : List Spec.Shape} {τ : Spec.Shape} (h : Γ ++ ss ++ [τ] = Γ ++ (ss ++ [τ])) (w : TList α (Γ ++ ss)) (y : Spec.Tensor α τ) : (cast h (w.snoc y)).takeLeft = w.takeLeft

takeLeft ignores a snoc-ed final block (after reassociating the context).

theorem Proofs.Autograd.Algebra.Graph.takeLeft_backpropAllCtx {α : Type} [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList α Γ) (d : Δ) (seed : TList α (Γ ++ ss)) : (g.backpropAllCtx x d seed).takeLeft = g.backpropCtx x d seed

The input (Γ-prefix) block of the full backpropagation is the inputs-only backpropagation.

This identifies the link-facing backpropAllCtx (which retains a cotangent for every value, mirroring the tape engine's dense reverse pass) with the proof-facing backpropCtx on the input block.

theorem Proofs.Autograd.Algebra.GraphData.takeLeft_backpropAllCtx {α : Type} [Add α] {Δ : Type} {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TList α Γ) (d : Δ) (seed : TList α (Γ ++ ss)) : (g.backpropAllCtx x d seed).takeLeft = g.backpropCtx x d seed

GraphData version of Graph.takeLeft_backpropAllCtx.

theorem Proofs.Autograd.Algebra.Graph.backpropCtx_eq_adjoint_fderiv {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (d : Δ) (hg : GraphFDerivCorrect (g.toReal d)) (x : TList ℝ Γ) (seed : TList ℝ (Γ ++ ss)) : flattenCtx (g.backpropCtx x d seed) = (ContinuousLinearMap.adjoint (fderiv ℝ (g.toReal d).evalVec (flattenCtx x))) (flattenCtx seed)

Analytic upgrade of the algebraic reverse pass. At carrier ℝ and a fixed environment, the inputs-only backpropagation computes the adjoint of the Fréchet derivative of the graph's (vectorized) forward evaluation.

theorem Proofs.Autograd.Algebra.Graph.backpropCtx_eq_adjoint_fderiv_at {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (d : Δ) (x : TList ℝ Γ) (hg : GraphFDerivCorrectAt (g.toReal d) (flattenCtx x)) (seed : TList ℝ (Γ ++ ss)) : flattenCtx (g.backpropCtx x d seed) = (ContinuousLinearMap.adjoint (fderiv ℝ (g.toReal d).evalVec (flattenCtx x))) (flattenCtx seed)

Pointwise variant of backpropCtx_eq_adjoint_fderiv: differentiability is assumed only at the values actually encountered, admitting non-smooth primitives away from their kinks.

theorem Proofs.Autograd.Algebra.Graph.toReal_evalVec {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (d : Δ) (x : TList ℝ Γ) : (g.toReal d).evalVec (flattenCtx x) = flattenCtx (g.eval x d)

The function differentiated in the endpoints is the graph's own forward evaluation.

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAux_adjoint_fderiv {Δ : Type} {Γ : List Spec.Shape} [DecidableEq Spec.Shape] {ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList ℝ Γ) (d0 : Δ) (seed : TList ℝ (Γ ++ ss)) (hg : GraphFDerivCorrect (g.toReal d0)) : (g.compileAux x d0).1.backwardDenseFrom seed.toAnyArray = Except.ok (g.backpropAllCtx x d0 seed).toAnyArray ∧ flattenCtx (g.backpropAllCtx x d0 seed).takeLeft = (ContinuousLinearMap.adjoint (fderiv ℝ (g.toReal d0).evalVec (flattenCtx x))) (flattenCtx seed)

Tape-model reverse pass = adjoint of the Fréchet derivative. Running the tape engine's dense reverse pass (Tape.backwardDenseFrom) on a compiled graph — the exact tape model instantiated at α := ℝ, not the native Float or CUDA execution path — succeeds and returns the full backpropagation context, whose input (Γ-prefix) block is exactly the adjoint of the Fréchet derivative of the graph's forward evaluation applied to the seed.

This composes the runtime link (backwardDenseFrom_compileAux_eq_backpropAllCtx) with the analytic upgrade above.

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAux_adjoint_fderiv_at {Δ : Type} {Γ : List Spec.Shape} [DecidableEq Spec.Shape] {ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList ℝ Γ) (d0 : Δ) (seed : TList ℝ (Γ ++ ss)) (hg : GraphFDerivCorrectAt (g.toReal d0) (flattenCtx x)) : (g.compileAux x d0).1.backwardDenseFrom seed.toAnyArray = Except.ok (g.backpropAllCtx x d0 seed).toAnyArray ∧ flattenCtx (g.backpropAllCtx x d0 seed).takeLeft = (ContinuousLinearMap.adjoint (fderiv ℝ (g.toReal d0).evalVec (flattenCtx x))) (flattenCtx seed)

Pointwise variant of backwardDenseFrom_compileAux_adjoint_fderiv.