Runtime-to-tape autograd link proofs.

These modules connect executable runtime graph bookkeeping to the proof-oriented autograd tape semantics used by correctness theorems.

BackwardGraph and FDeriv are about the proved sweep Tape.backwardDenseFrom. BackwardDense and BackwardDenseGraph extend the same results to the sweep the eager trainer actually executes, Tape.backwardDenseAll, which skips nodes that never receive a cotangent.