Lean: prove the R420 Fin661 COPY/scatter lifecycle

[chinmayarvind23]

Adds the actual R420 Fin 661 COPY/scatter lifecycle instance left open by #612. For the pinned retained-major slice (9 COPY, 568 ADD, 9 ERASE), Lean proves every original coordinate equals direct retained-centre XOR scatter, sources/helpers are preserved, and temporary register 660 finishes false independently of its incoming value. Restoration is stated only when that temporary starts false.

The new instance uses fresh finite bounds and literal R420 data. An external checker regenerates every centre, scatter row and ordered destination list from the pinned JSON; Lean then proves the membership loop agrees with those exported windows and that decoding preserves their order. The two generic modules are byte-exact copies from #590 and are freshly compiled with the two new modules. No historical Fin 730 object is reused.

Validation: all four modules compiled successfully with official Lean 4.21.0, and all 28 required axiom probes passed, using only propext and Quot.sound where needed. Eleven source-binding tests pass normally and with Python assertions disabled; they include data mutations with refreshed hashes and omissions of required modules, probes and source inputs. Builds ran offline in a restricted Docker container with read-only sources; no supplier scripts were executed. The package records the official distribution digest, source/runtime trust boundary and local validation evidence. No GitHub CI result is claimed.

Reproduce from the repository root with the official Linux Lean 4.21.0 distribution:

python3 research/r420-scatter-lifecycle/check.py \
  --lean /opt/lean-4.21.0-linux/bin/lean --build-dir /tmp/r420-lifecycle-build
cd research/r420-scatter-lifecycle
python3 -m unittest -v test_binding
python3 -O -m unittest -v test_binding

The build directory must be fresh. Expected: PASS 4 fresh modules, 28 standard-axiom probes, plus 11 passing tests per run. A separate compiled negative control replaced exact_lifecycle with sorry and refreshed its source hash; the checker rejected the resulting sorryAx dependency rather than accepting the compiler's successful exit.

This is a scalar Boolean proof for the historical R420 component: COPY overwrites, ADD uses XOR, and ERASE writes false. Physical COPY/ERASE legality, frame transport, A/C cleanup, D compensation and the complete/all-size multiplication theorem remain separate. The selected frontier and kappa are unchanged. #834 verifies expressions in #612's existing source package; this PR adds the previously absent lifecycle theorem.

Base: f567884aeb8851b6e794af1184119a3bfbe1e631. Generic proof source: #590 at 58690bdbb587f482569ba1bdf7bf61a5396b4768. R420 data, decoded payload and exporter are pinned in MANIFEST.json. Recent PRs were checked for overlap through #854. Prepared by Chinmay (@chinmayarvind23) with substantial OpenAI Codex assistance, adapting James Chang's generic/historical proofs. Credits and original notices for eumemic's R420 supplier and Dylan Crow / utcorvusvolat-dotcom's inherited exporter are preserved under Apache-2.0.