diff --git a/research/r420-lean-source-binding/CLAIM.md b/research/r420-lean-source-binding/CLAIM.md
new file mode 100644
index 0000000000..07aa6cec40
--- /dev/null
+++ b/research/r420-lean-source-binding/CLAIM.md
@@ -0,0 +1,18 @@
+# Independent source-expression audit
+
+- Track: independent verification; OS-random assignment seed **75**.
+- Base: `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`.
+- Started: 2026-10-13 06:35 UTC. Target finish: 07:50 UTC, reserving the final quarter for verification and handoff.
+- Object: the external correspondence between PR612's literal/derived Lean data and PR543's historical R420 circuit, including the inherited PR590 data.
+- Method: independently tokenize the restricted source grammar, require the actual alias and derived expressions, reconstruct the seven ordered fields, and compare them with the supplier payload. Exercise expressions ignored by the historical correspondence script.
+- Deliverable: a portable, fail-closed checker, reproducible controls, source pins and a concise scope statement. No new kappa or Lean kernel replay is proposed.
+
+The three candidates were (1) a separate prime-power cyclic-inverse identity engine, rejected because #621/#668/#796/#804/#820 already cover the natural independent methods; (2) the R420 Lean-to-supplier correspondence, chosen after narrowing it to expressions that the historical audit does not read; and (3) packed selected-bit finite verification, rejected because #735/#763/#773 already audit the guards and carry behavior. Seed 75 selected the verification track and favored an older formal-interface dependency rather than the latest frontier.
+
+The repository ledger and `im-cold617-formal-binding.py` already record successful R420 literal correspondence. This work does not claim first verification. The bounded hypothesis is that a restricted source parser can detect changes to aliases and derived expressions that its predecessor's separate literal extraction leaves unchecked. Such a mutation is not a counterexample to the original circuit or to the complete hash-pinned Lean build.
+
+No pinned coordination issue was found (the open Discussions request #650 is unrelated). The claim is local. Overlap searches included PR612, source correspondence, independent verification, cyclic inverses and packed-bit audits. Workers stay within the chosen parser, controls and review scope.
+
+Final overlap refresh covered new arrivals through #833 and focused searches for PR612/source correspondence. No matching source-expression audit was found. Main advanced to `f567884aeb8851b6e794af1184119a3bfbe1e631`; all nine consumed/context source files are unchanged. The package retains its exact original base. Outcome: all 13 fields match, six altered expressions expose the historical check's narrower coverage, and the new checker rejects all 33 negative cases. See VALIDATION.md for the checks and limitations.
+
+Submitted as [PR #834](https://github.com/CrocSwap/integer-mult-bounds/pull/834). The contribution is complete for external review; maintainer acceptance and hosted workflow approval are separate.
diff --git a/research/r420-lean-source-binding/EXPECTED.json b/research/r420-lean-source-binding/EXPECTED.json
new file mode 100644
index 0000000000..c4b15c21ce
--- /dev/null
+++ b/research/r420-lean-source-binding/EXPECTED.json
@@ -0,0 +1,37 @@
+{
+  "B_gates": 837,
+  "B_operands": 1077,
+  "committed_compressed_sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784",
+  "decoded_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2",
+  "fields": [
+    "B",
+    "R",
+    "coords",
+    "final",
+    "form",
+    "format",
+    "frames",
+    "h",
+    "lines",
+    "ret",
+    "scatter",
+    "start",
+    "v"
+  ],
+  "frames": 672,
+  "projection_sha256": "146b60c61652c52d8b197ed2f2caf9b9ba11bd8c3c5ed9e07c04d8c27bea92e6",
+  "scatter_terms": 568,
+  "source_manifest_sha256": "ee1d5de6c0edade0688c5730ef154a91830cb1f20a6791a675225b310529c16a",
+  "source_sha256": {
+    "research/community-cold617-audit/im-cold617-formal-binding.py": "73e8a29f02d66243923f9754ab4df0d4f4bb75a1cd465566da1e4f836bfa18e0",
+    "research/community-cold617-audit/pr612/lean/SOURCE-CORRESPONDENCE.json": "28d22002baeb35edfd303ec3192e0b74407999476a5a0963ad83d57d8f73a210",
+    "research/community-cold617-audit/pr612/lean/SelectedBitCarrierBoundaryData.lean": "0a784ff0b77bdb865161c5cd246e10c81e60da1de66f2bb92a75c1b233f8b6e9",
+    "research/community-cold617-audit/pr612/lean/SelectedBitCarrierPhaseBData.lean": "c864011bf19cff4e83d01dfc5f46d3af38c968a15a49b55624186e2079d9758a",
+    "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784",
+    "research/lean-current-r420-boundary-interfaces/CurrentR420BoundaryData.lean": "123b45657d8f5b1fb07a9c238c49230bb99dc0a7a65b7fd6bc5717a234f6f509",
+    "research/lean-current-r420-boundary-interfaces/CurrentR420PhaseBXor.lean": "5ab8ca016e7e53de76b13ef553fe85412d7c9100b30851fa4a81c31ad77d1c11",
+    "research/lean-current-r420-boundary-interfaces/DEPENDENCIES.json": "383b60b7508e014727bb01ed2657518ec0acec7beead402d45355d95a1511378",
+    "research/lean-current-r420-boundary-interfaces/SOURCE_BINDING.json": "4b396bc7316f54f4a50d439ae9d404a3b0f9b58f5626b67c6f9ab72325b7e997"
+  },
+  "status": "PASS_R420_LEAN_SOURCE_EXPRESSIONS"
+}
diff --git a/research/r420-lean-source-binding/README.md b/research/r420-lean-source-binding/README.md
new file mode 100644
index 0000000000..a6fe3917f2
--- /dev/null
+++ b/research/r420-lean-source-binding/README.md
@@ -0,0 +1,44 @@
+# R420 Lean source-expression audit
+
+This independently checks the external correspondence between PR612's Lean data and PR543's historical R420 supplier. The existing maintainer audit already confirmed the seven data fields. This package additionally checks the **actual alias and derived expressions** used to assemble those fields, and makes the check portable.
+
+The historical [`im-cold617-formal-binding.py`](../community-cold617-audit/im-cold617-formal-binding.py) extracts three B-gate lists and concatenates them itself. It does not read the Lean definition of `phaseB`. It similarly constructs `start` itself and assumes the recorded frame, final and inherited-data expressions. Thus its external comparison can pass after some of those Lean expressions change. This is a limitation of that standalone audit, not a defect found in the original circuit or a bypass of PR612's hash-pinned Lean build.
+
+## Reproduce
+
+From the repository root, using Python 3.11+ and its standard library:
+
+```sh
+python -I -B research/r420-lean-source-binding/verify.py
+python -I -B research/r420-lean-source-binding/test_binding.py
+```
+
+Both commands also support Python's `-O` mode. They read the existing source files and create no repository outputs by default. No Lean installation, supplier execution or network is required.
+
+Expected verifier output:
+
+```text
+PASS_R420_LEAN_SOURCE_EXPRESSIONS fields=13 frames=672 gates=837 operands=1077
+```
+
+The verifier compares its complete deterministic report against [EXPECTED.json](EXPECTED.json). The test command passes 13 tests, including 33 distinct negative cases. Six demonstrate changes accepted by the assertion-enabled historical script: `start` offset, B-band order, the `lines`/`frames`/`scatter` reversals, and the `final` prefix length. The revised semantic checks reject them independently of source-hash admission. Other controls cover malformed declarations, constructors, indices, order, multiplicity and JSON types; unchanged inputs, nested comments and recompression pass.
+
+## What the comparison establishes
+
+The checker has its own restricted tokenizer and literal parser; it imports neither the supplier nor the historical audit. It accepts only the recorded forms of the imported aliases and derived expressions. This deliberately small grammar is **not a general Lean interpreter**. A semantically equivalent source rewrite can require a reviewed parser update.
+
+It reconstructs and compares all seven ordered fields: 120 line labels, the 672-frame table through its explicit permutation, both 660-entry endpoint arrays, nine retained helper identifiers, all 837 B gates including their 1,077 operand occurrences, and all 120 scatter rows with 568 index occurrences. Order and multiplicity are preserved even where a weaker scalar check could ignore them. The inherited PR590 frame/line/scatter data are read from the maintainer's retained source files; their historical 489-helper instance is not substituted for the R420 instance.
+
+The six scalar/domain fields `h`, `v`, `R`, `format`, `form` and `coords` are also compared, giving 13 fields in total. The checker does not interpret the supplier's other fields or prove the meanings of those metadata labels.
+
+Source pins identify the exact base and consumed files. The original gzip container remains pinned as an immutable input. An alternate compression of the identical decompressed payload can be checked without requiring the same gzip header or stream.
+
+Use `--word /path/to/recompressed.json.gz` for that comparison, `--root /path/to/checkout` for a different source root, or `--json` to print the checked report. The default root is derived from the checker's location.
+
+## Boundary and attribution
+
+This is an independent external source audit, not a new Lean theorem or a fresh kernel build. The source equality and prior Lean results remain separate pieces of evidence. The full A/C cleanup, D compensation, current COPY/ERASE lifecycle, physical frame transport, hosting and all-size multiplication transfer remain outside this package. No new kappa, current-frontier applicability, runtime improvement or complete multiplication proof is claimed.
+
+The base is `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`. PR612 and its PR590 dependencies are James Chang's (`jamesyc`) formalization, with disclosed OpenAI assistance. PR543 is eumemic's R420 supplier, with disclosed Anthropic Claude assistance and its retained predecessor lineage. Douglas R. Colkitt's maintainer audit supplies the prior correspondence script and receipt. Their original files and notices are unchanged.
+
+Prepared for **Chinmay Arvind (@chinmayarvind23)** with substantial **OpenAI Codex assistance** in implementation, controls, review and writing. Licensed under the repository's Apache-2.0 license. Automated agent review is not independent human peer review. See [CLAIM.md](CLAIM.md) for task selection and overlap, [SOURCES.json](SOURCES.json) for pins, and [VALIDATION.md](VALIDATION.md) for measured checks and limitations.
diff --git a/research/r420-lean-source-binding/SOURCES.json b/research/r420-lean-source-binding/SOURCES.json
new file mode 100644
index 0000000000..9fa149a622
--- /dev/null
+++ b/research/r420-lean-source-binding/SOURCES.json
@@ -0,0 +1,45 @@
+{
+  "base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261",
+  "decoded_word_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2",
+  "files": {
+    "research/community-cold617-audit/im-cold617-formal-binding.py": "73e8a29f02d66243923f9754ab4df0d4f4bb75a1cd465566da1e4f836bfa18e0",
+    "research/community-cold617-audit/pr612/lean/SOURCE-CORRESPONDENCE.json": "28d22002baeb35edfd303ec3192e0b74407999476a5a0963ad83d57d8f73a210",
+    "research/community-cold617-audit/pr612/lean/SelectedBitCarrierBoundaryData.lean": "0a784ff0b77bdb865161c5cd246e10c81e60da1de66f2bb92a75c1b233f8b6e9",
+    "research/community-cold617-audit/pr612/lean/SelectedBitCarrierPhaseBData.lean": "c864011bf19cff4e83d01dfc5f46d3af38c968a15a49b55624186e2079d9758a",
+    "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784",
+    "research/lean-current-r420-boundary-interfaces/CurrentR420BoundaryData.lean": "123b45657d8f5b1fb07a9c238c49230bb99dc0a7a65b7fd6bc5717a234f6f509",
+    "research/lean-current-r420-boundary-interfaces/CurrentR420PhaseBXor.lean": "5ab8ca016e7e53de76b13ef553fe85412d7c9100b30851fa4a81c31ad77d1c11",
+    "research/lean-current-r420-boundary-interfaces/DEPENDENCIES.json": "383b60b7508e014727bb01ed2657518ec0acec7beead402d45355d95a1511378",
+    "research/lean-current-r420-boundary-interfaces/SOURCE_BINDING.json": "4b396bc7316f54f4a50d439ae9d404a3b0f9b58f5626b67c6f9ab72325b7e997"
+  },
+  "format": "r420-lean-source-binding-v1",
+  "git_blobs_at_base": {
+    "research/community-cold617-audit/im-cold617-formal-binding.py": "4ac7c097c3d091c1ba612152dc2dd2808773b6a5",
+    "research/community-cold617-audit/pr612/lean/SOURCE-CORRESPONDENCE.json": "426390e631b1293e24ab61805afc47c769bf8fe8",
+    "research/community-cold617-audit/pr612/lean/SelectedBitCarrierBoundaryData.lean": "e2b5637e2709fbd2011cf058abd4246d5e29f7ce",
+    "research/community-cold617-audit/pr612/lean/SelectedBitCarrierPhaseBData.lean": "ff7e3304638c696e43ae53c5b5a93740a8d96492",
+    "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "0c63ca62759dc63d302be6552aeeee1ede70350f",
+    "research/lean-current-r420-boundary-interfaces/CurrentR420BoundaryData.lean": "bd1ed3b06c1eb089dc5d76cdbd582d536dd1368e",
+    "research/lean-current-r420-boundary-interfaces/CurrentR420PhaseBXor.lean": "573423b0ab0a67caa2e52adf698f33ed0b88083e",
+    "research/lean-current-r420-boundary-interfaces/DEPENDENCIES.json": "9bd26559e90505d7b891a3b4ce7d295300710ccb",
+    "research/lean-current-r420-boundary-interfaces/SOURCE_BINDING.json": "4a0589d97cb4575b324eba6ab89eb5a791120b6d"
+  },
+  "scope": "Seven structured fields plus six scalar/domain fields of historical R420 source correspondence. No frontier transport or new Lean kernel evidence.",
+  "source_prs": {
+    "543": {
+      "author": "eumemic",
+      "commit": "2065fe4f72a914d907f1046603f5a36f17018535",
+      "role": "historical R420 supplier"
+    },
+    "590": {
+      "author": "jamesyc",
+      "commit": "58690bdbb587f482569ba1bdf7bf61a5396b4768",
+      "role": "retained carrier data; two consumed modules pinned below"
+    },
+    "612": {
+      "author": "jamesyc",
+      "commit": "ce37f3ce35ba8891771e01492b3a21978763bebb",
+      "role": "R420 formal boundary package"
+    }
+  }
+}
diff --git a/research/r420-lean-source-binding/VALIDATION.md b/research/r420-lean-source-binding/VALIDATION.md
new file mode 100644
index 0000000000..1218e2c14c
--- /dev/null
+++ b/research/r420-lean-source-binding/VALIDATION.md
@@ -0,0 +1,37 @@
+# Validation
+
+Executed on 2026-10-13 using CPython 3.12.15 on Linux in the official image
+`python@sha256:a6e34c598f2467ed0e9a8d349809fcd8b5c603269512df273a0bb1784edc11b1`.
+Containers had no network, a read-only checkout and root filesystem, no Linux
+capabilities, no privilege escalation, two CPUs, 1 GiB memory and 64 PIDs.
+Temporary test files used a bounded writable `/tmp`.
+
+- The verifier reproduced all 13 fields and the complete expected receipt.
+- All 13 tests passed normally and with `-I -O -B`. They contain 33 distinct
+  negative cases: six historical false positives, one checked-literal change,
+  14 source-grammar cases, seven order/multiplicity cases and five JSON cases.
+- Each historical false positive runs the original R420 portion of the
+  maintainer script with only three local path substitutions. Its assertions
+  are explicitly retained even in optimized Python. A separate rejected
+  literal mutation confirms that those assertions run.
+- Source-expression controls bypass hash admission, so their rejection
+  exercises the parser and exact comparison. They do not claim the changed
+  Lean modules compile or evade the formal package's source hashes.
+- Unchanged sources, nested comments and a different gzip encoding of the
+  identical payload pass. Every consumed file matches its base Git blob.
+- A minimal relocated tree, without Git or the original absolute paths,
+  passes. Six release corruptions fail: changed Lean source, expected receipt,
+  manifest provenance, omitted source pin, historical checker and gzip payload.
+  Restoring the minimal tree passes again.
+- The selected-record integrity check passed at this base for
+  `1661202643272239/1000000000000000000`. Staged files match working bytes
+  exactly, and `git diff --cached --check` passes.
+
+Review caught and corrected a lexer issue and an initially permissive
+list/tuple conversion before the final runs. Explicit Fin constructors and
+gate tuples now have rejection controls. Separate automated review found no
+remaining blocking issue; this is not human peer review.
+
+No fresh Lean kernel build, supplier cold replay, repository-wide `make verify`,
+remote CI result or full multiplication theorem is claimed. All changes are
+standalone additions; no historical source, frontier or `upstream/` file changes.
diff --git a/research/r420-lean-source-binding/test_binding.py b/research/r420-lean-source-binding/test_binding.py
new file mode 100644
index 0000000000..2afde53220
--- /dev/null
+++ b/research/r420-lean-source-binding/test_binding.py
@@ -0,0 +1,205 @@
+#!/usr/bin/env python3
+"""Regression checks for the historical external R420 source correspondence.
+
+Only the R420 prefix of the pinned historical Python script is executed, with
+three local directory substitutions. Its assertions are retained even under -O.
+These tests make no claim that mutated Lean files pass Lean kernel checking.
+Run this repository code in the same restricted environment as verify.py.
+"""
+
+import copy
+import gzip
+import importlib.util
+import json
+from pathlib import Path
+import tempfile
+import unittest
+import warnings
+
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+CURRENT = Path("research/lean-current-r420-boundary-interfaces")
+OLD = Path("research/community-cold617-audit/pr612/lean")
+WORD = Path("research/e8-bit-r420/data/bitE8mut-r420.json.gz")
+HISTORICAL = Path("research/community-cold617-audit/im-cold617-formal-binding.py")
+CURRENT_FILE = "CurrentR420BoundaryData.lean"
+BOUNDARY_FILE = "SelectedBitCarrierBoundaryData.lean"
+PHASE_FILE = "SelectedBitCarrierPhaseBData.lean"
+
+spec = importlib.util.spec_from_file_location("r420_binding", HERE / "verify.py")
+binding = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(binding)
+
+
+def replace_once(text, old, new):
+    if text.count(old) != 1:
+        raise ValueError("mutation anchor must occur exactly once: " + old)
+    return text.replace(old, new, 1)
+
+
+class SourceCorrespondenceTests(unittest.TestCase):
+    @classmethod
+    def setUpClass(cls):
+        binding.audit(ROOT)  # Pin the historical code before executing it.
+        cls.current = (ROOT / CURRENT / CURRENT_FILE).read_text(encoding="utf-8")
+        cls.boundary = (ROOT / OLD / BOUNDARY_FILE).read_text(encoding="utf-8")
+        cls.phase = (ROOT / OLD / PHASE_FILE).read_text(encoding="utf-8")
+        cls.raw = (ROOT / WORD).read_bytes()
+        cls.word = json.loads(gzip.decompress(cls.raw))
+        source = (ROOT / HISTORICAL).read_text(encoding="utf-8")
+        marker = "p=root/'research/lean-current588-native-moment';"
+        if source.count(marker) != 1:
+            raise ValueError("historical R420 prefix boundary changed")
+        cls.prefix = source.split(marker)[0]
+
+    def historical_check(self, current):
+        """Run the actual historical checks; do not reimplement their logic."""
+        with tempfile.TemporaryDirectory(prefix="r420-binding-") as dirname:
+            root = Path(dirname)
+            for relative in (CURRENT, OLD, WORD.parent):
+                (root / relative).mkdir(parents=True, exist_ok=True)
+            (root / CURRENT / CURRENT_FILE).write_text(current, encoding="utf-8")
+            (root / OLD / BOUNDARY_FILE).write_text(self.boundary, encoding="utf-8")
+            (root / OLD / PHASE_FILE).write_text(self.phase, encoding="utf-8")
+            (root / WORD).write_bytes(self.raw)
+            (root / CURRENT / "SOURCE_BINDING.json").write_bytes(
+                (ROOT / CURRENT / "SOURCE_BINDING.json").read_bytes())
+            program = replace_once(
+                self.prefix, "'/tmp/integer-mult-family588'", repr(str(root)))
+            for filename in (BOUNDARY_FILE, PHASE_FILE):
+                program = replace_once(
+                    program, repr("/tmp/im-cold617-replay/lean612-macos/" + filename),
+                    repr(str(root / OLD / filename)))
+            # optimize=0 is essential: the inherited script uses assert.
+            with warnings.catch_warnings():
+                # The retained historical json.load(open(...)) emits this
+                # unrelated warning under unittest; its code stays unchanged.
+                warnings.simplefilter("ignore", ResourceWarning)
+                exec(compile(program, str(ROOT / HISTORICAL), "exec", optimize=0), {})
+            receipt = json.loads((root / OLD / "SOURCE-CORRESPONDENCE.json").read_text())
+            self.assertEqual(receipt["status"], "PASS_LITERAL_R420_SOURCE_CORRESPONDENCE")
+            self.assertEqual(receipt["B_gates"], 837)
+            self.assertEqual(len(receipt["fields"]), 7)
+
+    def semantic_check(self, current):
+        projection = binding.extract_projection(current, self.boundary, self.phase)
+        binding.compare_projection(projection, self.word)
+
+    def demonstrate_missed_change(self, old, new):
+        changed = replace_once(self.current, old, new)
+        self.historical_check(changed)
+        # Deliberately bypass source-hash admission: expression/value checking
+        # itself must reject the altered data, rather than relying on a hash.
+        with self.assertRaises(binding.AuditError):
+            self.semantic_check(changed)
+
+    def test_unmodified_sources_pass_both(self):
+        self.historical_check(self.current)
+        self.semantic_check(self.current)
+
+    def test_start_offset_change_is_missed_by_historical_check(self):
+        self.demonstrate_missed_change("(fun r => r+2)", "(fun r => r+3)")
+
+    def test_phase_band_order_change_is_missed_by_historical_check(self):
+        self.demonstrate_missed_change(
+            "def phaseB := firstTargets ++ sourceMiddle ++ lastTargets",
+            "def phaseB := lastTargets ++ sourceMiddle ++ firstTargets")
+
+    def test_lines_alias_reversal_is_missed_by_historical_check(self):
+        self.assertNotEqual(self.word["lines"], self.word["lines"][::-1])
+        self.demonstrate_missed_change(
+            "abbrev lines := SelectedBitCarrierBoundary.Data.lines",
+            "abbrev lines := SelectedBitCarrierBoundary.Data.lines.reverse")
+
+    def test_frame_map_reversal_is_missed_by_historical_check(self):
+        self.assertNotEqual(self.word["frames"], self.word["frames"][::-1])
+        self.demonstrate_missed_change(
+            "def frames : List (List Nat) := frameOrder.map frameAt",
+            "def frames : List (List Nat) := (frameOrder.map frameAt).reverse")
+
+    def test_scatter_alias_reversal_is_missed_by_historical_check(self):
+        self.assertNotEqual(self.word["scatter"], self.word["scatter"][::-1])
+        self.demonstrate_missed_change(
+            "abbrev scatter := SelectedBitCarrierPhaseB.Data.scatter",
+            "abbrev scatter := SelectedBitCarrierPhaseB.Data.scatter.reverse")
+
+    def test_final_prefix_length_change_is_missed_by_historical_check(self):
+        self.demonstrate_missed_change(
+            "SelectedBitCarrierBoundary.Data.final.take 660",
+            "SelectedBitCarrierBoundary.Data.final.take 659")
+
+    def test_historical_assertions_are_active_even_under_optimized_python(self):
+        changed = replace_once(self.current, "[603, 568, 597, 583,", "[602, 568, 597, 583,")
+        with self.assertRaises(AssertionError):
+            self.historical_check(changed)
+        with self.assertRaises(binding.AuditError):
+            self.semantic_check(changed)
+
+    def test_source_grammar_controls(self):
+        cases = [
+            ("literal_suffix", "def ret : List Nat := [603, 568, 597, 583, 569, 604, 616, 596, 598]", "def ret : List Nat := [603, 568, 597, 583, 569, 604, 616, 596, 598] ++ []"),
+            ("duplicate_declaration", "def R : Nat := 420", "def R : Nat := 420\ndef R : Nat := 420"),
+            ("namespace_shadow", "def R : Nat := 420", "namespace Shadow\ndef R : Nat := 420\nend Shadow"),
+            ("unrecognized_command", "def R : Nat := 420", "set_option maxRecDepth 3000\ndef R : Nat := 420"),
+            ("malformed_fin_proof", "⟨0, by decide⟩", "⟨0, by decide extra⟩"),
+            ("duplicate_frame_index", "⟨0, by decide⟩", "⟨1, by decide⟩"),
+            ("frame_index_out_of_bounds", "⟨0, by decide⟩", "⟨672, by decide⟩"),
+            ("bare_fin_index", "⟨0, by decide⟩", "0"),
+            ("frame_lookup_alias", "SelectedBitCarrierBoundary.Data.frames[i.val]", "SelectedBitCarrierBoundary.Data.frames[0]"),
+            ("phase_missing_band", "def phaseB := firstTargets ++ sourceMiddle ++ lastTargets", "def phaseB := firstTargets ++ lastTargets"),
+            ("trailing_module_command", "end CurrentMain.CurrentR420Boundary.Data", "end CurrentMain.CurrentR420Boundary.Data\nopen CurrentMain"),
+            ("unsupported_character", "def R : Nat := 420", "def R : Nat := 420;"),
+            ("unterminated_comment", "def R : Nat := 420", "def R : Nat := 420 /-"),
+            ("list_as_gate_tuple", "(143, 120, [3])", "[143, 120, [3]]"),
+        ]
+        for name, old, new in cases:
+            with self.subTest(name=name), self.assertRaises(binding.AuditError):
+                self.semantic_check(replace_once(self.current, old, new))
+
+    def test_order_and_multiplicity_controls(self):
+        original = binding.extract_projection(self.current, self.boundary, self.phase)
+        for name, mutate in [
+            ("B_gate_order", lambda p: p["B"].reverse()),
+            ("B_operand_order", lambda p: p["B"][-1][2].reverse()),
+            ("B_operand_multiplicity", lambda p: p["B"][-1][2].extend([5, 5])),
+            ("scatter_order", lambda p: p["scatter"][0].reverse()),
+            ("scatter_multiplicity", lambda p: p["scatter"][0].extend([0, 0])),
+            ("frame_rows_order", lambda p: p["frames"].reverse()),
+            ("retained_order", lambda p: p["ret"].reverse()),
+        ]:
+            altered = copy.deepcopy(original)
+            mutate(altered)
+            with self.subTest(name=name), self.assertRaises(binding.AuditError):
+                binding.compare_projection(altered, self.word)
+
+    def test_json_types_and_keys(self):
+        projection = binding.extract_projection(self.current, self.boundary, self.phase)
+        for field, transform in [
+            ("h", lambda _: 8.0),
+            ("B", lambda v: [[False, *v[0][1:]], *v[1:]]),
+            ("start", lambda v: [*v[:120], False, *v[121:]]),
+        ]:
+            altered = copy.deepcopy(self.word)
+            altered[field] = transform(altered[field])
+            with self.subTest(field=field), self.assertRaises(binding.AuditError):
+                binding.compare_projection(projection, altered)
+        for payload in ('{"h":8,"h":8}', '{"h":NaN}'):
+            with self.subTest(payload=payload), self.assertRaises(binding.AuditError):
+                binding.load_word(payload)
+
+    def test_nested_comments_are_accepted(self):
+        changed = replace_once(self.current, "def R : Nat := 420",
+                               "def /- nested /- def R := 999 -/ comment -/ R : Nat := 420")
+        self.semantic_check(changed)
+
+    def test_recompression_preserves_result(self):
+        with tempfile.TemporaryDirectory(prefix="r420-recompress-") as directory:
+            alternate = Path(directory) / "word.json.gz"
+            alternate.write_bytes(gzip.compress(gzip.decompress(self.raw), compresslevel=1, mtime=75))
+            self.assertNotEqual(alternate.read_bytes(), self.raw)
+            self.assertEqual(binding.audit(ROOT, alternate), binding.audit(ROOT))
+
+
+if __name__ == "__main__":
+    unittest.main(verbosity=2)
diff --git a/research/r420-lean-source-binding/verify.py b/research/r420-lean-source-binding/verify.py
new file mode 100644
index 0000000000..51d84d96ec
--- /dev/null
+++ b/research/r420-lean-source-binding/verify.py
@@ -0,0 +1,330 @@
+#!/usr/bin/env python3
+"""Audit the complete, pinned PR612 data expressions against PR543's payload.
+
+This recognizes a deliberately closed subset of these three Lean data modules.
+It neither executes Lean nor validates proof terms or general Lean expressions.
+No supplier, generator, predecessor checker, or other repository code is imported.
+"""
+import argparse
+import gzip
+import hashlib
+import io
+import json
+from pathlib import Path
+import sys
+
+
+class AuditError(ValueError):
+    pass
+
+
+CURRENT = "research/lean-current-r420-boundary-interfaces/CurrentR420BoundaryData.lean"
+BOUNDARY = "research/community-cold617-audit/pr612/lean/SelectedBitCarrierBoundaryData.lean"
+PHASE = "research/community-cold617-audit/pr612/lean/SelectedBitCarrierPhaseBData.lean"
+WORD_PATH = "research/e8-bit-r420/data/bitE8mut-r420.json.gz"
+EXPECTED_PATHS = {CURRENT, BOUNDARY, PHASE, WORD_PATH,
+    "research/community-cold617-audit/im-cold617-formal-binding.py",
+    "research/community-cold617-audit/pr612/lean/SOURCE-CORRESPONDENCE.json",
+    "research/lean-current-r420-boundary-interfaces/CurrentR420PhaseBXor.lean",
+    "research/lean-current-r420-boundary-interfaces/DEPENDENCIES.json",
+    "research/lean-current-r420-boundary-interfaces/SOURCE_BINDING.json"}
+
+
+def require(ok, message):
+    if not ok:
+        raise AuditError(message)
+
+
+def tokens(text):
+    """Tokenize without searching inside strings or nested Lean comments."""
+    result, i = [], 0
+    while i < len(text):
+        c = text[i]
+        if c.isspace():
+            i += 1
+        elif text.startswith("--", i):
+            end = text.find("\n", i + 2)
+            i = len(text) if end < 0 else end + 1
+        elif text.startswith("/-", i):
+            i, depth = i + 2, 1
+            while i < len(text) and depth:
+                if text.startswith("/-", i):
+                    depth, i = depth + 1, i + 2
+                elif text.startswith("-/", i):
+                    depth, i = depth - 1, i + 2
+                else:
+                    i += 1
+            require(depth == 0, "unterminated Lean comment")
+        elif c == '"':
+            j = i + 1
+            while j < len(text) and text[j] != '"':
+                require(text[j] not in "\\\r\n", "unsupported Lean string escape/newline")
+                j += 1
+            require(j < len(text), "unterminated Lean string")
+            result.append(text[i:j + 1])
+            i = j + 1
+        elif c.isascii() and (c.isalpha() or c == "_"):
+            j = i + 1
+            while j < len(text) and text[j].isascii() and (text[j].isalnum() or text[j] in "_.'"):
+                j += 1
+            result.append(text[i:j])
+            i = j
+        elif c in "0123456789":
+            j = i + 1
+            while j < len(text) and text[j] in "0123456789":
+                j += 1
+            require(j == i + 1 or c != "0", "noncanonical numeral")
+            result.append(text[i:j])
+            i = j
+        elif text[i:i + 2] in (":=", "++", "=>"):
+            result.append(text[i:i + 2])
+            i += 2
+        elif c in "[](),.:+*-×⟨⟩'":
+            result.append(c)
+            i += 1
+        else:
+            raise AuditError(f"unsupported Lean character at offset {i}: {c!r}")
+    return result
+
+
+def module(text, prefix, suffix, names):
+    ts, pre, post = tokens(text), tokens(prefix), tokens(suffix)
+    require(ts[:len(pre)] == pre and ts[-len(post):] == post, "module wrapper differs")
+    ts = ts[len(pre):-len(post)]
+    out, i = {}, 0
+    while i < len(ts):
+        require(ts[i] in ("def", "abbrev") and i + 2 < len(ts), "expected data declaration")
+        kind, name = ts[i:i + 2]
+        require(name not in out, f"duplicate declaration: {name}")
+        i += 2
+        header = []
+        while i < len(ts) and ts[i] != ":=":
+            header.append(ts[i])
+            i += 1
+        require(i < len(ts), f"missing definition body: {name}")
+        i += 1
+        start = i
+        while i < len(ts) and ts[i] not in ("def", "abbrev"):
+            i += 1
+        require(i > start, f"empty definition body: {name}")
+        out[name] = (kind, header, ts[start:i])
+    require(list(out) == names.split(), "declaration names/order differ")
+    return out
+
+
+def rhs(decls, name, header, kind="def"):
+    actual_kind, actual_header, body = decls[name]
+    require(actual_kind == kind and actual_header == tokens(header), f"declaration type differs: {name}")
+    return body
+
+
+def fixed(decls, name, header, expression, kind="def"):
+    require(rhs(decls, name, header, kind) == tokens(expression), f"unsupported expression: {name}")
+
+
+def literal(ts, allow_fin=False):
+    """Recursively consume one entire numeric/string/list/tuple/Fin literal."""
+    i = 0
+
+    def take(expected):
+        nonlocal i
+        require(i < len(ts) and ts[i] == expected, f"expected literal token {expected!r}")
+        i += 1
+
+    def value():
+        nonlocal i
+        require(i < len(ts), "truncated literal")
+        t = ts[i]
+        i += 1
+        if t in ("[", "("):
+            end = "]" if t == "[" else ")"
+            items = []
+            if i < len(ts) and ts[i] != end:
+                items.append(value())
+                while i < len(ts) and ts[i] == ",":
+                    i += 1
+                    items.append(value())
+            take(end)
+            require(t == "[" or len(items) == 3, "only triple tuples are supported")
+            return items if t == "[" else tuple(items)
+        if t == "⟨":
+            require(allow_fin, "Fin constructor outside frameOrder")
+            n = value()
+            require(type(n) is int and 0 <= n < 672, "Fin literal out of bounds")
+            for expected in (",", "by", "decide", "⟩"):
+                take(expected)
+            return ("Fin", n)
+        if t == "-":
+            require(i < len(ts) and ts[i].isascii() and ts[i].isdigit(), "bad negative literal")
+            n = -int(ts[i])
+            i += 1
+            return n
+        if t.startswith('"'):
+            return t[1:-1]
+        require(t.isascii() and t.isdigit(), f"not a supported literal: {t}")
+        return int(t)
+
+    result = value()
+    require(i == len(ts), "trailing expression after literal")
+    return result
+
+
+def gates(ts):
+    value = literal(ts)
+    require(type(value) is list and all(type(g) is tuple and len(g) == 3 for g in value), "expected list of gate tuples")
+    return [list(g) for g in value]
+
+
+def extract_projection(current_text, boundary_text, phase_text):
+    old = module(boundary_text, "import Init namespace CurrentMain.SelectedBitCarrierBoundary.Data",
+                 "end CurrentMain.SelectedBitCarrierBoundary.Data", "h v R format form lines frames start final ret registers")
+    prior = module(phase_text, "import SelectedBitCarrierBoundaryCheck namespace CurrentMain.SelectedBitCarrierPhaseB.Data",
+                   "end CurrentMain.SelectedBitCarrierPhaseB.Data", "phaseB scatter")
+    cur = module(current_text, "import SelectedBitCarrierPhaseBData namespace CurrentMain.CurrentR420Boundary.Data set_option Elab.async false",
+                 "end CurrentMain.CurrentR420Boundary.Data", "h v R registers format form coords lines frameOrder frameAt frames start final ret scatter firstTargets sourceMiddle lastTargets phaseB Reg ExtendedReg embed temporary")
+    old_types = {"h": "Nat", "v": "Nat", "R": "Nat", "format": "String", "form": "String", "lines": "List (List Int)", "frames": "List (List Nat)", "start": "List Nat", "final": "List Nat", "ret": "List Nat"}
+    data = {name: literal(rhs(old, name, ": " + typ)) for name, typ in old_types.items()}
+    fixed(old, "registers", ": Nat", "2*v+R")
+    gates(rhs(prior, "phaseB", ": List (Nat × Nat × List Nat)"))  # Not reused as current B.
+    scatter = literal(rhs(prior, "scatter", ": List (List Nat)"))
+    for name in ("h", "v", "format", "form", "lines"):
+        fixed(cur, name, "", "SelectedBitCarrierBoundary.Data." + name, "abbrev")
+    fixed(cur, "scatter", "", "SelectedBitCarrierPhaseB.Data.scatter", "abbrev")
+    r = literal(rhs(cur, "R", ": Nat"))
+    coords = literal(rhs(cur, "coords", ": String"))
+    fixed(cur, "registers", ": Nat", "2*v+R")
+    order = literal(rhs(cur, "frameOrder", ": List (Fin 672)"), allow_fin=True)
+    require(type(order) is list and all(type(i) is tuple and len(i) == 2 and i[0] == "Fin" for i in order), "expected explicit Fin constructors in frameOrder")
+    order = [i[1] for i in order]
+    require(sorted(order) == list(range(672)), "frameOrder is not the required permutation")
+    fixed(cur, "frameAt", "(i : Fin 672) : List Nat", "SelectedBitCarrierBoundary.Data.frames[i.val]'(by rw [SelectedBitCarrierBoundary.frame_domain.1] exact i.isLt)")
+    fixed(cur, "frames", ": List (List Nat)", "frameOrder.map frameAt")
+    fixed(cur, "start", ": List Nat", "(List.range 120).map (fun r => r+2) ++ List.replicate 540 0")
+    fixed(cur, "final", ": List Nat", "SelectedBitCarrierBoundary.Data.final.take 660")
+    ret = literal(rhs(cur, "ret", ": List Nat"))
+    bands = [gates(rhs(cur, name, ": List (Nat × Nat × List Nat)")) for name in ("firstTargets", "sourceMiddle", "lastTargets")]
+    fixed(cur, "phaseB", "", "firstTargets ++ sourceMiddle ++ lastTargets")
+    fixed(cur, "Reg", "", "Fin 660", "abbrev")
+    fixed(cur, "ExtendedReg", "", "Fin 661", "abbrev")
+    fixed(cur, "embed", "(r : Reg) : ExtendedReg", "⟨r.val, Nat.lt_trans r.isLt (by decide)⟩")
+    fixed(cur, "temporary", ": ExtendedReg", "⟨660, by decide⟩")
+    require(data["h"] == 8 and data["v"] == 120 and type(r) is int and r == 420, "current dimensions differ")
+    require(len(data["frames"]) == 672 and len(data["final"]) >= 660, "historical table dimensions differ")
+    require([len(b) for b in bands] == [120, 597, 120], "B band lengths differ")
+    projection = {k: data[k] for k in ("h", "v", "format", "form", "lines")}
+    projection.update(R=r, coords=coords, frames=[data["frames"][i] for i in order],
+                      start=list(range(2, 122)) + [0] * 540, final=data["final"][:660],
+                      ret=ret, scatter=scatter, B=bands[0] + bands[1] + bands[2])
+    validate_projection(projection)
+    return projection
+
+
+def validate_projection(p):
+    def nat(n, bound):
+        return type(n) is int and 0 <= n < bound
+
+    def rows(value, count, entry):
+        return type(value) is list and len(value) == count and all(type(row) is list and all(entry(x) for x in row) for row in value)
+
+    require(p["h"] == 8 and p["v"] == 120 and p["R"] == 420, "wrong dimensions")
+    require(rows(p["lines"], 120, lambda n: type(n) is int) and all(len(row) == 8 for row in p["lines"]), "invalid line coordinates")
+    require(rows(p["frames"], 672, lambda n: nat(n, 120)), "invalid frames")
+    for field in ("start", "final"):
+        require(type(p[field]) is list and len(p[field]) == 660 and all(nat(n, 672) for n in p[field]), f"invalid {field}")
+    require(type(p["ret"]) is list and len(p["ret"]) == 9 and all(nat(n, 660) and n >= 240 for n in p["ret"]), "invalid retained helpers")
+    require(rows(p["scatter"], 120, lambda n: nat(n, 9)), "invalid scatter")
+    require(type(p["B"]) is list and len(p["B"]) == 837, "invalid B length")
+    for gate in p["B"]:
+        require(type(gate) is list and len(gate) == 3 and nat(gate[0], 672) and nat(gate[1], 660) and type(gate[2]) is list and all(nat(n, 660) for n in gate[2]), "invalid B gate")
+    for key in ("coords", "form", "format"):
+        require(type(p[key]) is str, f"invalid {key}")
+
+
+def compare_projection(projection, word):
+    def equal(a, b, path):
+        require(type(a) is type(b), f"type mismatch at {path}")
+        if type(a) is list:
+            require(len(a) == len(b), f"length mismatch at {path}")
+            for i, (x, y) in enumerate(zip(a, b)):
+                equal(x, y, f"{path}[{i}]")
+        else:
+            require(a == b, f"value mismatch at {path}")
+
+    validate_projection(projection)
+    require(type(word) is dict, "supplier must be a JSON object")
+    for key, value in projection.items():
+        require(key in word, f"missing supplier field: {key}")
+        equal(value, word[key], key)
+
+
+def load_word(raw):
+    def pairs(items):
+        result = {}
+        for key, value in items:
+            require(key not in result, f"duplicate JSON key: {key}")
+            result[key] = value
+        return result
+
+    def constant(value):
+        raise AuditError(f"non-finite JSON constant: {value}")
+
+    return json.loads(raw, object_pairs_hook=pairs, parse_constant=constant)
+
+
+def audit(root, word_path=None):
+    manifest_raw = Path(__file__).with_name("SOURCES.json").read_bytes()
+    manifest = load_word(manifest_raw)
+    require(manifest.get("format") == "r420-lean-source-binding-v1", "wrong source manifest format")
+    pins = manifest.get("files")
+    require(type(pins) is dict and set(pins) == EXPECTED_PATHS, "source manifest paths differ")
+    require(type(manifest.get("git_blobs_at_base")) is dict and set(manifest["git_blobs_at_base"]) == EXPECTED_PATHS, "source git-blob paths differ")
+    texts = {}
+    for relative, expected in pins.items():
+        raw = (Path(root) / relative).read_bytes()
+        require(hashlib.sha256(raw).hexdigest() == expected, f"source hash mismatch: {relative}")
+        blob = hashlib.sha1(f"blob {len(raw)}\0".encode() + raw).hexdigest()
+        require(blob == manifest["git_blobs_at_base"][relative], f"source git blob mismatch: {relative}")
+        if relative in (CURRENT, BOUNDARY, PHASE):
+            texts[relative] = raw.decode("utf-8")
+    source_binding = load_word((Path(root) / "research/lean-current-r420-boundary-interfaces/SOURCE_BINDING.json").read_bytes())
+    payload_hash = manifest.get("decoded_word_sha256")
+    require(source_binding["input"]["decoded_sha256"] == payload_hash and source_binding["input"]["compressed_sha256"] == pins[WORD_PATH], "source context and manifest disagree")
+    raw = (Path(word_path) if word_path is not None else Path(root) / WORD_PATH).read_bytes()
+    compressed_hash = hashlib.sha256(raw).hexdigest()
+    require(len(raw) <= 1024 * 1024, "compressed payload exceeds bound")
+    if word_path is None:
+        require(compressed_hash == pins[WORD_PATH], "committed gzip hash mismatch")
+    with gzip.GzipFile(fileobj=io.BytesIO(raw)) as stream:
+        decoded = stream.read(1024 * 1024 + 1)
+    require(len(decoded) <= 1024 * 1024, "decoded payload exceeds bound")
+    require(hashlib.sha256(decoded).hexdigest() == payload_hash, "decoded payload hash mismatch")
+    projection = extract_projection(texts[CURRENT], texts[BOUNDARY], texts[PHASE])
+    compare_projection(projection, load_word(decoded))
+    canonical = json.dumps(projection, sort_keys=True, separators=(",", ":")).encode()
+    return {"status": "PASS_R420_LEAN_SOURCE_EXPRESSIONS", "fields": sorted(projection),
+            "source_manifest_sha256": hashlib.sha256(manifest_raw).hexdigest(),
+            "source_sha256": pins, "decoded_sha256": payload_hash,
+            "committed_compressed_sha256": pins[WORD_PATH], "projection_sha256": hashlib.sha256(canonical).hexdigest(),
+            "B_gates": len(projection["B"]), "B_operands": sum(len(g[2]) for g in projection["B"]),
+            "frames": len(projection["frames"]), "scatter_terms": sum(map(len, projection["scatter"]))}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--root", type=Path, default=Path(__file__).resolve().parents[2])
+    parser.add_argument("--word", type=Path, help="Alternate gzip encoding; decoded bytes must match the pinned payload.")
+    parser.add_argument("--json", action="store_true", help="Print the deterministic full report.")
+    args = parser.parse_args()
+    try:
+        report = audit(args.root, args.word)
+        expected = load_word(Path(__file__).with_name("EXPECTED.json").read_bytes())
+        require(report == expected, "report differs from EXPECTED.json")
+    except (AuditError, OSError, ValueError, EOFError) as exc:
+        print(f"FAIL_R420_LEAN_SOURCE_EXPRESSIONS: {exc}", file=sys.stderr)
+        return 1
+    print(json.dumps(report, indent=2, sort_keys=True) if args.json else f"{report['status']} fields={len(report['fields'])} frames={report['frames']} gates={report['B_gates']} operands={report['B_operands']}")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())