Independent verification: check R420 Lean source expressions

[chinmayarvind23]

Change and mathematical scope

Independent verification / external source audit; no new kappa.

The existing R420 correspondence script extracts three B-gate lists and concatenates them itself, without reading Lean's actual phaseB expression. It similarly assumes several alias and endpoint expressions. Six changed expressions still pass its assertion-enabled R420 check. This package supplies an independent restricted parser that rejects those changes and reproduces the unchanged data exactly.

The maintainer already checked the seven structured fields. This adds expression validation, portable replay and controls; it does not claim first correspondence or a defect in the original circuit. The mutations are not claimed to compile in Lean or bypass PR612's hash-pinned build.

Only research/r420-lean-source-binding/ is added. It checks 13 fields: the seven structured fields plus six scalar/domain fields, including all 672 frames, 837 ordered gates and 1,077 operand occurrences. Source hashes, Git blobs and a deterministic receipt bind the result. Identical decoded gzip payloads remain portable across compression encodings.

Validation

python -I -B research/r420-lean-source-binding/verify.py
python -I -B research/r420-lean-source-binding/test_binding.py

Expected verifier output: PASS_R420_LEAN_SOURCE_EXPRESSIONS fields=13 frames=672 gates=837 operands=1077.

All 13 tests pass normally and with -O on CPython 3.12.15/Linux in an offline restricted container. They cover 33 negative cases, including six historical false positives, plus unchanged sources, nested comments and recompression. Minimal relocation and six package-corruption controls pass; source Git-byte checks, selected-record integrity and staged whitespace pass.

Base: 7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261; seed 75. All consumed sources remain identical on refreshed main f567884aeb8851b6e794af1184119a3bfbe1e631. Overlap checked through #833. Credit James Chang's PR590/612 formalization, eumemic's PR543 supplier and Douglas R. Colkitt's prior maintainer audit; exact pins and retained notices are linked in the package.

No fresh Lean build, supplier cold replay, full make verify, remote CI or complete multiplication theorem is claimed. Physical transport, cleanup/lifecycle, hosting and all-size obligations remain. Prepared for Chinmay Arvind (@chinmayarvind23) with substantial OpenAI Codex assistance, under Apache-2.0; no independent human review is claimed.