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

Two independent developments meet in this file.

• The runtime link (NN.Proofs.Autograd.Runtime.Link.BackwardGraph) 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 (NN.Proofs.Autograd.Tape.Core.FDeriv) 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. Both use TorchLean.TensorPack ℝ Γ for their contexts. This file connects their evaluation, JVP, and backpropagation semantics:

• 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 (from NN.Proofs.Autograd.Tape.Core.Soundness) 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. TensorPack.takeLeft reads the input (Γ-prefix) block out of a full context (it is the left half of TorchLean.TensorPack.split), and takeLeft_backpropAllCtx (for GraphData, and for Graph through toData) identifies the input block of the full backpropagation with the inputs-only backpropCtx.
• Vectorization transport. The flattenCtx_* lemmas of NN.Proofs.Autograd.Tape.Core.FDeriv commute context vectorization with cast/snoc/unsnoc/add, so the TensorPack-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_lowerGraphToTape_adjoint_fderiv combines it with the runtime link: the tape model's dense reverse pass on a lowered 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.

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 : TorchLean.TensorPack ℝ Γ) (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 : TorchLean.TensorPack ℝ Γ) (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 : TorchLean.TensorPack ℝ Γ) (d : Δ) (seed : TorchLean.TensorPack ℝ (Γ ++ ss)) : (g.toReal d).backpropCtx x seed = g.backpropCtx x d seed

Specialization preserves the reverse pass.

@[reducible, inline]

abbrev Proofs.Autograd.Algebra.TensorPack.takeLeft {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (xs : TorchLean.TensorPack α (Γ ++ ss)) : TorchLean.TensorPack α Γ

Read the input (Γ-prefix) block out of a full context over Γ ++ ss: the left half of the public TorchLean.TensorPack.split, under the name the link theorems use.

theorem Proofs.Autograd.Algebra.TensorPack.takeLeft_eq_split {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (xs : TorchLean.TensorPack α (Γ ++ ss)) : takeLeft xs = xs.split.1

The proof context's input projection is the public tensor-pack split.

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

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

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

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

theorem Proofs.Autograd.Algebra.GraphData.takeLeft_backpropAllCtx {α : Type} [TorchLean.Storage α] [Add α] {Δ : Type} {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TensorPack.takeLeft (g.backpropAllCtx x d seed) = 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.Graph.takeLeft_backpropAllCtx {α : Type} [TorchLean.Storage α] [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TensorPack.takeLeft (g.backpropAllCtx x d seed) = g.backpropCtx x d seed

Graph form of GraphData.takeLeft_backpropAllCtx: both backpropAllCtx and backpropCtx of a proof-carrying graph are the GraphData programs on g.toData.

theorem Proofs.Autograd.Algebra.Graph.backpropCtx_eq_adjoint_fderiv {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (d : Δ) (hg : GraphFDerivCorrect (g.toReal d)) (x : TorchLean.TensorPack ℝ Γ) (seed : TorchLean.TensorPack ℝ (Γ ++ 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 : TorchLean.TensorPack ℝ Γ) (hg : GraphFDerivCorrectAt (g.toReal d) (flattenCtx x)) (seed : TorchLean.TensorPack ℝ (Γ ++ 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 : TorchLean.TensorPack ℝ Γ) : (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_lowerGraphToTape_adjoint_fderiv {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack ℝ Γ) (d0 : Δ) (seed : TorchLean.TensorPack ℝ (Γ ++ ss)) (hg : GraphFDerivCorrect (g.toReal d0)) : (g.lowerGraphToTape x d0).1.backwardDenseFrom seed.toShapeErasedArray = Except.ok (g.backpropAllCtx x d0 seed).toShapeErasedArray ∧ flattenCtx (TensorPack.takeLeft (g.backpropAllCtx x d0 seed)) = (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 lowered 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_lowerGraphToTape_eq_backpropAllCtx) with the analytic upgrade above.

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphToTape_adjoint_fderiv_at {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack ℝ Γ) (d0 : Δ) (seed : TorchLean.TensorPack ℝ (Γ ++ ss)) (hg : GraphFDerivCorrectAt (g.toReal d0) (flattenCtx x)) : (g.lowerGraphToTape x d0).1.backwardDenseFrom seed.toShapeErasedArray = Except.ok (g.backpropAllCtx x d0 seed).toShapeErasedArray ∧ flattenCtx (TensorPack.takeLeft (g.backpropAllCtx x d0 seed)) = (ContinuousLinearMap.adjoint (fderiv ℝ (g.toReal d0).evalVec (flattenCtx x))) (flattenCtx seed)

Pointwise variant of backwardDenseFrom_lowerGraphToTape_adjoint_fderiv.