Autograd: connect the runtime link to the Fréchet-derivative model

[NicolasRouquette]

Why

The autograd proof stack currently has two disconnected halves:

• NN/Proofs/Autograd/Runtime/Link/* proves the tape engine's dense reverse pass (Tape.backwardDenseFrom) agrees with the algebraic model's backpropAllCtx, over any commutative semiring carrier and non-differentiable environment Δ.
• NN/Proofs/Autograd/Tape/Core/FDeriv.lean proves reverse-mode accumulation computes the adjoint of the Fréchet derivative of the forward evaluation, over ℝ.

They are stated on different graph types with no translation function and no lemma relating them, so neither result reaches the other's conclusion: the link theorem never mentions real derivatives, and the analytic theorem never touches Tape.backwardDenseFrom. Anyone using the exact tape model's gradients for sensitivity analysis or verification purposes has to trust the algebraic model's hand-written VJP fields rather than a calculus-level statement.

What

One new self-contained, additive-only module, NN/Proofs/Autograd/Runtime/Link/FDeriv.lean (plus its Link.lean aggregator import):

• Slice isomorphism. Algebra.{Node,Graph}.toReal specialize the algebraic model at α := ℝ and a fixed environment to the analytic model; {Node,Graph}.toAlgebra embed the analytic model back as the Δ := Unit slice; the round trip is the identity, so the analytic model is exactly the environment-free real slice of the algebraic one. Commutation lemmas cover all three semantics (eval, jvpCtx, backpropCtx).
• Input-prefix extraction. TList.takeLeft and takeLeft_backpropAllCtx (Graph and GraphData forms) identify the input block of the full backpropagation with the inputs-only backpropCtx — the missing lemma relating the two backpropagation forms the codebase keeps side by side.
• Vectorization transport. flattenCtx commutes with cast/snoc/unsnoc/add, exhibiting evalVec/jvpVec/backpropVec as exactly the flattenings of the TList semantics.
• Composed endpoints. backpropCtx_eq_adjoint_fderiv and backwardDenseFrom_compileAux_adjoint_fderiv (with pointwise _at variants for graphs containing non-smooth primitives): the tape model's dense reverse pass on a compiled graph, instantiated at α := ℝ, succeeds and returns the full backpropagation context, whose input prefix is exactly (fderiv ℝ eval x)† seed.

Scope. Every statement is about the exact tape model — Tape.backwardDenseFrom instantiated at the exact carrier α := ℝ. Nothing here is a claim about the native Float evaluation or the CUDA execution path; relating those to the exact model is a separate (approximation) concern.

All new declarations depend only on [propext, Classical.choice, Quot.sound].

Follow-up enabled

The round-trip lemmas double as a ready-made migration specification if you later want to re-found the analytic model as an abbreviation of the algebraic one at α := ℝ, Δ := Unit (as is already done for TList). Happy to take that on as a separate PR if wanted.

[Robertboy18]

Thanks, Nicolas. This is a useful bridge, and the proofs compile cleanly. One wording change before we merge: could you make it explicit that the endpoint is the exact tape model instantiated over ℝ, not the native Float or CUDA execution path? Phrases such as "executable dense reverse pass" and "runtime reverse pass" currently read more broadly than the theorem states. The theorem itself looks good.

[Robertboy18]

Thanks, Nicolas — the revised scope is clear now. This addresses my wording concern. I’ll wait for the current CI run to finish before merging.

[Robertboy18]

Thanks, Nicolas! This is merged now. The exact tape connection to Fréchet derivatives is a valuable addition, and I’m doing a final local pass to tighten the documentation around the two-way correspondence.