feat(autograd): reduce the TapeM surface to one lemma, and prove it

[NicolasRouquette]

The gap

The pure tape engine (Runtime.Autograd.Tape) is well covered by proofs. TapeM — the
StateT (Tape α) Result wrapper that users actually write eager programs in — has no proofs at
all: git grep -l TapeM on main finds the runtime definition, the training helpers, and three
test files, and nothing under NN/Proofs/. So a do-block has no route back to a statement about
the tape it built, and a proof about a program has to be written against a hand-threaded
Tape.<op> chain that is not the program.

The observation this rests on

Every TapeM wrapper that threads the tape is the same four lines:

def mul {α : Type} [Mul α] [DecidableEq Shape] {s : Shape}
  (aId bId : Nat) : TapeM α Nat := do
  let t ← get
  let (t', id) ← liftM (Tape.mul (t := t) (s := s) aId bId)
  set t'
  pure id

There are 31 of these, differing only in the pure op and its binders. This PR names the shape once:

def opM {γ : Type} (g : Tape α → Result (Tape α × γ)) : TapeM α γ := do
  let t ← get
  let (t', id) ← liftM (g t)
  set t'
  pure id

so each wrapper is definitionally opM at its own pure counterpart — TapeM.mul aId bId is
opM fun t => Tape.mul (t := t) aId bId. The existing wrappers are left exactly as they are; the
identity is real either way.

What the PR adds

NN/Runtime/Autograd/Engine/TapeM.lean gains TapeM.opM (20 lines, definition + docstring).

NN/Proofs/Autograd/Tape/Builder.lean (new) proves, all generic in the carrier α:

• opM_run_ok / opM_run_error — a pure op's outcome becomes the monadic run's outcome. The
  pair swaps: a pure op returns tape-then-value, run returns value-then-state.
• opM_run_inv — and back again.
• run_bind_inv — a successful run of m >>= f splits into its two successful stages. This is
  what peels a do-block one statement at a time.
• exec_inv — a successful exec is a successful run that returned something.
• run_leaf — stated separately, because leaf is total: its pure counterpart returns a bare pair
  rather than a Result.
• run_<op>_ok for all 31 tape-threading wrappers — add, sub, mul, div, scale, abs,
  sqrt, clamp, max, min, relu, linear, matmul, conv, convTranspose, maxPool,
  smoothMaxPool, avgPool, layerNorm, batchNorm, multiHeadAttention, mseLoss, sigmoid,
  tanh, softmaxLast, softplus, exp, log, inv, safeLog, sum.

Each member of the family is the proof term opM_run_ok with g supplied and nothing else — no
unfolding lemma in between:

theorem run_mul_ok {α : Type} [Mul α] [DecidableEq Shape] {s : Shape} (aId bId : Nat)
    {t t' : Tape α} {id : Nat}
    (h : Runtime.Autograd.Tape.mul (t := t) (s := s) aId bId = .ok (t', id)) :
    (TapeM.mul (s := s) aId bId).run t = .ok (id, t') :=
  opM_run_ok (g := fun tt => Runtime.Autograd.Tape.mul (t := tt) (s := s) aId bId) h

That is the property worth having: if one of these ever stops typechecking, its wrapper has stopped
being opM at its pure op. The family cannot drift into stating something weaker than the wrapper
does, because it is not stating anything separately.

TapeM.backwardScalar is deliberately outside the family — it reads the tape without writing one
back, so it is a different shape.

Axiom profile

The layer contributes nothing of its own. Verified, not assumed:

'Runtime.Autograd.TapeM.opM' does not depend on any axioms
'Proofs.Autograd.Builder.opM_run_ok' depends on axioms: [propext]
'Proofs.Autograd.Builder.opM_run_error' depends on axioms: [propext]
'Proofs.Autograd.Builder.opM_run_inv' depends on axioms: [propext]
'Proofs.Autograd.Builder.run_bind_inv' does not depend on any axioms
'Proofs.Autograd.Builder.exec_inv' does not depend on any axioms

Where a per-op lemma reports more, it is inherited from the op it names, not introduced here:

'Proofs.Autograd.Builder.run_mul_ok'  depends on axioms: [propext]
'Runtime.Autograd.Tape.mul'           depends on axioms: [propext]

'Proofs.Autograd.Builder.run_sum_ok'  depends on axioms: [propext, Quot.sound]
'Runtime.Autograd.Tape.sum'           depends on axioms: [propext, Quot.sound]

'Proofs.Autograd.Builder.run_conv_ok' depends on axioms: [propext, Classical.choice, Quot.sound]
'Runtime.Autograd.Tape.conv'          depends on axioms: [propext, Classical.choice, Quot.sound]

The test does both things to one program

NN/Tests/Runtime/Rationals/TapeBuilderTest.lean takes a user-style block over ℚ,

def prog : TapeM ℚ Nat := do
  let a ← TapeM.leaf (s := [2]) xa
  let b ← TapeM.leaf (s := [2]) xb
  let m ← TapeM.mul (s := [2]) a b
  TapeM.scale (s := [2]) m c

runs it and checks the value (4 * ([2,3] * [5,7]) is [40, 84]), and proves — from nothing but
"the block executed successfully" — the pure-Tape fact behind each of its four statements:

theorem prog_peel {t t' : Tape ℚ} (h : TapeM.exec t prog = .ok t') :
    ∃ (t1 t2 t3 : Tape ℚ) (ida idb idm ids : Nat),
      Tape.leaf (t := t) xa = (t1, ida)
      ∧ Tape.leaf (t := t1) xb = (t2, idb)
      ∧ Tape.mul (t := t2) (s := [2]) ida idb = .ok (t3, idm)
      ∧ Tape.scale (t := t3) (s := [2]) idm c = .ok (t', ids)

The proof is the peel and nothing else: exec_inv, then run_bind_inv once per statement, then
run_leaf or opM_run_inv at each op.

Tape.empty has no native implementation available to the elaborator, so the numeric half cannot
be forced by a compile-time #guard; it runs under nn_tests_suite, which is where the note in the
file points.

Checks run

lake build                        Build completed successfully (4139 jobs).   [no warnings]
lake exe nn_tests_suite           tape_builder_test (Rat): OK
                                  == TorchLean: all curated tests passed ==
python3 scripts/checks/repo_lint.py   OK: no issues found.

PR checklist

• lake build succeeds — 4139 jobs, no errors and no warnings.
• Tests added — TapeBuilderTest, wired into Tests.Runtime.Rationals.Suite.
• Docstrings on every new definition and theorem; module docstring on the new file.
• Trust boundaries — none crossed; this is proof-layer only, no native or FFI surface.
• No new sorry in NN/.
• No new axioms.

Optional follow-up, not in this PR

The 31 wrappers could have their bodies replaced by opM <their g>, which would make
the identity manifest instead of incidental. It is defeq either way,
so the lemmas here hold unchanged.

Kept out so this PR stays purely additive; happy to do it in a second PR if preferred.

---

Notes for Nicolas (not part of the PR body)

• Branch exists locally only. git push -u origin tapem-run-lemmas, then open the PR against
  lean-dojo/TorchLean:main.
• AI_USAGE.md upstream discloses AI assistance at the repository level; nothing in this PR needs
  a per-PR disclosure beyond whatever you normally add.
• The working tree was on cuda-arch-target before this; tapem-run-lemmas was cut from
  upstream/main, so it carries none of the CUDA work.
• PKC's examples/.../TapeMBridge.lean is the file this generalizes. If this merges, that file
  shrinks to the demo plus the eager-provenance endpoint — its opM, the three opM_run_* lemmas,
  run_bind_inv, exec_inv and its 13 per-op lemmas all come from upstream instead, and they
  arrive generic in the carrier rather than fixed at ℝ.