Independent verification: check R420 Lean source expressions

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.

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"
+}

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.

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"
+    }
+  }
+}

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.