From 4e31c0d816432435de2ca3965d33efb3ea6602a4 Mon Sep 17 00:00:00 2001
From: chinmayarvind23 <chinmayarvind23@gmail.com>
Date: Tue, 13 Oct 2026 02:44:55 -0500
Subject: [PATCH] formal: prove R420 Fin661 copy scatter lifecycle

---
 .../BitCopyScatterWindow.lean                 | 191 +++++++++++++++++
 .../BitXorTargetTranslation.lean              | 139 ++++++++++++
 research/r420-scatter-lifecycle/LICENSE       | 201 ++++++++++++++++++
 research/r420-scatter-lifecycle/MANIFEST.json |  98 +++++++++
 .../R420ScatterData.lean                      | 147 +++++++++++++
 .../R420ScatterLifecycle.lean                 | 181 ++++++++++++++++
 .../r420-scatter-lifecycle/R420_NOTICE.md     |  64 ++++++
 research/r420-scatter-lifecycle/README.md     |  95 +++++++++
 .../r420-scatter-lifecycle/SUPPLIER_NOTICE.md |  69 ++++++
 research/r420-scatter-lifecycle/VALIDATION.md |  46 ++++
 research/r420-scatter-lifecycle/check.py      | 200 +++++++++++++++++
 .../r420-scatter-lifecycle/test_binding.py    | 105 +++++++++
 .../test_kernel_rejection.py                  |  54 +++++
 13 files changed, 1590 insertions(+)
 create mode 100644 research/r420-scatter-lifecycle/BitCopyScatterWindow.lean
 create mode 100644 research/r420-scatter-lifecycle/BitXorTargetTranslation.lean
 create mode 100644 research/r420-scatter-lifecycle/LICENSE
 create mode 100644 research/r420-scatter-lifecycle/MANIFEST.json
 create mode 100644 research/r420-scatter-lifecycle/R420ScatterData.lean
 create mode 100644 research/r420-scatter-lifecycle/R420ScatterLifecycle.lean
 create mode 100644 research/r420-scatter-lifecycle/R420_NOTICE.md
 create mode 100644 research/r420-scatter-lifecycle/README.md
 create mode 100644 research/r420-scatter-lifecycle/SUPPLIER_NOTICE.md
 create mode 100644 research/r420-scatter-lifecycle/VALIDATION.md
 create mode 100644 research/r420-scatter-lifecycle/check.py
 create mode 100644 research/r420-scatter-lifecycle/test_binding.py
 create mode 100644 research/r420-scatter-lifecycle/test_kernel_rejection.py

