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 none 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 TapeM.Internal.record applied to its pure
counterpart:

def mul {α : Type} [TorchLean.Storage α] [Mul α] {s : Shape}
  (aId bId : Nat) : TapeM α Nat :=
  Internal.record fun t => Tape.mul (t := t) (s := s) aId bId

There are 33 of these, differing only in the pure op and its binders. So the whole surface
reduces through one lemma about Internal.record, and nothing in TapeM.lean needs to change.

What the PR adds

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

• record_run_ok / record_run_error: a pure op's outcome becomes the monadic run's
  outcome. The pair swaps: a pure op returns tape-then-id, run returns value-then-state.
• record_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.
• run_leaf: stated separately, because leaf is total; its pure counterpart returns a bare
  pair rather than a Result. On current main it is rfl.
• run_<op>_ok for all 33 tape-threading wrappers: add, sub, mul, div, scale, abs,
  sqrt, clamp, max, min, relu, linear, matmul, conv, convTranspose,
  maxPool, smoothMaxPool, avgPool, layerNorm, batchNorm, attention, mseLoss,
  sigmoid, tanh, softmaxLast, softplus, exp, sin, cos, log, inv, safeLog,
  sum.

Each member of the family is the proof term record_run_ok with op supplied and nothing
else:

theorem run_mul_ok [Mul α] {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') :=
  record_run_ok (op := 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 Internal.record at its pure op. The family cannot drift into stating something
weaker than the wrapper does, because it is not stating anything separately. The binders are
copied from each wrapper, so every lemma can be applied exactly where its wrapper can be called.

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

Axiom profile

Checked with #print axioms on 465fe109: every lemma in the file, run_bind_inv and
run_leaf included, reports [propext, Classical.choice, Quot.sound], which is exactly what
Runtime.Autograd.TapeM.Internal.record and the Tape ops themselves report on this tree. The
layer introduces nothing the runtime definitions it reasons about do not already carry.

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 ran", the pure-Tape fact behind each of its four statements:

theorem prog_peel {t t' : Tape ℚ} {ids : Nat} (h : prog.run t = .ok (ids, t')) :
    ∃ (t1 t2 t3 : Tape ℚ) (ida idb idm : 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: run_bind_inv once per statement, then run_leaf or
record_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.

Checks run

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

PR checklist

• Builds with no errors or 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; proof layer only, no native or FFI surface.
• No new sorry in NN/.
• No new axioms.

[Robertboy18]

Hey Nicolas, can you rebase this onto the latest main?

[Robertboy18]

Thanks! These TapeM proofs still look useful. Could you update this against current main and build around the existing TapeM.Internal.record helper? We consolidated the runtime wrappers during cleanup, so the proof layer should reuse that.

[NicolasRouquette]

Rebased onto current main (b062b9a3) and built around TapeM.Internal.record, as asked.

What changed in the port:

• TapeM.lean is no longer touched. The lemmas are stated on the existing
  TapeM.Internal.record, which is the helper the 33 op wrappers already go through, so the PR
  is now additive only: the proof module, the test, and two import lines.
• exec_inv is gone because TapeM.exec no longer exists on main; the test's theorem now
  takes prog.run t = .ok (ids, t') directly.
• The per-op family follows the current wrapper surface: multiHeadAttention became
  attention, and sin / cos are new members. 33 lemmas, binders copied from each wrapper.

Checks on 465fe109:

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

The PR description is updated to match.

[Robertboy18]

Hey Nicolas, thanks for this! The proof bridge compiles locally, the core lemma axiom checks contain only the standard Lean axioms, and the rational tape-builder example passes. Merging this one.