proofs(autograd): connect the runtime link to the Fréchet-derivative model

The runtime link (Runtime/Link/BackwardGraph) proves the executable dense
reverse pass agrees with the algebraic model's backpropAllCtx over any
commutative semiring; the analytic tape model (Tape/Core/FDeriv) proves
reverse-mode accumulation computes the adjoint of the Fréchet derivative
of the forward evaluation over the reals. The two developments were
stated on different graph types with no formal connection between them.

New module NN/Proofs/Autograd/Runtime/Link/FDeriv.lean supplies it:

- Algebra.{Node,Graph}.toReal specialize the algebraic model at the real
  carrier and a fixed environment to the analytic model, and
  {Node,Graph}.toAlgebra embed the analytic model back as the Unit-
  environment 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).
- TList.takeLeft plus takeLeft_backpropAllCtx (Graph and GraphData
  forms) identify the input-prefix block of the full backpropagation
  with the inputs-only backpropCtx.
- flattenCtx transport lemmas commute context vectorization with
  cast/snoc/unsnoc/add, exhibiting evalVec/jvpVec/backpropVec as 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 executable
  dense reverse pass on a compiled graph returns the full
  backpropagation context, whose input prefix is (fderiv eval x)† seed.

The round-trip lemmas double as the correctness specification for a
possible follow-up that re-founds the analytic model as an abbreviation
of the algebraic one (as already done for TList).

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

Author: NicolasRouquette

NN/Proofs/Autograd/Runtime/Link.lean

@@ -11,6 +11,7 @@ public import NN.Proofs.Autograd.Runtime.Link.Invariants
 public import NN.Proofs.Autograd.Runtime.Link.Accumulation
 public import NN.Proofs.Autograd.Runtime.Link.BackwardGraph
 public import NN.Proofs.Autograd.Runtime.Link.BackwardGraphData
+public import NN.Proofs.Autograd.Runtime.Link.FDeriv
 
 /-!
 Runtime-to-tape autograd link proofs.