diff --git a/research/r420-scatter-lifecycle/BitCopyScatterWindow.lean b/research/r420-scatter-lifecycle/BitCopyScatterWindow.lean
new file mode 100644
index 0000000000..50726d30f4
--- /dev/null
+++ b/research/r420-scatter-lifecycle/BitCopyScatterWindow.lean
@@ -0,0 +1,191 @@
+import BitXorTargetTranslation
+
+/-! Boolean scalar projection of a retained-centre COPY/ADD/ERASE window.
+COPY overwrites the temporary and ERASE writes false. No physical allocation,
+frame transport, or restoration of an arbitrary incoming temporary is asserted.
+The overwrite/clear statement shapes parallel the accepted F19 scalar adapter;
+its rational Module instance is not imported or treated as Boolean semantics. -/
+namespace CurrentMain.BitCopyScatter
+set_option Elab.async false
+variable {Reg : Type} [DecidableEq Reg]
+abbrev State (Reg : Type) := Reg → Bool
+
+def copy (temp centre : Reg) (s : State Reg) : State Reg :=
+  fun r => if r = temp then s centre else s r
+
+def clear (temp : Reg) (s : State Reg) : State Reg :=
+  fun r => if r = temp then false else s r
+
+/-- Ordered destination loop, using the accepted scalar XOR ADD. -/
+def adds (src : Reg) : List Reg → State Reg → State Reg
+  | [], s => s
+  | d :: ds, s => adds src ds (BitXor.single d src s)
+
+def window (temp centre : Reg) (ds : List Reg) (s : State Reg) : State Reg :=
+  clear temp (adds temp ds (copy temp centre s))
+
+structure Window (Reg : Type) where
+  centre : Reg
+  targets : List Reg
+
+def WellFormed (temp : Reg) (w : Window Reg) : Prop :=
+  w.centre ≠ temp ∧ ∀ d ∈ w.targets, d ≠ temp ∧ d ≠ w.centre
+
+def runWindows (temp : Reg) : List (Window Reg) → State Reg → State Reg
+  | [], s => s
+  | w :: ws, s => runWindows temp ws (window temp w.centre w.targets s)
+
+def directWindows : List (Window Reg) → State Reg → State Reg
+  | [], s => s
+  | w :: ws, s => directWindows ws (adds w.centre w.targets s)
+
+theorem copy_at_temp (temp centre : Reg) (s : State Reg) :
+    copy temp centre s temp = s centre := by simp [copy]
+
+theorem clear_at_temp (temp : Reg) (s : State Reg) :
+    clear temp s temp = false := by simp [clear]
+
+private theorem single_copy (temp centre dst : Reg)
+    (hdt : dst ≠ temp) (hdc : dst ≠ centre) (s : State Reg) :
+    BitXor.single dst temp (copy temp centre s) =
+      copy temp centre (BitXor.single dst centre s) := by
+  funext r
+  by_cases hr : r = temp
+  · subst r
+    simp [copy, BitXor.single, Ne.symm hdt, Ne.symm hdc]
+  · simp [copy, BitXor.single, hr]
+
+private theorem adds_copy (temp centre : Reg) (ds : List Reg) :
+    (∀ d ∈ ds, d ≠ temp ∧ d ≠ centre) → ∀ s,
+    adds temp ds (copy temp centre s) = copy temp centre (adds centre ds s) := by
+  induction ds with
+  | nil => intro h s; rfl
+  | cons d ds ih =>
+    intro h s
+    change adds temp ds (BitXor.single d temp (copy temp centre s)) =
+      copy temp centre (adds centre ds (BitXor.single d centre s))
+    rw [single_copy temp centre d (h d List.mem_cons_self).1
+      (h d List.mem_cons_self).2 s]
+    exact ih (fun r hr => h r (List.mem_cons_of_mem d hr)) (BitXor.single d centre s)
+
+private theorem clear_copy (temp centre : Reg) (s : State Reg) :
+    clear temp (copy temp centre s) = clear temp s := by
+  funext r
+  by_cases hr : r = temp <;> simp [clear, copy, hr]
+
+private theorem clear_clear (temp : Reg) (s : State Reg) :
+    clear temp (clear temp s) = clear temp s := by
+  funext r
+  by_cases hr : r = temp <;> simp [clear, hr]
+
+theorem window_eq_clear_direct (temp centre : Reg) (ds : List Reg)
+    (h : ∀ d ∈ ds, d ≠ temp ∧ d ≠ centre) (s : State Reg) :
+    window temp centre ds s = clear temp (adds centre ds s) := by
+  unfold window
+  rw [adds_copy temp centre ds h s, clear_copy]
+
+private theorem single_clear (temp src dst : Reg)
+    (hst : src ≠ temp) (hdt : dst ≠ temp) (s : State Reg) :
+    BitXor.single dst src (clear temp s) = clear temp (BitXor.single dst src s) := by
+  funext r
+  by_cases hr : r = temp
+  · subst r
+    simp [clear, BitXor.single, Ne.symm hdt]
+  · simp [clear, BitXor.single, hr, hst]
+
+private theorem adds_clear (temp src : Reg) (ds : List Reg) (hst : src ≠ temp) :
+    (∀ d ∈ ds, d ≠ temp) → ∀ s,
+    adds src ds (clear temp s) = clear temp (adds src ds s) := by
+  induction ds with
+  | nil => intro h s; rfl
+  | cons d ds ih =>
+    intro h s
+    change adds src ds (BitXor.single d src (clear temp s)) =
+      clear temp (adds src ds (BitXor.single d src s))
+    rw [single_clear temp src d hst (h d List.mem_cons_self) s]
+    exact ih (fun r hr => h r (List.mem_cons_of_mem d hr)) (BitXor.single d src s)
+
+private theorem copy_clear_input (temp centre : Reg) (hct : centre ≠ temp)
+    (s : State Reg) : copy temp centre (clear temp s) = copy temp centre s := by
+  funext r
+  by_cases hr : r = temp <;> simp [copy, clear, hr, hct]
+
+private theorem runWindows_clear (temp : Reg) (ws : List (Window Reg)) :
+    (∀ w ∈ ws, WellFormed temp w) → ∀ s,
+    runWindows temp ws (clear temp s) = clear temp (directWindows ws s) := by
+  induction ws with
+  | nil => intro h s; rfl
+  | cons w ws ih =>
+    intro h s
+    have hw := h w List.mem_cons_self
+    change runWindows temp ws (window temp w.centre w.targets (clear temp s)) =
+      clear temp (directWindows ws (adds w.centre w.targets s))
+    rw [window_eq_clear_direct temp w.centre w.targets hw.2,
+      adds_clear temp w.centre w.targets hw.1 (fun d hd => (hw.2 d hd).1),
+      clear_clear]
+    exact ih (fun q hq => h q (List.mem_cons_of_mem w hq)) (adds w.centre w.targets s)
+
+/-- Nonempty copy windows dispose of the incoming temporary and end it at zero.
+All other coordinates agree with the direct retained-centre XOR word. -/
+theorem runWindows_eq_clear_direct (temp : Reg) (ws : List (Window Reg))
+    (hne : ws ≠ []) (h : ∀ w ∈ ws, WellFormed temp w) (s : State Reg) :
+    runWindows temp ws s = clear temp (directWindows ws s) := by
+  cases ws with
+  | nil => exact False.elim (hne rfl)
+  | cons w ws =>
+    have hw := h w List.mem_cons_self
+    calc
+      runWindows temp (w :: ws) s = runWindows temp (w :: ws) (clear temp s) := by
+        change runWindows temp ws (window temp w.centre w.targets s) =
+          runWindows temp ws (window temp w.centre w.targets (clear temp s))
+        simp only [window, copy_clear_input temp w.centre hw.1 s]
+      _ = clear temp (directWindows (w :: ws) s) := runWindows_clear temp (w :: ws) h s
+
+private theorem adds_untouched (src : Reg) (ds : List Reg) :
+    ∀ s r, r ∉ ds → adds src ds s r = s r := by
+  induction ds with
+  | nil => intro s r h; rfl
+  | cons d ds ih =>
+    intro s r h
+    have hrd : r ≠ d := fun he => h (by simp [he])
+    have hrs : r ∉ ds := fun hr => h (List.mem_cons_of_mem d hr)
+    change adds src ds (BitXor.single d src s) r = s r
+    rw [ih (BitXor.single d src s) r hrs]
+    simp [BitXor.single, hrd]
+
+theorem directWindows_untouched (ws : List (Window Reg)) :
+    ∀ s r, (∀ w ∈ ws, r ∉ w.targets) → directWindows ws s r = s r := by
+  induction ws with
+  | nil => intro s r h; rfl
+  | cons w ws ih =>
+    intro s r h
+    change directWindows ws (adds w.centre w.targets s) r = s r
+    rw [ih (adds w.centre w.targets s) r (fun q hq => h q (List.mem_cons_of_mem w hq))]
+    exact adds_untouched w.centre w.targets s r (h w List.mem_cons_self)
+
+/-- Equality away from the disposable slot suffices, even if the two incoming
+slots differ. This is loss of the temporary's old value, not its restoration. -/
+theorem runWindows_independent_of_temp (temp : Reg) (ws : List (Window Reg))
+    (hne : ws ≠ []) (h : ∀ w ∈ ws, WellFormed temp w)
+    (s t : State Reg) (hst : ∀ r, r ≠ temp → s r = t r) :
+    runWindows temp ws s = runWindows temp ws t := by
+  cases ws with
+  | nil => exact False.elim (hne rfl)
+  | cons w ws =>
+    have hct := (h w List.mem_cons_self).1
+    have hc : copy temp w.centre s = copy temp w.centre t := by
+      funext r
+      by_cases hr : r = temp
+      · simp [copy, hr, hst w.centre hct]
+      · simp [copy, hr, hst r hr]
+    change runWindows temp ws (window temp w.centre w.targets s) =
+      runWindows temp ws (window temp w.centre w.targets t)
+    simp only [window, hc]
+
+end CurrentMain.BitCopyScatter
+#print axioms CurrentMain.BitCopyScatter.copy_at_temp
+#print axioms CurrentMain.BitCopyScatter.clear_at_temp
+#print axioms CurrentMain.BitCopyScatter.window_eq_clear_direct
+#print axioms CurrentMain.BitCopyScatter.runWindows_eq_clear_direct
+#print axioms CurrentMain.BitCopyScatter.directWindows_untouched
+#print axioms CurrentMain.BitCopyScatter.runWindows_independent_of_temp
diff --git a/research/r420-scatter-lifecycle/BitXorTargetTranslation.lean b/research/r420-scatter-lifecycle/BitXorTargetTranslation.lean
new file mode 100644
index 0000000000..1638dbbaa3
--- /dev/null
+++ b/research/r420-scatter-lifecycle/BitXorTargetTranslation.lean
@@ -0,0 +1,139 @@
+import Init
+
+/-! Raw Boolean XOR semantics for an ordered multi-source gate. Frame metadata
+is retained but has no scalar action here; physical frame transport is separate.
+This small structural adapter reuses core Bool XOR laws. It does not interpret
+COPY/ERASE or assert any source-specific operator or geometry. -/
+namespace CurrentMain.BitXor
+set_option Elab.async false
+
+structure Gate (Reg : Type) where
+  frame : Nat
+  dst : Reg
+  sources : List Reg
+
+abbrev State (Reg : Type) := Reg → Bool
+variable {Reg : Type} [DecidableEq Reg]
+
+/-- One actual XOR ADD, preserving every other register. -/
+def single (dst src : Reg) (s : State Reg) : State Reg :=
+  fun r => if r = dst then s r ^^ s src else s r
+
+/-- Operand order matches the source checker's `for src in srcs` loop. -/
+def sourcesRun (dst : Reg) : List Reg → State Reg → State Reg
+  | [], s => s
+  | src :: rest, s => sourcesRun dst rest (single dst src s)
+
+def step (g : Gate Reg) (s : State Reg) : State Reg :=
+  sourcesRun g.dst g.sources s
+
+theorem sourcesRun_untouched (dst : Reg) (rs : List Reg) :
+    ∀ s r, r ≠ dst → sourcesRun dst rs s r = s r := by
+  induction rs with
+  | nil => intro s r hr; rfl
+  | cons src rs ih =>
+    intro s r hr
+    change sourcesRun dst rs (single dst src s) r = s r
+    rw [ih (single dst src s) r hr]
+    simp [single, hr]
+
+def run : List (Gate Reg) → State Reg → State Reg
+  | [], s => s
+  | g :: gs, s => run gs (step g s)
+
+variable (target : Reg → Prop) [DecidablePred target]
+
+def shift (s delta : State Reg) : State Reg :=
+  fun r => if target r then s r ^^ delta r else s r
+
+def eraseTargets (s : State Reg) : State Reg :=
+  fun r => if target r then false else s r
+
+theorem single_shift (dst src : Reg) (hsrc : ¬ target src)
+    (s delta : State Reg) :
+    single dst src (shift target s delta) =
+      shift target (single dst src s) delta := by
+  funext r
+  by_cases hd : r = dst
+  · subst r
+    by_cases ht : target dst <;>
+      simp [single, shift, ht, hsrc, Bool.xor_right_comm]
+    exact Bool.xor_comm (delta dst) (s src)
+  · by_cases ht : target r <;>
+      simp [single, shift, hd, ht, hsrc, Bool.xor_right_comm]
+
+theorem sourcesRun_shift (dst : Reg) (rs : List Reg) :
+    (∀ r ∈ rs, ¬ target r) → ∀ s delta,
+    sourcesRun dst rs (shift target s delta) =
+      shift target (sourcesRun dst rs s) delta := by
+  induction rs with
+  | nil => intro h s delta; rfl
+  | cons src rs ih =>
+    intro h s delta
+    have hs : ¬ target src := h src List.mem_cons_self
+    have ht : ∀ r ∈ rs, ¬ target r := fun r hr => h r (List.mem_cons_of_mem src hr)
+    change sourcesRun dst rs (single dst src (shift target s delta)) = _
+    rw [single_shift target dst src hs s delta]
+    exact ih ht (single dst src s) delta
+
+theorem step_shift (g : Gate Reg) (h : ∀ r ∈ g.sources, ¬ target r)
+    (s delta : State Reg) :
+    step g (shift target s delta) = shift target (step g s) delta :=
+  sourcesRun_shift target g.dst g.sources h s delta
+
+theorem run_shift (gs : List (Gate Reg)) :
+    (∀ g ∈ gs, ∀ r ∈ g.sources, ¬ target r) → ∀ s delta,
+    run gs (shift target s delta) = shift target (run gs s) delta := by
+  induction gs with
+  | nil => intro h s delta; rfl
+  | cons g gs ih =>
+    intro h s delta
+    change run gs (step g (shift target s delta)) =
+      shift target (run gs (step g s)) delta
+    rw [step_shift target g (h g List.mem_cons_self) s delta]
+    exact ih (fun q hq => h q (List.mem_cons_of_mem g hq)) (step g s) delta
+
+theorem run_off_target (gs : List (Gate Reg)) :
+    (∀ g ∈ gs, target g.dst) → ∀ s r, ¬ target r → run gs s r = s r := by
+  induction gs with
+  | nil => intro h s r hr; rfl
+  | cons g gs ih =>
+    intro h s r hr
+    have hne : r ≠ g.dst := by
+      intro he
+      apply hr
+      simpa [he] using h g List.mem_cons_self
+    change run gs (step g s) r = s r
+    rw [ih (fun q hq => h q (List.mem_cons_of_mem g hq)) (step g s) r hr]
+    exact sourcesRun_untouched g.dst g.sources s r hne
+
+theorem erase_shift_self (s : State Reg) :
+    shift target (eraseTargets target s) s = s := by
+  funext r
+  by_cases hr : target r <;> simp [shift, eraseTargets, hr]
+
+theorem target_identity (gs : List (Gate Reg))
+    (h : ∀ g ∈ gs, ∀ r ∈ g.sources, ¬ target r)
+    (s : State Reg) (r : Reg) (hr : target r) :
+    run gs s r = (s r ^^ run gs (eraseTargets target s) r) := by
+  calc
+    run gs s r = run gs (shift target (eraseTargets target s) s) r := by
+      rw [erase_shift_self]
+    _ = shift target (run gs (eraseTargets target s)) s r :=
+      congrFun (run_shift target gs h (eraseTargets target s) s) r
+    _ = (s r ^^ run gs (eraseTargets target s) r) := by
+      simp [shift, hr, Bool.xor_comm]
+
+theorem erased_eq_of_agree_off_target (s t : State Reg)
+    (h : ∀ r, ¬ target r → s r = t r) :
+    eraseTargets target s = eraseTargets target t := by
+  funext r
+  by_cases hr : target r
+  · simp [eraseTargets, hr]
+  · simp [eraseTargets, hr, h r hr]
+
+end CurrentMain.BitXor
+#print axioms CurrentMain.BitXor.run_shift
+#print axioms CurrentMain.BitXor.run_off_target
+#print axioms CurrentMain.BitXor.target_identity
+#print axioms CurrentMain.BitXor.erased_eq_of_agree_off_target
diff --git a/research/r420-scatter-lifecycle/LICENSE b/research/r420-scatter-lifecycle/LICENSE
new file mode 100644
index 0000000000..261eeb9e9f
--- /dev/null
+++ b/research/r420-scatter-lifecycle/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/research/r420-scatter-lifecycle/MANIFEST.json b/research/r420-scatter-lifecycle/MANIFEST.json
new file mode 100644
index 0000000000..c759b02f22
--- /dev/null
+++ b/research/r420-scatter-lifecycle/MANIFEST.json
@@ -0,0 +1,98 @@
+{
+  "format": "r420-scatter-lifecycle-v1",
+  "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631",
+  "word": "research/e8-bit-r420/data/bitE8mut-r420.json.gz",
+  "decoded_word_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2",
+  "core_manifest": "research/lean-current-r420-boundary-interfaces/OFFICIAL_CORE_MANIFEST.json",
+  "repository_inputs": [
+    {
+      "path": "research/e8-bit-r420/data/bitE8mut-r420.json.gz",
+      "sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784"
+    },
+    {
+      "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py",
+      "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3"
+    },
+    {
+      "path": "research/lean-current-r420-boundary-interfaces/OFFICIAL_CORE_MANIFEST.json",
+      "sha256": "2c27354193fc7b11079b61116ab8e9c80485903845bda48ddf3c66057fed2cb1"
+    }
+  ],
+  "predecessor": {
+    "pr": 590,
+    "head": "58690bdbb587f482569ba1bdf7bf61a5396b4768",
+    "byte_exact_files": [
+      "BitXorTargetTranslation.lean",
+      "BitCopyScatterWindow.lean"
+    ],
+    "adapted_from": "SelectedBitCarrierScatterLifecycle.lean",
+    "adapted_source_sha256": "754c8278cdb41dbff984faae2b1e7acaba611c4473adf5b7436c9d95c5564f3a"
+  },
+  "modules": [
+    {
+      "name": "BitXorTargetTranslation",
+      "sha256": "149a88cfbb2a76a755b1cb697f1c27ab7cc8d61b1cdb190f8affdb5c5f758873",
+      "imports": [
+        "Init"
+      ],
+      "probes": [
+        "CurrentMain.BitXor.run_shift",
+        "CurrentMain.BitXor.run_off_target",
+        "CurrentMain.BitXor.target_identity",
+        "CurrentMain.BitXor.erased_eq_of_agree_off_target"
+      ]
+    },
+    {
+      "name": "BitCopyScatterWindow",
+      "sha256": "b289ca173b33e5af27bf829f17de6ab739f959cb07c1028d39ebcdde5c8c90dd",
+      "imports": [
+        "BitXorTargetTranslation"
+      ],
+      "probes": [
+        "CurrentMain.BitCopyScatter.copy_at_temp",
+        "CurrentMain.BitCopyScatter.clear_at_temp",
+        "CurrentMain.BitCopyScatter.window_eq_clear_direct",
+        "CurrentMain.BitCopyScatter.runWindows_eq_clear_direct",
+        "CurrentMain.BitCopyScatter.directWindows_untouched",
+        "CurrentMain.BitCopyScatter.runWindows_independent_of_temp"
+      ]
+    },
+    {
+      "name": "R420ScatterData",
+      "sha256": "bec9b10d43674b4e10ae986d09ba06e4bf4f130eb939fa4cc65ac1f8edb0d800",
+      "imports": [
+        "Init"
+      ],
+      "probes": [
+        "CurrentMain.R420ScatterData.source_shape"
+      ]
+    },
+    {
+      "name": "R420ScatterLifecycle",
+      "sha256": "c79b756afe8e74e5b3b0d4df9e7fdbf401149c69c4c20154ed86d19b8fae3f65",
+      "imports": [
+        "R420ScatterData",
+        "BitCopyScatterWindow"
+      ],
+      "probes": [
+        "CurrentMain.R420ScatterLifecycle.original_excludes_temp",
+        "CurrentMain.R420ScatterLifecycle.exporter_window_binding",
+        "CurrentMain.R420ScatterLifecycle.raw_shape",
+        "CurrentMain.R420ScatterLifecycle.raw_domains",
+        "CurrentMain.R420ScatterLifecycle.source_rows_no_duplicates",
+        "CurrentMain.R420ScatterLifecycle.decode_roundtrip",
+        "CurrentMain.R420ScatterLifecycle.ordered_window_binding",
+        "CurrentMain.R420ScatterLifecycle.decoded_bounds",
+        "CurrentMain.R420ScatterLifecycle.windows_well_formed",
+        "CurrentMain.R420ScatterLifecycle.windows_nonempty",
+        "CurrentMain.R420ScatterLifecycle.exact_lifecycle",
+        "CurrentMain.R420ScatterLifecycle.final_temp_zero",
+        "CurrentMain.R420ScatterLifecycle.original_coordinate",
+        "CurrentMain.R420ScatterLifecycle.original_registers",
+        "CurrentMain.R420ScatterLifecycle.sources_helpers_preserved",
+        "CurrentMain.R420ScatterLifecycle.incoming_temp_independent",
+        "CurrentMain.R420ScatterLifecycle.clean_temp_restored"
+      ]
+    }
+  ]
+}
diff --git a/research/r420-scatter-lifecycle/R420ScatterData.lean b/research/r420-scatter-lifecycle/R420ScatterData.lean
new file mode 100644
index 0000000000..a3048431f8
--- /dev/null
+++ b/research/r420-scatter-lifecycle/R420ScatterData.lean
@@ -0,0 +1,147 @@
+import Init
+
+/-! Literal projection of the pinned PR543 R420 word. Generated by check.py's
+render_data; checked against the source before every build. Supplier:
+eumemic, with substantial Anthropic Claude assistance; Apache-2.0. -/
+namespace CurrentMain.R420ScatterData
+set_option Elab.async false
+def v : Nat := 120
+def R : Nat := 420
+def ret : List Nat := [603, 568, 597, 583, 569, 604, 616, 596, 598]
+def scatter : List (List Nat) := [[0, 1],
+  [0, 2],
+  [0, 3],
+  [0, 1, 2, 3],
+  [0, 4],
+  [0, 1, 2, 4],
+  [0, 1, 3, 4],
+  [0, 2, 3, 4],
+  [0, 5],
+  [0, 2, 3, 4, 5],
+  [0, 4, 5],
+  [0, 2, 3, 5],
+  [0, 3, 5],
+  [0, 2, 4, 5],
+  [0, 3, 4, 5],
+  [0, 2, 5],
+  [0, 6],
+  [0, 1, 3, 4, 6],
+  [0, 4, 6],
+  [0, 1, 3, 6],
+  [0, 3, 6],
+  [0, 1, 4, 6],
+  [0, 3, 4, 6],
+  [0, 1, 6],
+  [0, 3, 4, 5, 6],
+  [0, 2, 5, 6],
+  [0, 1, 5, 6],
+  [0, 1, 2, 3, 4, 5, 6],
+  [0, 2, 3, 4, 5, 6],
+  [0, 5, 6],
+  [0, 1, 2, 5, 6],
+  [0, 1, 3, 4, 5, 6],
+  [0, 7],
+  [0, 1, 2, 4, 7],
+  [0, 4, 7],
+  [0, 1, 2, 7],
+  [0, 2, 7],
+  [0, 1, 4, 7],
+  [0, 2, 4, 7],
+  [0, 1, 7],
+  [0, 2, 4, 5, 7],
+  [0, 3, 5, 7],
+  [0, 1, 5, 7],
+  [0, 1, 2, 3, 4, 5, 7],
+  [0, 2, 3, 4, 5, 7],
+  [0, 5, 7],
+  [0, 1, 3, 5, 7],
+  [0, 1, 2, 4, 5, 7],
+  [0, 1, 4, 6, 7],
+  [0, 3, 6, 7],
+  [0, 2, 6, 7],
+  [0, 1, 2, 3, 4, 6, 7],
+  [0, 1, 3, 4, 6, 7],
+  [0, 6, 7],
+  [0, 2, 3, 6, 7],
+  [0, 1, 2, 4, 6, 7],
+  [0, 1, 2, 3, 4, 5, 6, 7],
+  [0, 1, 5, 6, 7],
+  [0, 2, 5, 6, 7],
+  [0, 3, 4, 5, 6, 7],
+  [0, 3, 5, 6, 7],
+  [0, 2, 4, 5, 6, 7],
+  [0, 1, 4, 5, 6, 7],
+  [0, 1, 2, 3, 5, 6, 7],
+  [0, 8],
+  [0, 1, 2, 3, 8],
+  [0, 3, 8],
+  [0, 1, 2, 8],
+  [0, 2, 8],
+  [0, 1, 3, 8],
+  [0, 2, 3, 8],
+  [0, 1, 8],
+  [0, 2, 3, 5, 8],
+  [0, 4, 5, 8],
+  [0, 2, 3, 4, 5, 8],
+  [0, 5, 8],
+  [0, 1, 5, 8],
+  [0, 1, 2, 3, 4, 5, 8],
+  [0, 1, 4, 5, 8],
+  [0, 1, 2, 3, 5, 8],
+  [0, 1, 3, 6, 8],
+  [0, 4, 6, 8],
+  [0, 1, 3, 4, 6, 8],
+  [0, 6, 8],
+  [0, 2, 6, 8],
+  [0, 1, 2, 3, 4, 6, 8],
+  [0, 2, 4, 6, 8],
+  [0, 1, 2, 3, 6, 8],
+  [0, 1, 2, 3, 4, 5, 6, 8],
+  [0, 1, 5, 6, 8],
+  [0, 2, 5, 6, 8],
+  [0, 3, 4, 5, 6, 8],
+  [0, 4, 5, 6, 8],
+  [0, 2, 3, 5, 6, 8],
+  [0, 1, 3, 5, 6, 8],
+  [0, 1, 2, 4, 5, 6, 8],
+  [0, 1, 2, 7, 8],
+  [0, 4, 7, 8],
+  [0, 1, 2, 4, 7, 8],
+  [0, 7, 8],
+  [0, 3, 7, 8],
+  [0, 1, 2, 3, 4, 7, 8],
+  [0, 3, 4, 7, 8],
+  [0, 1, 2, 3, 7, 8],
+  [0, 1, 2, 3, 4, 5, 7, 8],
+  [0, 1, 5, 7, 8],
+  [0, 3, 5, 7, 8],
+  [0, 2, 4, 5, 7, 8],
+  [0, 4, 5, 7, 8],
+  [0, 2, 3, 5, 7, 8],
+  [0, 1, 2, 5, 7, 8],
+  [0, 1, 3, 4, 5, 7, 8],
+  [0, 1, 2, 3, 4, 6, 7, 8],
+  [0, 2, 6, 7, 8],
+  [0, 3, 6, 7, 8],
+  [0, 1, 4, 6, 7, 8],
+  [0, 4, 6, 7, 8],
+  [0, 1, 3, 6, 7, 8],
+  [0, 1, 2, 6, 7, 8],
+  [0, 2, 3, 4, 6, 7, 8]]
+
+/-- Exact retained-major membership loop in the pinned record exporter. -/
+def exportedWindows : List (Nat × List Nat) := [(603, [120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239]),
+  (568, [120, 123, 125, 126, 137, 139, 141, 143, 146, 147, 150, 151, 153, 155, 157, 159, 162, 163, 166, 167, 168, 171, 172, 175, 176, 177, 182, 183, 185, 187, 189, 191, 196, 197, 198, 199, 200, 202, 205, 207, 208, 209, 214, 215, 216, 218, 221, 223, 224, 225, 230, 231, 232, 235, 237, 238]),
+  (597, [121, 123, 125, 127, 129, 131, 133, 135, 145, 147, 148, 150, 153, 155, 156, 158, 160, 163, 164, 167, 170, 171, 174, 175, 176, 178, 181, 183, 185, 187, 188, 190, 192, 194, 197, 199, 204, 205, 206, 207, 208, 210, 213, 215, 216, 218, 221, 223, 224, 227, 229, 230, 232, 233, 238, 239]),
+  (583, [122, 123, 126, 127, 129, 131, 132, 134, 137, 139, 140, 142, 144, 147, 148, 151, 161, 163, 164, 166, 169, 171, 172, 174, 176, 179, 180, 183, 185, 186, 189, 190, 192, 194, 197, 199, 200, 202, 205, 207, 208, 211, 213, 214, 220, 221, 222, 223, 224, 226, 229, 231, 232, 234, 237, 239]),
+  (569, [124, 125, 126, 127, 129, 130, 133, 134, 137, 138, 141, 142, 144, 147, 148, 151, 153, 154, 157, 158, 160, 163, 164, 167, 168, 171, 172, 175, 176, 179, 181, 182, 193, 194, 197, 198, 201, 202, 205, 206, 208, 211, 212, 215, 217, 218, 221, 222, 224, 227, 228, 231, 232, 235, 236, 239]),
+  (604, [128, 129, 130, 131, 132, 133, 134, 135, 144, 145, 146, 147, 148, 149, 150, 151, 160, 161, 162, 163, 164, 165, 166, 167, 176, 177, 178, 179, 180, 181, 182, 183, 192, 193, 194, 195, 196, 197, 198, 199, 208, 209, 210, 211, 212, 213, 214, 215, 224, 225, 226, 227, 228, 229, 230, 231]),
+  (616, [136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 232, 233, 234, 235, 236, 237, 238, 239]),
+  (596, [152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239]),
+  (598, [184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239])]
+
+theorem source_shape : v = 120 ∧ R = 420 ∧ 2*v+R = 660 ∧
+    ret.length = 9 ∧ scatter.length = 120 ∧
+    (scatter.map List.length).foldl Nat.add 0 = 568 := by decide +kernel
+end CurrentMain.R420ScatterData
+#print axioms CurrentMain.R420ScatterData.source_shape
diff --git a/research/r420-scatter-lifecycle/R420ScatterLifecycle.lean b/research/r420-scatter-lifecycle/R420ScatterLifecycle.lean
new file mode 100644
index 0000000000..9aaee269c4
--- /dev/null
+++ b/research/r420-scatter-lifecycle/R420ScatterLifecycle.lean
@@ -0,0 +1,181 @@
+import R420ScatterData
+import BitCopyScatterWindow
+
+/-! Exact R420 instance of the retained-major COPY/ADD/ERASE scalar slice.
+The 660 original registers and disposable slot 660 form a fresh Fin 661 domain.
+The current retained centres and scatter rows come from the pinned R420 word.
+Adapted from James Chang's PR590 historical instance, with OpenAI assistance
+by Chinmay (@chinmayarvind23). Physical COPY/ERASE legality and frames remain
+separate obligations. The generated loop order is retained-major. -/
+namespace CurrentMain.R420ScatterLifecycle
+open R420ScatterData
+set_option Elab.async false
+abbrev Register := Fin 661
+abbrev OriginalRegister := Fin 660
+abbrev State := Register → Bool
+abbrev RawWindow := Nat × List Nat
+
+def temp : Register := ⟨660, by decide⟩
+def IsTarget (r : Register) : Prop := 120 ≤ r.val ∧ r.val < 240
+
+def embed (r : OriginalRegister) : Register :=
+  ⟨r.val, Nat.lt_trans r.isLt (by decide : 660 < 661)⟩
+
+theorem original_excludes_temp (r : OriginalRegister) : embed r ≠ temp := by
+  intro he
+  have hv : r.val = 660 := congrArg Fin.val he
+  exact (Nat.ne_of_lt r.isLt) hv
+
+/-- Exact enumerate-ret, enumerate-scatter, membership-test scalar projection.
+No default lookup is used. COPY/ERASE surround each returned destination list. -/
+def rawWindows : List RawWindow :=
+  ret.zipIdx.map (fun q =>
+    (q.1, scatter.zipIdx.filterMap (fun row =>
+      if q.2 ∈ row.1 then some (120 + row.2) else none)))
+
+/-- Python exporter and Lean decoder agree on every centre and destination,
+including their order; the literal right side is regenerated from the word. -/
+theorem exporter_window_binding : rawWindows = exportedWindows := by decide +kernel
+
+theorem raw_shape : rawWindows.length = 9 ∧
+    rawWindows.map (fun w => w.2.length) = [120,56,56,56,56,56,56,56,56] ∧
+    (rawWindows.map (fun w => w.2.length + 2)).foldl Nat.add 0 = 586 := by
+  decide +kernel
+
+theorem raw_domains : rawWindows.all (fun w =>
+    decide (240 ≤ w.1 ∧ w.1 < 660) &&
+    w.2.all (fun d => decide (120 ≤ d ∧ d < 240))) = true := by
+  decide +kernel
+
+/-- Membership emits each target once per retained index. The stored rows also
+have no repeated indices, recorded separately without permuting the word. -/
+theorem source_rows_no_duplicates : scatter.all (fun row => decide row.Nodup) = true := by
+  decide +kernel
+
+attribute [local irreducible] rawWindows scatter
+
+private theorem raw_properties (w : RawWindow) (hw : w ∈ rawWindows) :
+    (240 ≤ w.1 ∧ w.1 < 660) ∧ ∀ d ∈ w.2, 120 ≤ d ∧ d < 240 := by
+  have h := Bool.and_eq_true_iff.mp ((List.all_eq_true.mp raw_domains) w hw)
+  refine ⟨of_decide_eq_true h.1, ?_⟩
+  intro d hd
+  exact of_decide_eq_true ((List.all_eq_true.mp h.2) d hd)
+
+def decodeWindow (w : RawWindow) (hw : w ∈ rawWindows) : BitCopyScatter.Window Register where
+  centre := ⟨w.1, Nat.lt_trans (raw_properties w hw).1.2 (by decide : 660 < 661)⟩
+  targets := w.2.attach.map (fun d =>
+    ⟨d.val, Nat.lt_trans ((raw_properties w hw).2 d.val d.property).2 (by decide : 240 < 661)⟩)
+
+def windows : List (BitCopyScatter.Window Register) :=
+  rawWindows.attach.map (fun w => decodeWindow w.val w.property)
+
+def encodeWindow (w : BitCopyScatter.Window Register) : RawWindow :=
+  (w.centre.val, w.targets.map Fin.val)
+
+theorem decode_roundtrip (w : RawWindow) (hw : w ∈ rawWindows) :
+    encodeWindow (decodeWindow w hw) = w := by
+  rcases w with ⟨centre, targets⟩
+  simp only [encodeWindow, decodeWindow, List.map_map, Function.comp_def]
+  rw [List.attach_map_subtype_val]
+
+theorem ordered_window_binding : windows.map encodeWindow = rawWindows := by
+  unfold windows
+  rw [List.map_map]
+  simp only [Function.comp_def, decode_roundtrip]
+  exact List.attach_map_subtype_val _
+
+theorem decoded_bounds (w : BitCopyScatter.Window Register) (hw : w ∈ windows) :
+    (240 ≤ w.centre.val ∧ w.centre.val < 660) ∧
+      ∀ d ∈ w.targets, IsTarget d := by
+  obtain ⟨raw, hraw, heq⟩ := List.mem_map.mp hw
+  subst w
+  constructor
+  · exact (raw_properties raw.val raw.property).1
+  · intro d hd
+    simp only [decodeWindow] at hd
+    obtain ⟨target, htarget, heq⟩ := List.mem_map.mp hd
+    subst d
+    exact (raw_properties raw.val raw.property).2 target.val target.property
+
+theorem windows_well_formed (w : BitCopyScatter.Window Register) (hw : w ∈ windows) :
+    BitCopyScatter.WellFormed temp w := by
+  have h := decoded_bounds w hw
+  constructor
+  · intro he
+    have hv := congrArg Fin.val he
+    exact (Nat.ne_of_lt h.1.2) hv
+  · intro d hd
+    have ht := h.2 d hd
+    constructor
+    · intro he
+      have hv := congrArg Fin.val he
+      exact (Nat.ne_of_lt (Nat.lt_trans ht.2 (by decide : 240 < 660))) hv
+    · intro he
+      have hv := congrArg Fin.val he
+      exact (Nat.ne_of_lt (Nat.lt_of_lt_of_le ht.2
+        (Nat.le_trans (by decide : 240 ≤ 240) h.1.1))) hv
+
+theorem windows_nonempty : windows ≠ [] := by
+  have hl : windows.length = 9 := by
+    simpa only [windows, List.length_map, List.length_attach] using raw_shape.1
+  intro he
+  rw [he] at hl
+  contradiction
+
+def executeScatter (s : State) : State := BitCopyScatter.runWindows temp windows s
+def directScatter (s : State) : State := BitCopyScatter.directWindows windows s
+
+/-- Every original coordinate follows the direct retained-major XOR scatter;
+the temporary is explicitly discarded to false for every incoming value. -/
+theorem exact_lifecycle (s : State) :
+    executeScatter s = BitCopyScatter.clear temp (directScatter s) :=
+  BitCopyScatter.runWindows_eq_clear_direct temp windows windows_nonempty windows_well_formed s
+
+theorem final_temp_zero (s : State) : executeScatter s temp = false := by
+  rw [exact_lifecycle]
+  exact BitCopyScatter.clear_at_temp temp (directScatter s)
+
+theorem original_coordinate (s : State) (r : Register) (hr : r ≠ temp) :
+    executeScatter s r = directScatter s r := by
+  rw [exact_lifecycle]
+  simp [BitCopyScatter.clear, hr]
+
+theorem original_registers (s : State) (r : OriginalRegister) :
+    executeScatter s (embed r) = directScatter s (embed r) :=
+  original_coordinate s (embed r) (original_excludes_temp r)
+
+/-- Arbitrary original source/helper dirt is retained across the copy slice. -/
+theorem sources_helpers_preserved (s : State) (r : Register)
+    (hr : ¬ IsTarget r) (ht : r ≠ temp) : executeScatter s r = s r := by
+  rw [original_coordinate s r ht]
+  exact BitCopyScatter.directWindows_untouched windows s r
+    (fun w hw hmem => hr ((decoded_bounds w hw).2 r hmem))
+
+theorem incoming_temp_independent (s t : State)
+    (h : ∀ r, r ≠ temp → s r = t r) : executeScatter s = executeScatter t :=
+  BitCopyScatter.runWindows_independent_of_temp temp windows windows_nonempty windows_well_formed s t h
+
+/-- This restoration statement requires the disposable slot to start at zero.
+An arbitrary incoming value in temporary 660 is discarded, not restored. -/
+theorem clean_temp_restored (s : State) (h : s temp = false) :
+    executeScatter s temp = s temp := by
+  rw [final_temp_zero, h]
+
+end CurrentMain.R420ScatterLifecycle
+#print axioms CurrentMain.R420ScatterLifecycle.original_excludes_temp
+#print axioms CurrentMain.R420ScatterLifecycle.exporter_window_binding
+#print axioms CurrentMain.R420ScatterLifecycle.raw_shape
+#print axioms CurrentMain.R420ScatterLifecycle.raw_domains
+#print axioms CurrentMain.R420ScatterLifecycle.source_rows_no_duplicates
+#print axioms CurrentMain.R420ScatterLifecycle.decode_roundtrip
+#print axioms CurrentMain.R420ScatterLifecycle.ordered_window_binding
+#print axioms CurrentMain.R420ScatterLifecycle.decoded_bounds
+#print axioms CurrentMain.R420ScatterLifecycle.windows_well_formed
+#print axioms CurrentMain.R420ScatterLifecycle.windows_nonempty
+#print axioms CurrentMain.R420ScatterLifecycle.exact_lifecycle
+#print axioms CurrentMain.R420ScatterLifecycle.final_temp_zero
+#print axioms CurrentMain.R420ScatterLifecycle.original_coordinate
+#print axioms CurrentMain.R420ScatterLifecycle.original_registers
+#print axioms CurrentMain.R420ScatterLifecycle.sources_helpers_preserved
+#print axioms CurrentMain.R420ScatterLifecycle.incoming_temp_independent
+#print axioms CurrentMain.R420ScatterLifecycle.clean_temp_restored
diff --git a/research/r420-scatter-lifecycle/R420_NOTICE.md b/research/r420-scatter-lifecycle/R420_NOTICE.md
new file mode 100644
index 0000000000..cb68783d7d
--- /dev/null
+++ b/research/r420-scatter-lifecycle/R420_NOTICE.md
@@ -0,0 +1,64 @@
+# Notice
+
+Apache-2.0 (`LICENSE`, copied from #493's package). Prepared by eumemic with substantial Anthropic Claude
+assistance.
+
+## New in this package
+
+- `code/gen_l3.py` (the generator), `code/nodeopt.py` (bill-aware realization of the block nodes), `code/planio.py`
+  (plan loader), `data/plan-l3.json` (the CP-SAT plan, nominated by `discovery/planL3.py` and `discovery/planL3b.py`)
+  and `data/bitE8mut-r420.json.gz` (the word).
+- `code/xcheck.py` (independent exact replay and interleaved-interface audit), `code/mutants.py` (word-level mutation
+  controls), `code/mutrec_b.py` (record-level phase-B mutants, adapted from #493's `mutate_records_mut.py`).
+- `code/adapt11.py` (R-specific copies of #493's eleven-stage audit files; the same six edits #503's `adapt.py`
+  makes for R = 480).
+- `code/provenance.py` (adapted from #493's, itself from #381's), `code/cited.py`, `code/summary.py`, `verify.sh`,
+  `EXPECTED.json`, `DEPENDS.json`, `requirements.txt`, `data/complex-b.json`, `data/selection9-r420.json` and
+  `data/hosting11-r420.json` (frozen nominations of #442's hosting programme, rediscovered by `verify.sh`),
+  `.github/workflows/e8-bit-r420.yml`.
+
+## Vendored, byte-identical (git blob ids in `SOURCE-pr*.json`, checked by `code/provenance.py`)
+
+- **PR #510 (DreamingOfClouds, with Claude Opus 5.5 via Claude Code), commit 64edee1** (`vendor/pr510/`):
+  - `e8-r480-nine-stage/code/assemble9.py` (#463's nine-stage invoice and #493's outer-assembly loop),
+    `code/adapt.py`, `data/selection9-r480.json` and `EXPECTED.json`;
+  - the files #510 vendors from PR #463 (DreamingOfClouds; head cdf0c1c):
+    - `e8-r715-eleven-stage-whole/code/{global_k,emit_k,audit_parent_k,audit_hosted_k,hosting_k,bank_routes_k}.py`,
+      derived from PR #443 and PR #444 (chafreaky, with OpenAI Codex assistance), PR #442 (DaysSky, with Claude) and
+      PR #386 (Zhihao Chen, with OpenAI Codex assistance);
+    - `e8-r740-replica32/code/{config,bank_routes,tile_m,e8core}.py` (PR #443, chafreaky) and `engines/` (PR #315's
+      moment engines, DreamingOfClouds);
+    - `idle-axis-hosting/hosting_core.py` (PR #442, DaysSky, with Anthropic Claude assistance);
+  - `e8-r480-dead-totals/data/bitE8mut-r480.json.gz`: PR #503's R480 word (DreamingOfClouds), as carried by #510's
+    branch.
+- **PR #535 (icekylinx, with GPT-6 Astra assistance), commit 8b758a1** (`data/complex/pr535/`): `EXPECTED.json` and
+  `evidence/audit/EXACT-ASSEMBLY-PR493.json` (the same blobs as at 25f9b7c).
+
+## Used from main, unchanged (pinned in `DEPENDS.json`)
+
+- `research/e8-bit-carrier-skeleton` (PR #493, eumemic): the skeleton modules and D4 partition the generator imports;
+  #370's checker and its relaxed copy; the official cohort checkers (#266 as generalised by #370; #381's
+  `columns_k.cpp`); `gram_frames.py`; the record exporter and mutants; #386's nine-stage and #445's eleven-stage
+  geometry; #472's eleven-stage emitter, audit and assembly as adapted there; #442's hosting programme
+  (`discovery/host_select.py`); the R489 word; the control receipts. Provenance and licences of those files are in
+  that package's `NOTICE.md`.
+- `research/direct-delivery504-global/EXPECTED.json` (PR #531, icekylinx, with GPT-6 Astra assistance): its complex b
+  and κ.
+
+## Cited, not rebuilt
+
+Complex coarse savings in `data/complex-b.json`, each bound to its PR's receipt by `code/cited.py`: PR #535 (primary;
+open), PR #531 (merged), and PR #484, #471 and #458 (controls). No complex construction is rebuilt here.
+
+## Ideas used
+
+- PR #493 (eumemic): the D4 quad skeleton with sources as carriers.
+- PR #503 (DreamingOfClouds): the nine totals on dead registers, hosted by the last eligible register.
+- PR #510 (DreamingOfClouds): the nine-stage pricing of these words. DreamingOfClouds' LP in #493's thread gives 480
+  under the hypothesis this word avoids.
+- PR #425 (Zhihao Chen / jacklightChen, with OpenAI Codex assistance): the scalar-interface lemma.
+- PR #535's `PR510-MUTABLE-SOURCE-CARRYOVER.md` (icekylinx): the role-independent bit-side pullback argument.
+- PR #370 (Dylan Crow / utcorvusvolat-dotcom): the bitE8/1 format, its independent checker and the decoder totals.
+- PR #472, #445, #443 (chafreaky), PR #442 (DaysSky), PR #463 and #315 (DreamingOfClouds), PR #386 (Zhihao Chen): the
+  pricing pipelines.
+- Jacob Sussman introduced the E8 unit.
diff --git a/research/r420-scatter-lifecycle/README.md b/research/r420-scatter-lifecycle/README.md
new file mode 100644
index 0000000000..c85ca4663d
--- /dev/null
+++ b/research/r420-scatter-lifecycle/README.md
@@ -0,0 +1,95 @@
+# R420 COPY/scatter lifecycle
+
+This proves the Boolean behavior of the **661-register** retained-major scatter
+slice of eumemic's PR543 R420 word: **9 COPY, 568 ADD and 9 ERASE** operations.
+It fills the scalar lifecycle obligation left open by PR612. The R420 word is a
+historical component; this package does not certify the complete current selected
+construction or improve κ.
+The repository source pins use main `f567884aeb8851b6e794af1184119a3bfbe1e631`.
+
+For every input state, including arbitrary source, helper and temporary bits:
+
+- Each of the 660 original coordinates equals direct retained-centre XOR scatter.
+- Original source/helper coordinates are preserved.
+- Temporary register 660 ends false, independently of its incoming value.
+- Its incoming value is restored only under the explicit premise that it was false.
+
+`R420ScatterData.lean` contains current retained centres, scatter rows and the exact
+ordered windows obtained from the record exporter. `check.py` regenerates those
+literals from the pinned JSON before compiling. The kernel proves the Lean
+membership loop equals every exported centre/destination in order; aggregate
+counts alone are insufficient. Fresh finite bounds then instantiate PR590's
+generic COPY/scatter theorem on `Fin 661`. All four modules compile from source;
+no historical `Fin 730` object is retained or renamed.
+
+The exporter is pinned at
+`research/e8-bit-carrier-skeleton/code/bit/export_records.py`, lines 59–63, which
+R420 reuses. COPY is modeled as overwrite, ADD as Boolean XOR, and ERASE as writing
+false. This is a scalar projection: frame transport, physical allocation and
+ERASE legality, A/C cleanup, D compensation, the complete multiplier and all-size
+transfer remain separate. No equality with a reordered row-major circuit is claimed.
+
+## Reproduce
+
+Use Python 3 and the official **Lean 4.21.0 Linux** distribution, with no Mathlib
+or network access. The existing PR612 official-core manifest pins the Lean binary
+and all 317 `Init` source/object pairs; the checker checks these before and after
+the build. The supplied compiler and shared-library runtime remain trusted;
+these manifest checks do not pin the complete executable runtime.
+Repository supplier scripts are never executed.
+
+From the repository root:
+
+```sh
+python3 research/r420-scatter-lifecycle/check.py \
+  --lean /opt/lean-4.21.0-linux/bin/lean --build-dir /tmp/r420-lifecycle-build
+```
+
+The build directory must not exist. Each module gets a fresh object, a 60-second
+wall/CPU budget, a 4 GiB address-space limit and one compiler thread. The checker
+requires all **28** printed probes, in order, to use only standard Lean axioms.
+Objects, raw logs and `RESULT.json` are written outside the package. For only
+source correspondence, use `--bind-only`; that mode does not claim a Lean build.
+
+`MANIFEST.json` records repository inputs, source hashes, imports and probes.
+The source-binding boundary is external to Lean; the literal theorem itself is
+kernel checked. The official runtime manifest is reused from
+`research/lean-current-r420-boundary-interfaces/OFFICIAL_CORE_MANIFEST.json`.
+
+The eleven source-binding controls run with either normal or optimized Python:
+
+```sh
+cd research/r420-scatter-lifecycle
+python3 -m unittest -v test_binding
+python3 -O -m unittest -v test_binding
+```
+
+Three controls alter retained order, a scatter index or exported destination
+order while preserving the shapes and refreshing the local data hash; source
+regeneration must still reject them. Other controls change proof, exporter or
+generic semantics, and one checks a valid relocated set of inputs.
+Omitted modules, lifecycle probes or exporter inputs and redirected source paths
+must also be rejected.
+
+An optional compiler acceptance control copies the package to a new directory,
+replaces only the lifecycle proof with `sorry`, refreshes its source hash, and
+requires rejection of the resulting `sorryAx` probe after compilation:
+
+```sh
+python3 test_kernel_rejection.py --lean /opt/lean-4.21.0-linux/bin/lean \
+  --output-dir /tmp/r420-lifecycle-negative
+```
+
+The accepted package remains unchanged. Recorded results are in `VALIDATION.md`.
+
+## Attribution
+
+Apache-2.0. Prepared by Chinmay (@chinmayarvind23), with substantial OpenAI Codex
+assistance. `BitXorTargetTranslation.lean` and `BitCopyScatterWindow.lean` are
+byte-identical to James Chang's PR590 at
+`58690bdbb587f482569ba1bdf7bf61a5396b4768`; the lifecycle proof adapts its explicitly
+historical instance. PR612 identified the remaining R420 obligation; PR834 audits
+that package's source expressions but does not establish this lifecycle theorem.
+The R420 supplier is eumemic's work with substantial Anthropic Claude assistance;
+the inherited record exporter credits Dylan Crow / utcorvusvolat-dotcom.
+Original notices are preserved in `SUPPLIER_NOTICE.md` and `R420_NOTICE.md`.
diff --git a/research/r420-scatter-lifecycle/SUPPLIER_NOTICE.md b/research/r420-scatter-lifecycle/SUPPLIER_NOTICE.md
new file mode 100644
index 0000000000..5a0ecdcd2c
--- /dev/null
+++ b/research/r420-scatter-lifecycle/SUPPLIER_NOTICE.md
@@ -0,0 +1,69 @@
+# Notice
+
+Apache-2.0 (`LICENSE`). Prepared by eumemic with substantial Anthropic Claude assistance.
+
+## New in this package
+
+- `code/skeleton/`: the D4 quad-skeleton geometry (`geom.py`), the word builder with source registers as gate
+  destinations (`wordkit.py`), the generator (`gen.py`) and an E8 root-line helper (`e8.py`, #370's Hamming
+  coordinates and line order).
+- `data/skeleton/plan-skB.json` (CP-SAT plan nominated by `discovery/plan.py`), `data/skeleton/d4part-pairs.json`
+  (the 5-pair D4 partition, found by `discovery/d4part.py`), `data/bit/bitE8mut-r489.json.gz` (the word),
+  `data/eleven/hosting.json` (frozen hosting selection nominated by `discovery/host_select.py` with #442's integer
+  programme), `data/eleven/residual-isometries.json` (the frame-zero record of #443's isometry format: every helper of
+  this word enters at frame zero).
+- `code/bit/independent/relax.py` (generates the relaxed #370 checker), `interface.py` (#425 lemma hypotheses),
+  `mutate_mut.py` (word-level mutants and hypothesis controls), `code/bit/mutate_records_mut.py` (record-level
+  mutable-source mutants).
+- `code/eleven/adapt.py` and the adapted files it checks, `code/eleven/{emit,audit,local_audit}.py` (PR #472's files
+  plus 19 listed edits: R = 489, package paths, a `--hosting` argument, one frame-zero entrance instead of eleven).
+- `code/eleven/assemble.py`: PR #472's bit invoice and pricing arithmetic with R as a parameter, and its outer
+  assembly run once per cited complex supplier.
+- `code/cited.py`, `data/complex-b.json`, `verify.sh`, `EXPECTED.json`, `requirements.txt`, `discovery/`,
+  `.github/workflows/e8-bit-carrier-skeleton.yml`.
+
+## Vendored, byte-identical (git blob ids in `SOURCE-pr*.json`, checked by `code/provenance.py`)
+
+- **PR #370 (Dylan Crow / utcorvusvolat-dotcom, with Anthropic Claude assistance), commit b7fe9cd:** the independent
+  checker `checkword.py` and its controls `mutate.py`; `export_records.py`, `mutate_records.py`, `stage_cohort.py`;
+  PR #266's official cohort checkers as generalised there (`legality_h.cpp`, `columns_h.cpp`, NCOPY); nlohmann/json
+  (`json.hpp`, MIT licence in its header); `gram_frames.py`; PR #315's engines (`code/pricing/`, DreamingOfClouds);
+  the R865 word `data/bit/bitE8-r865.json.gz` (read only for the E8 label table by the geometry scripts); `LICENSE`.
+- **PR #381 (DaysSky, assisted with Claude), commit 00765b2:** `columns_k.cpp`.
+- **PR #386 (Zhihao Chen / jacklightChen, with OpenAI Codex assistance), commit dd11cf8:** the nine-stage bit geometry
+  `code/nine/geometry.py` (parent geometry checked by the eleven-stage audit) and `portable-include/bits/stdc++.h`.
+- **PR #436 (eumemic, with Anthropic Claude assistance), commit 8f6b829:** `code/provenance.py`.
+- **PR #445 (chafreaky, with OpenAI Codex assistance), commit 40ab91d:** `code/hub/r740-hosted-eleven/code/geometry.py`
+  (eleven-stage geometry), `row_bound.py` (orthogonal-cover row bound), `emit.py` and `data/selection.json` (used
+  unchanged for the PR #445 control).
+- **PR #451 (chafreaky, with OpenAI Codex assistance), commit f3a3815:** `code/hub/r740-hosted-rank149/`: its
+  eleven-stage bit emitter (byte-identical to PR #445's), frozen selection, R740 rank149 word and isometries
+  (PR #451 control).
+- **PR #472 (chafreaky, with OpenAI Codex assistance), commit 259c684,** and files its branch carries unchanged:
+  - `code/hub/e8-r715-whole-hosted/`: PR #472's eight-replica pooled emitter, independent audit, local projector
+    audit and assembly (the originals of the adapted files), its R715 word, isometries and frozen hosting (used
+    unchanged for the PR #472 control);
+  - `code/hub/e8-r740-replica32/`: PR #443 (chafreaky): `bank_routes.py`, `tile_m.py`, `e8core.py`, the R740 rank138
+    word and its isometries (PR #445 control); PR #315's engines (DreamingOfClouds) in `code/engines/`;
+  - `code/hub/idle-axis-hosting/hosting_core.py`: PR #442 (DaysSky, with Anthropic Claude assistance).
+- **Receipts (`data/complex/`):** `EXPECTED.json` of PR #484 (DreamingOfClouds, 035845c), PR #471 (Dugongue,
+  56b3da6), PR #458 (chafreaky, 44e9eae), PR #448 (higherbeing, 359022b), and of the bit-bound frontier PRs #483
+  (Dugongue, 3738c3c), #473 (rohanarun, c7590f1) and #478 (Dugongue, bea1d52).
+
+The repository-level files `certificates/joint-dual-kappa.json`, `certificates/joint-dual-validation.json` and
+`research/joint-dual/SOURCE.json` in this branch are byte-identical to rohanarun's PR #318 (a45747d). They repair
+stale root-file pins so the repository's joint check passes; #417, #436 and #439 carry the same repair.
+
+## Cited, not rebuilt
+
+Complex coarse savings in `data/complex-b.json`, each bound to its PR's `EXPECTED.json` by `code/cited.py`:
+PR #484 (primary; draft, conditional on its Lemmas A and G), PR #471 (the complex supplier of #473, #478 and #483),
+PR #458 (the complex supplier of #472) and PR #448 (information only; disputed cross-copy split). No complex
+construction is rebuilt here.
+
+## Ideas used
+
+PR #425 (Zhihao Chen, with OpenAI Codex assistance): the scalar-interface lemma that permits source registers as
+gate destinations when the full-frame cleanup restores them. PR #463 (DreamingOfClouds, with Claude Opus 5.5): the
+carrier bound (three registers leave a source's line). PR #433 (icekylinx): source rows written on the bit side.
+PR #442 (DaysSky): idle-axis hosting of whole residuals. Jacob Sussman introduced the E8 unit.
diff --git a/research/r420-scatter-lifecycle/VALIDATION.md b/research/r420-scatter-lifecycle/VALIDATION.md
new file mode 100644
index 0000000000..d87761632a
--- /dev/null
+++ b/research/r420-scatter-lifecycle/VALIDATION.md
@@ -0,0 +1,46 @@
+# Validation, 2026-10-13
+
+One fresh positive build passed on the first attempt: **4 modules and all 28
+required probes**, each using only standard Lean axioms. No previous objects were
+retained. `exact_lifecycle` uses `propext` and `Quot.sound`; no `sorryAx` or
+`Lean.ofReduceBool` was accepted. All eleven source-binding tests passed under
+normal Python and `python -O`.
+
+The official Lean 4.21.0 Linux release reported commit `6741444a63ee`. Its release
+archive SHA-256 was checked before extraction:
+`455c6df09d5bd54d2a51b137939c47e2dda816d512ac789c4b3642c9bf98bde8`.
+The checker verified the inherited 317-module `Init` manifest before and after
+compilation. The provided compiler/shared-library runtime remains a trusted input.
+
+Execution used the official Python 3.12 container
+`python@sha256:a6e34c598f2467ed0e9a8d349809fcd8b5c603269512df273a0bb1784edc11b1`,
+with network disabled, a read-only root filesystem, dropped capabilities,
+`no-new-privileges`, a 6 GiB container limit and two CPUs. Source and Lean runtime
+mounts were read-only. Each Lean process additionally had the limits documented
+in the README. The measurements below include subprocess wall time on this host;
+they are not benchmarks or portable performance guarantees.
+
+| Module | Seconds | Raw log SHA-256 |
+|---|---:|---|
+| BitXorTargetTranslation | 7.903805 | `a318c0e783704721480ab18b79e230e55b6ad2e43ddad13346744b52b0aad29b` |
+| BitCopyScatterWindow | 7.861302 | `5765dea8e482ea3bf34e3307faf42a1e126470a361009188f1ce10ccf493e7dd` |
+| R420ScatterData | 8.365274 | `3821642190add5514dbafb619d24f29b43fca0a9c0e957e0a04b93d007858cf3` |
+| R420ScatterLifecycle | 9.204342 | `c69c7f9bf3bd4d9b55da8dfb34602e78635c639ed6a7befde9cded9ffb13693c` |
+
+The emitted `RESULT.json` SHA-256 was
+`498b7f9e662d31279e7558191c4f691aa276d6d2b2d8514fa70277421a07dc05`;
+its input `MANIFEST.json` SHA-256 was
+`447b11e3f43eefb3d63b4395801bc5d7f99e8a777b8b7da2fa532a1d8c2f8ee6`.
+The reproduction command emits fresh source copies, objects, logs and a result
+receipt into the specified build directory; timing and warning paths can differ.
+
+The independent acceptance control also passed. With the exact lifecycle proof
+replaced by `sorry` in a temporary copy and its manifest hash refreshed, Lean
+compiled the module but reported `[propext, sorryAx, Quot.sound]` for that theorem.
+The checker exited 1 with `nonstandard axioms: CurrentMain.R420ScatterLifecycle.exact_lifecycle`.
+Its raw Lean log SHA-256 was
+`574ac69eca593e3fd5ae7f342e73028b4fc1acae5ec6ea192de09d8b934977e9`.
+This exercises axiom acceptance independently of source-hash rejection.
+
+These are scoped local checks. No full repository replay, CI success, physical
+COPY/ERASE proof, complete selected-construction proof or improved κ is reported.
diff --git a/research/r420-scatter-lifecycle/check.py b/research/r420-scatter-lifecycle/check.py
new file mode 100644
index 0000000000..0d2e88ba39
--- /dev/null
+++ b/research/r420-scatter-lifecycle/check.py
@@ -0,0 +1,200 @@
+#!/usr/bin/env python3
+"""Bind the R420 literals, then compile four fresh Lean modules offline."""
+import argparse
+import gzip
+import hashlib
+import json
+import os
+from pathlib import Path
+import re
+import resource
+import shutil
+import signal
+import subprocess
+import time
+
+PACKAGE = Path(__file__).resolve().parent
+STANDARD_AXIOMS = {"propext", "Classical.choice", "Quot.sound"}
+CORE_MANIFEST_SHA = "2c27354193fc7b11079b61116ab8e9c80485903845bda48ddf3c66057fed2cb1"
+SOURCE_PATHS = [
+    "research/e8-bit-r420/data/bitE8mut-r420.json.gz",
+    "research/e8-bit-carrier-skeleton/code/bit/export_records.py",
+    "research/lean-current-r420-boundary-interfaces/OFFICIAL_CORE_MANIFEST.json",
+]
+REQUIRED_PROBES = {
+    "BitXorTargetTranslation": ("CurrentMain.BitXor", [
+        "run_shift", "run_off_target", "target_identity", "erased_eq_of_agree_off_target"]),
+    "BitCopyScatterWindow": ("CurrentMain.BitCopyScatter", [
+        "copy_at_temp", "clear_at_temp", "window_eq_clear_direct", "runWindows_eq_clear_direct",
+        "directWindows_untouched", "runWindows_independent_of_temp"]),
+    "R420ScatterData": ("CurrentMain.R420ScatterData", ["source_shape"]),
+    "R420ScatterLifecycle": ("CurrentMain.R420ScatterLifecycle", [
+        "original_excludes_temp", "exporter_window_binding", "raw_shape", "raw_domains",
+        "source_rows_no_duplicates", "decode_roundtrip", "ordered_window_binding",
+        "decoded_bounds", "windows_well_formed", "windows_nonempty", "exact_lifecycle",
+        "final_temp_zero", "original_coordinate", "original_registers",
+        "sources_helpers_preserved", "incoming_temp_independent", "clean_temp_restored"]),
+}
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def sha(path):
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def validate_inventory(manifest):
+    require([row["path"] for row in manifest["repository_inputs"]] == SOURCE_PATHS,
+            "exact three-source inventory required")
+    require(manifest["word"] == SOURCE_PATHS[0] and manifest["core_manifest"] == SOURCE_PATHS[2],
+            "fixed word/core manifest paths required")
+    require([row["name"] for row in manifest["modules"]] == list(REQUIRED_PROBES),
+            "exact four-module inventory required")
+    for row in manifest["modules"]:
+        namespace, names = REQUIRED_PROBES[row["name"]]
+        require(row["probes"] == [namespace + "." + name for name in names],
+                f"required probe inventory: {row['name']}")
+
+
+def render_data(word):
+    """Exact source projection; no repository generator or supplier is run."""
+    require(type(word["v"]) is int and word["v"] == 120, "R420 port count")
+    require(type(word["R"]) is int and word["R"] == 420, "R420 helper count")
+    require(len(word["ret"]) == 9 and len(word["scatter"]) == 120, "R420 shape")
+    require(all(type(x) is int and 240 <= x < 660 for x in word["ret"]), "retained domain")
+    require(all(type(row) is list and all(type(k) is int and 0 <= k < 9 for k in row)
+                for row in word["scatter"]), "scatter domain")
+    nat_list = lambda xs: "[" + ", ".join(map(str, xs)) + "]"
+    rows = ",\n  ".join(nat_list(row) for row in word["scatter"])
+    windows = [(q, [120 + t for t, row in enumerate(word["scatter"]) if k in row])
+               for k, q in enumerate(word["ret"])]
+    window_rows = ",\n  ".join(f"({q}, {nat_list(ds)})" for q, ds in windows)
+    return ("import Init\n\n"
+            "/-! Literal projection of the pinned PR543 R420 word. Generated by check.py's\n"
+            "render_data; checked against the source before every build. Supplier:\n"
+            "eumemic, with substantial Anthropic Claude assistance; Apache-2.0. -/\n"
+            "namespace CurrentMain.R420ScatterData\n"
+            "set_option Elab.async false\n"
+            f"def v : Nat := {word['v']}\n"
+            f"def R : Nat := {word['R']}\n"
+            f"def ret : List Nat := {nat_list(word['ret'])}\n"
+            f"def scatter : List (List Nat) := [{rows}]\n\n"
+            "/-- Exact retained-major membership loop in the pinned record exporter. -/\n"
+            f"def exportedWindows : List (Nat × List Nat) := [{window_rows}]\n\n"
+            "theorem source_shape : v = 120 ∧ R = 420 ∧ 2*v+R = 660 ∧\n"
+            "    ret.length = 9 ∧ scatter.length = 120 ∧\n"
+            "    (scatter.map List.length).foldl Nat.add 0 = 568 := by decide +kernel\n"
+            "end CurrentMain.R420ScatterData\n"
+            "#print axioms CurrentMain.R420ScatterData.source_shape\n")
+
+
+def bind(repo):
+    manifest = json.loads((PACKAGE / "MANIFEST.json").read_text())
+    validate_inventory(manifest)
+    for item in manifest["repository_inputs"]:
+        require(sha(repo / item["path"]) == item["sha256"], f"source hash: {item['path']}")
+    raw = gzip.decompress((repo / manifest["word"]).read_bytes())
+    require(hashlib.sha256(raw).hexdigest() == manifest["decoded_word_sha256"], "decoded word hash")
+    word = json.loads(raw)
+    require((PACKAGE / "R420ScatterData.lean").read_bytes() == render_data(word).encode(),
+            "R420 Lean data differs from exact source projection")
+    for module in manifest["modules"]:
+        path = PACKAGE / (module["name"] + ".lean")
+        require(sha(path) == module["sha256"], f"Lean source hash: {path.name}")
+        source = path.read_text()
+        require(re.findall(r"^import (\S+)$", source, re.M) == module["imports"],
+                f"imports: {path.name}")
+        require(re.findall(r"^#print axioms (\S+)$", source, re.M) == module["probes"],
+                f"probe declarations: {path.name}")
+    return manifest
+
+
+def check_core(repo, lean, manifest):
+    core_path = repo / manifest["core_manifest"]
+    require(sha(core_path) == CORE_MANIFEST_SHA, "official core manifest")
+    core = json.loads(core_path.read_text())
+    root = lean.parent.parent
+    require(sha(lean) == core["binary"]["sha256"], "official Lean binary")
+    require(len(core["ordered_modules"]) == 317, "official Init closure size")
+    for module in core["ordered_modules"]:
+        for kind in ("source", "object"):
+            record = module[kind]
+            path = root / record["file"]
+            require(path.stat().st_size == record["bytes"] and sha(path) == record["sha256"],
+                    f"official core {kind}: {module['module']}")
+
+
+def limits():
+    os.setsid()
+    resource.setrlimit(resource.RLIMIT_AS, (4 * 1024**3, 4 * 1024**3))
+    resource.setrlimit(resource.RLIMIT_CPU, (60, 62))
+
+
+def compile_modules(lean, build, manifest):
+    validate_inventory(manifest)
+    require(not build.exists(), "build directory must not already exist")
+    build.mkdir(parents=True)
+    env = {"PATH": str(lean.parent) + ":/usr/bin:/bin", "HOME": str(build),
+           "LEAN_PATH": str(build), "LANG": "C.UTF-8"}
+    receipts = []
+    for module in manifest["modules"]:
+        name = module["name"]
+        source = build / (name + ".lean")
+        shutil.copyfile(PACKAGE / source.name, source)
+        started = time.monotonic()
+        command = [str(lean), "-s", "65536", "-j", "1", "-o", name + ".olean", source.name]
+        with (build / (name + ".log")).open("wb") as log:
+            process = subprocess.Popen(command, cwd=build, env=env, stdout=log,
+                                       stderr=subprocess.STDOUT, preexec_fn=limits)
+            try:
+                code = process.wait(timeout=60)
+            except subprocess.TimeoutExpired:
+                os.killpg(process.pid, signal.SIGKILL)
+                process.wait()
+                raise ValueError(f"Lean timed out: {name}") from None
+        elapsed = time.monotonic() - started
+        text = (build / (name + ".log")).read_text()
+        require(code == 0, f"Lean failed: {name}; see {name}.log")
+        records = []
+        pattern = r"'([^']+)' (?:does not depend on any axioms|depends on axioms: \[([^\]]*)\])"
+        for match in re.finditer(pattern, text, re.S):
+            axioms = [] if match[2] is None else [x.strip() for x in match[2].split(",") if x.strip()]
+            require(set(axioms) <= STANDARD_AXIOMS, f"nonstandard axioms: {match[1]}")
+            records.append({"declaration": match[1], "axioms": axioms})
+        require([x["declaration"] for x in records] == module["probes"], f"missing/reordered probes: {name}")
+        require(sha(source) == module["sha256"], f"changed build source: {name}")
+        receipts.append({"module": name, "seconds": round(elapsed, 6), "probes": records,
+                         "source_sha256": sha(source), "object_sha256": sha(build / (name + ".olean")),
+                         "log_sha256": sha(build / (name + ".log"))})
+    return receipts
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--repo", type=Path, default=PACKAGE.parents[1])
+    parser.add_argument("--lean", type=Path)
+    parser.add_argument("--build-dir", type=Path)
+    parser.add_argument("--bind-only", action="store_true")
+    args = parser.parse_args()
+    manifest = bind(args.repo.resolve())
+    if args.bind_only:
+        print("PASS source binding; Lean compilation not requested")
+        return
+    require(args.lean is not None and args.build_dir is not None, "--lean and --build-dir required")
+    lean, build = args.lean.resolve(), args.build_dir.resolve()
+    check_core(args.repo.resolve(), lean, manifest)
+    receipts = compile_modules(lean, build, manifest)
+    bind(args.repo.resolve())
+    check_core(args.repo.resolve(), lean, manifest)
+    result = {"status": "PASS", "lean": "4.21.0", "modules": len(receipts),
+              "probes": sum(len(row["probes"]) for row in receipts),
+              "manifest_sha256": sha(PACKAGE / "MANIFEST.json"), "receipts": receipts}
+    (build / "RESULT.json").write_text(json.dumps(result, indent=2) + "\n")
+    print(f"PASS {result['modules']} fresh modules, {result['probes']} standard-axiom probes")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/research/r420-scatter-lifecycle/test_binding.py b/research/r420-scatter-lifecycle/test_binding.py
new file mode 100644
index 0000000000..0b74729a9f
--- /dev/null
+++ b/research/r420-scatter-lifecycle/test_binding.py
@@ -0,0 +1,105 @@
+"""Negative controls for source correspondence, independently of Lean execution."""
+import hashlib
+import json
+from pathlib import Path
+import shutil
+import tempfile
+import unittest
+
+import check
+
+
+class BindingTests(unittest.TestCase):
+    def setUp(self):
+        self.original = check.PACKAGE
+        self.temp = tempfile.TemporaryDirectory()
+        self.repo = Path(self.temp.name) / "repo"
+        self.package = self.repo / "research/r420-scatter-lifecycle"
+        self.package.mkdir(parents=True)
+        for source in [*self.original.glob("*.lean"), self.original / "MANIFEST.json"]:
+            shutil.copyfile(source, self.package / source.name)
+        self.manifest = json.loads((self.package / "MANIFEST.json").read_text())
+        for row in self.manifest["repository_inputs"]:
+            destination = self.repo / row["path"]
+            destination.parent.mkdir(parents=True, exist_ok=True)
+            shutil.copyfile(self.original.parents[1] / row["path"], destination)
+        check.PACKAGE = self.package
+
+    def tearDown(self):
+        check.PACKAGE = self.original
+        self.temp.cleanup()
+
+    def data_mutation(self, before, after):
+        path = self.package / "R420ScatterData.lean"
+        text = path.read_text()
+        self.assertIn(before, text)
+        path.write_text(text.replace(before, after, 1))
+        # Refreshing the local source hash must not defeat source correspondence.
+        for row in self.manifest["modules"]:
+            if row["name"] == "R420ScatterData":
+                row["sha256"] = hashlib.sha256(path.read_bytes()).hexdigest()
+        (self.package / "MANIFEST.json").write_text(json.dumps(self.manifest))
+        with self.assertRaisesRegex(ValueError, "exact source projection"):
+            check.bind(self.repo)
+
+    def test_valid_relocated_inputs(self):
+        self.assertEqual(len(check.bind(self.repo)["modules"]), 4)
+
+    def test_missing_module_inventory(self):
+        original = self.manifest["modules"]
+        for incomplete in ([], original[:-1]):
+            with self.subTest(modules=len(incomplete)):
+                self.manifest["modules"] = incomplete
+                (self.package / "MANIFEST.json").write_text(json.dumps(self.manifest))
+                with self.assertRaisesRegex(ValueError, "four-module inventory"):
+                    check.bind(self.repo)
+
+    def test_missing_lifecycle_probe(self):
+        self.manifest["modules"][-1]["probes"].remove("CurrentMain.R420ScatterLifecycle.exact_lifecycle")
+        (self.package / "MANIFEST.json").write_text(json.dumps(self.manifest))
+        with self.assertRaisesRegex(ValueError, "required probe inventory"):
+            check.bind(self.repo)
+
+    def test_missing_exporter_input(self):
+        self.manifest["repository_inputs"].pop(1)
+        (self.package / "MANIFEST.json").write_text(json.dumps(self.manifest))
+        with self.assertRaisesRegex(ValueError, "three-source inventory"):
+            check.bind(self.repo)
+
+    def test_redirected_word_path(self):
+        self.manifest["word"] = self.manifest["repository_inputs"][1]["path"]
+        (self.package / "MANIFEST.json").write_text(json.dumps(self.manifest))
+        with self.assertRaisesRegex(ValueError, "fixed word/core manifest paths"):
+            check.bind(self.repo)
+
+    def test_retained_order_even_with_refreshed_hash(self):
+        self.data_mutation("[603, 568, 597", "[568, 603, 597")
+
+    def test_scatter_index_with_same_shape(self):
+        self.data_mutation("def scatter : List (List Nat) := [[0, 1]",
+                           "def scatter : List (List Nat) := [[0, 2]")
+
+    def test_exported_destination_order_with_same_count(self):
+        self.data_mutation("(603, [120, 121, 122", "(603, [121, 120, 122")
+
+    def test_proof_source_change(self):
+        path = self.package / "R420ScatterLifecycle.lean"
+        path.write_text(path.read_text().replace("def temp : Register := ⟨660,", "def temp : Register := ⟨659,"))
+        with self.assertRaisesRegex(ValueError, "Lean source hash"):
+            check.bind(self.repo)
+
+    def test_changed_exporter(self):
+        path = self.repo / "research/e8-bit-carrier-skeleton/code/bit/export_records.py"
+        path.write_bytes(path.read_bytes().replace(b"if k in row:", b"if k not in row:"))
+        with self.assertRaisesRegex(ValueError, "source hash"):
+            check.bind(self.repo)
+
+    def test_changed_generic_semantics(self):
+        path = self.package / "BitCopyScatterWindow.lean"
+        path.write_text(path.read_text().replace("then false else s r", "then true else s r"))
+        with self.assertRaisesRegex(ValueError, "Lean source hash"):
+            check.bind(self.repo)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/research/r420-scatter-lifecycle/test_kernel_rejection.py b/research/r420-scatter-lifecycle/test_kernel_rejection.py
new file mode 100644
index 0000000000..7eb8776855
--- /dev/null
+++ b/research/r420-scatter-lifecycle/test_kernel_rejection.py
@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+"""Confirm that a missing lifecycle proof is rejected after Lean compilation."""
+import argparse
+import hashlib
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+
+
+def main():
+    package = Path(__file__).resolve().parent
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--lean", type=Path, required=True)
+    parser.add_argument("--repo", type=Path, default=package.parents[1])
+    parser.add_argument("--output-dir", type=Path, required=True)
+    args = parser.parse_args()
+    output = args.output_dir.resolve()
+    if output.exists():
+        raise ValueError("output directory must not already exist")
+    changed = output / "package"
+    changed.mkdir(parents=True)
+    for source in [*package.glob("*.lean"), package / "check.py", package / "MANIFEST.json"]:
+        shutil.copyfile(source, changed / source.name)
+    source = changed / "R420ScatterLifecycle.lean"
+    text = source.read_text()
+    original = ":=\n  BitCopyScatter.runWindows_eq_clear_direct temp windows windows_nonempty windows_well_formed s"
+    if text.count(original) != 1:
+        raise ValueError("expected exactly one lifecycle proof to replace")
+    source.write_text(text.replace(original, ":= by sorry"))
+    manifest_path = changed / "MANIFEST.json"
+    manifest = json.loads(manifest_path.read_text())
+    manifest["modules"][-1]["sha256"] = hashlib.sha256(source.read_bytes()).hexdigest()
+    manifest_path.write_text(json.dumps(manifest, indent=2) + "\n")
+    # Keep every statement and probe. Refreshing the source hash forces the
+    # acceptance decision to depend on Lean's reachable axiom report.
+    command = [sys.executable, str(changed / "check.py"), "--repo", str(args.repo.resolve()),
+               "--lean", str(args.lean.resolve()), "--build-dir", str(output / "build")]
+    result = subprocess.run(command, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, timeout=300)
+    (output / "checker.log").write_bytes(result.stdout)
+    log = output / "build/R420ScatterLifecycle.log"
+    expected = b"nonstandard axioms: CurrentMain.R420ScatterLifecycle.exact_lifecycle"
+    if result.returncode == 0 or expected not in result.stdout or not log.exists() or "sorryAx" not in log.read_text():
+        raise ValueError("missing-proof negative control did not reach the expected axiom rejection")
+    summary = {"status": "PASS", "control": "exact_lifecycle proof replaced by sorry",
+               "checker_exit": result.returncode, "rejection": expected.decode(),
+               "lean_log_sha256": hashlib.sha256(log.read_bytes()).hexdigest()}
+    (output / "NEGATIVE_RESULT.json").write_text(json.dumps(summary, indent=2) + "\n")
+    print("PASS missing lifecycle proof rejected through sorryAx after compilation")
+
+
+if __name__ == "__main__":
+    main()