diff --git a/.github/workflows/gate-operand-parity-lean.yml b/.github/workflows/gate-operand-parity-lean.yml
new file mode 100644
index 0000000000..1723038db3
--- /dev/null
+++ b/.github/workflows/gate-operand-parity-lean.yml
@@ -0,0 +1,49 @@
+# Manual and pull-request replay for the kernel-checked gate-operand parity
+# package.  Archives no scientific claim; see docs/research/research-archive-intake.md.
+name: Lean gate-operand parity
+on:
+  pull_request:
+    paths:
+      - 'research/gate-operand-parity-lean/**'
+      - 'research/e8-bit-p111-tuned/code/xcheck_p.py'
+      - 'research/e8-bit-carrier-skeleton/code/bit/export_records.py'
+      - '.github/workflows/gate-operand-parity-lean.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'research/gate-operand-parity-lean/**'
+      - '.github/workflows/gate-operand-parity-lean.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+concurrency:
+  group: gate-operand-parity-lean-${{ github.ref }}
+  cancel-in-progress: false
+
+jobs:
+  formal:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    env:
+      PYTHONDONTWRITEBYTECODE: '1'
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.12'
+      - name: Checksum-pinned official Lean
+        shell: bash
+        run: |
+          curl --fail --location --retry 3 https://github.com/leanprover/lean4/releases/download/v4.21.0/lean-4.21.0-linux.tar.zst -o "$RUNNER_TEMP/gate-lean.tar.zst"
+          echo "455c6df09d5bd54d2a51b137939c47e2dda816d512ac789c4b3642c9bf98bde8  $RUNNER_TEMP/gate-lean.tar.zst" | sha256sum --check
+          tar --zstd -xf "$RUNNER_TEMP/gate-lean.tar.zst" -C "$RUNNER_TEMP"
+      - name: Registered standard-library checks
+        run: python -I -B research/gate-operand-parity-lean/verify.py
+      - name: Fresh kernel build and axiom reports
+        run: python -I -B research/gate-operand-parity-lean/verify.py --lean "$RUNNER_TEMP/lean-4.21.0-linux/bin/lean"
+      - name: Rejection controls
+        run: python -I -B research/gate-operand-parity-lean/test_package.py
+      - run: git diff --exit-code
diff --git a/research/gate-operand-parity-lean/README.md b/research/gate-operand-parity-lean/README.md
new file mode 100644
index 0000000000..93465160a8
--- /dev/null
+++ b/research/gate-operand-parity-lean/README.md
@@ -0,0 +1,146 @@
+# Gate-operand parity in Lean: the all-size agreement contract, kernel-checked
+
+**Formal interface lemma; no new κ.** The selected κ stays
+`0.001672660197076918`. This package machine-checks the exact gate-operand
+agreement contract of the PR589 checker/exporter boundary: the bounded census
+and informal coefficient argument of
+[PR #3738](https://github.com/CrocSwap/integer-mult-bounds/pull/3738)
+(itself answering [PR #3696](https://github.com/CrocSwap/integer-mult-bounds/pull/3696)
+open question 1 in the [#2977](https://github.com/CrocSwap/integer-mult-bounds/pull/2977)/[#3004](https://github.com/CrocSwap/integer-mult-bounds/pull/3004)
+supplier-boundary cascade) is replaced here by an all-size Lean 4 theorem with
+its kernel axiom report.
+
+```lean
+theorem GateParity.sym_eq_exp_iff_contract (d : Nat) (srcs : List Nat) :
+    Contract d srcs ↔ ∀ v : Nat → Bool, sym d srcs v = exp d srcs v
+```
+
+## The two operators, exactly
+
+Over registers `Nat` and initial values `v : Nat → Bool`:
+
+| operator | pinned source | Lean definition |
+|---|---|---|
+| `sym` (checker) | `research/e8-bit-p111-tuned/code/xcheck_p.py`, gate run lines 252-255: `acc = 0; for s in srcs: acc ^= val[s]; val[d] ^= acc` | `fun r => if r = d then bxor (v d) (xfold (srcs.map v)) else v r` |
+| `exp` (exporter) | `research/e8-bit-carrier-skeleton/code/bit/export_records.py`, `run`: `for s in srcs: rec.append((1,d,s,1,f,ph))`, replayed as one sequential `ADD(d, s)` per source | `srcs.foldl (step d) v` with `step d x s = fun r => if r = d then bxor (x d) (x s) else x r` |
+
+Both are one gate `(d, srcs)`; `xfold` is the XOR fold of a boolean list.
+
+## The contract
+
+```lean
+def Contract (d : Nat) (srcs : List Nat) : Prop :=
+  d ∉ srcs ∨ ∃ p t, srcs = p ++ (d :: t) ∧ d ∉ t ∧ ∀ r, EvenCount (p.count r)
+```
+
+Spelled out: the destination is absent from the source list, or the list splits
+at the destination's last occurrence with every register occurring an even
+number of times in the prefix `p` and no destination in the suffix `t`. The
+prefix condition covers the destination itself: `EvenCount (p.count d)` is the
+"odd destination multiplicity" clause of the census contract, and the remaining
+clauses are the pre-last-occurrence evenness statement. This is exactly the
+contract measured in `research/gate-operand-parity-contract` (PR #3738); here it
+is proved for every register count and every source list, and cross-checked by
+that package's finite census.
+
+## What is machine-checked, and what is not
+
+Machine-checked (Lean 4.21.0 core, no Mathlib, `lean/GateParity.lean`):
+
+- **Main theorem** `sym_eq_exp_iff_contract`: agreement on every valuation iff
+  `Contract`, for all `d` and all `srcs`.
+- `exp_dest_free`: destination-free source lists always agree (the case used by
+  every one of the selected tuned word's 5,472 D/A/B/C gates).
+- `exp_split_d`: over a split `p ++ (d :: t)` with `d ∉ t`, the exporter state at
+  `d` is the XOR fold over `t`.
+- `allEvenCount_xfold`: if every register occurs an even number of times in a
+  list, the XOR fold of any valuation over that list is `false` (the pairing
+  argument, as strong induction on length).
+- `xfold_indicator`: the XOR fold under the indicator valuation of `r` is the
+  parity of `r`'s multiplicity; this supplies the divergent valuation whenever
+  the contract fails.
+- Kernel axiom reports (printed by the build):
+  `sym_eq_exp_iff_contract` depends on `[propext, Classical.choice, Quot.sound]`;
+  the four supporting lemmas on `[propext, Quot.sound]`. No `sorryAx`; the
+  verifier also rejects `sorry`, `axiom`, `unsafe`, `partial`, `opaque`,
+  `native_decide` and `run_tac` tokens in the proof source.
+
+Not established here:
+
+- No supplier, tariff, hosting, precision, all-size/compiler or selected-chain
+  change; no new κ; no selected-frontier change. This is a boundary lemma, not a
+  multiplication theorem.
+- The Lean statement formalizes the two operators as functions; it does not
+  replay the exporter or the checker, and the gate-list/record-stream counts of
+  the pinned word remain PR #3738's and PR #3696's measurements.
+- The finite census below corroborates the statement binding; the all-size
+  claim is carried only by the kernel proof.
+
+## Bounded finite cross-check
+
+`verify.py` includes an independent standard-library implementation of both
+operators and of the contract predicate, and requires, for every `(d, srcs)`
+pair with 4 registers and source lists of length `≤ 4`, that agreement *on all
+16 valuations* coincides with the predicate: **1,364 pairs, 708 agreeing, 656
+diverging, 100 % match**. This is a statement-binding check of the Lean
+definition, not a proof; it deliberately uses a domain disjoint from the
+published census domain (6 registers, length ≤ 4).
+
+## Reproduce
+
+Standard-library mode (this is the registered command; no Lean required, and it
+does not claim Lean ran):
+
+```sh
+python3.12 -B research/gate-operand-parity-lean/verify.py
+python3.12 -B research/gate-operand-parity-lean/test_package.py
+```
+
+Expected:
+
+```text
+PASS_GATE_OPERAND_PARITY_LEAN pins=2 targets=5 census_pairs=1364 census_agreements=708 census_divergences=656 contract_matches=1 lean_kernel=not_run
+PASS_GATE_OPERAND_PARITY_LEAN_CONTROLS controls=6 positive_total=120
+```
+
+Kernel mode (a fresh Lean build of the all-size theorem and its axiom reports):
+
+```sh
+python3.12 -B research/gate-operand-parity-lean/verify.py --lean <path>/bin/lean   # pinned Lean 4.21.0
+```
+
+Expected:
+
+```text
+PASS_GATE_OPERAND_PARITY_LEAN_KERNEL pins=2 targets=5 census_pairs=1364 census_agreements=708 census_divergences=656 contract_matches=1 lean=4.21.0 axioms=Classical.choice,Quot.sound,propext sorry_free=true
+```
+
+The package's own dispatched workflow
+(`.github/workflows/gate-operand-parity-lean.yml`) downloads the checksum-pinned
+official Lean 4.21.0 release and runs the kernel mode plus the rejection
+controls; its hosted result is the CI certification of the kernel claim.
+
+## Credit
+
+Prepared by Nick Petalas with AI assistance, under Apache-2.0.
+Predecessor credit: Wentao Li's PR #3696 (gate-operand export parity; its open
+question 1), the PR #2977/PR #3004 scatter cascade and the `#2992`/`#3273`/`#3346`
+successors, PR #3738 (the bounded census and exact contract this package
+formalizes), eumemic's pinned symbolic checker (`xcheck_p.py`) and Dylan Crow's
+pinned record exporter (`export_records.py`), which the two Lean definitions
+follow line for line.
+
+## Open next questions
+
+1. **Reordered exporters.** The contract depends on the destination's last
+   occurrence, so an exporter that sorted or reversed a gate's sources would
+   have a different, recomputable condition. Relevance: a successor schema that
+   reorders sources could move the boundary. First step: state the reordered
+   operator and adapt the proof's split point. Blocked by: no current exporter
+   reorders sources.
+2. **A shared formal layer with the scatter schema.** The scatter contract (all
+   positive multiplicities odd) is a different object settled by
+   `scatter-parity-contract-audit` and its successors. Relevance: one kernel
+   argument could cover both boundaries. First step: formalize the scatter
+   read/write pair and relate it to the same XOR-fold lemma. Blocked by: the
+   scatter record shape is not the gate shape and needs its own definitions.
diff --git a/research/gate-operand-parity-lean/SOURCES.json b/research/gate-operand-parity-lean/SOURCES.json
new file mode 100644
index 0000000000..c7eb99f3f1
--- /dev/null
+++ b/research/gate-operand-parity-lean/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/code/xcheck_p.py",
+      "usage": "input",
+      "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009",
+      "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e"
+    },
+    {
+      "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py",
+      "usage": "input",
+      "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350",
+      "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3"
+    }
+  ]
+}
diff --git a/research/gate-operand-parity-lean/TASK.json b/research/gate-operand-parity-lean/TASK.json
new file mode 100644
index 0000000000..aaec04eaab
--- /dev/null
+++ b/research/gate-operand-parity-lean/TASK.json
@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "A kernel-checked, all-size Lean 4 proof of the exact gate-operand agreement contract between the pinned PR589 checker operator (accumulate-then-write) and the pinned record exporter operator (sequential per-source ADD): sym and exp agree on every initial valuation exactly for the lists satisfying Contract (destination absent, or the list splits at the destination with an all-even prefix and no destination in the suffix).",
+  "scope_change_reason": "The card's method is used directly (state one missing boundary lemma, then formalize it), but the lemma is taken from the live supplier-boundary cascade rather than the historical selected review: PR2977/PR3004/PR3696 and the contract package settled the checker/exporter schema informally and by bounded census, with the all-size statement recorded as an informal coefficient argument. The stated open obligation there -- an all-size proof rather than a finite census -- is exactly a formal-interface lemma, so this package machine-checks it instead of duplicating the bounded census.",
+  "bottleneck_link": "The checker/exporter gate-operand contract is a source-bound acceptance condition of the selected bit supplier's export boundary. A kernel-checked version replaces the informal case argument with a machine-checked all-size theorem at the same hypothesis set; it does not change the selected kappa or any supplier cost.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the all-size Lean theorem, its kernel axiom reports, the bounded finite census cross-check, the source pins of the two frozen operators, and the rejection controls. Do not formalize the scatter schema, do not run the native backend, do not rebuild the selected chain and do not claim a new kappa.",
+  "outcome": "completed",
+  "evidence": "In Lean 4.21.0 core (no Mathlib), GateParity.sym_eq_exp_iff_contract proves for all d : Nat, all srcs : List Nat and all valuations v : Nat -> Bool that sym d srcs v = exp d srcs v exactly iff Contract d srcs, where Contract is 'd not in srcs, or srcs = p ++ (d :: t) with d not in t and every register occurring an even number of times in p'. Supporting all-size lemmas: destination-free agreement (exp_dest_free), the exporter state over a split list (exp_split_d), the pairing lemma that an all-even list XORs to false (allEvenCount_xfold), and the indicator lemma that the XOR fold of the indicator of r is the parity of r's multiplicity (xfold_indicator). Kernel reports: sym_eq_exp_iff_contract depends on propext, Classical.choice, Quot.sound; the four supporting lemmas on propext, Quot.sound; no sorryAx. The package also pins the two frozen operator line groups (checker gate run at code/xcheck_p.py lines 252-255; exporter per-source ADD at code/bit/export_records.py run()) and cross-checks the contract predicate against a direct simulation on all 1364 (d, srcs) pairs with 4 registers and lists of length <= 4 and every valuation (708 agreeing, 656 diverging, 100% match). This is a finite cross-check of the statement, not the proof; the all-size claim is carried by the Lean theorem.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does the exact contract transfer to an exporter that reorders a gate's sources before emitting the ADDs?",
+      "why_it_matters": "The condition depends on the position of the destination's last occurrence, so a sorted or reversed lowering has a different (recomputable) contract; the current pinned exporter preserves order.",
+      "first_step": "State the reordered-operator agreement condition and adapt the Lean proof's split point to the chosen order.",
+      "blocked_by": "No current exporter reorders sources; this is a successor-schema design question."
+    },
+    {
+      "question": "Can the destination-free lemma be reused to machine-check the scatter schema's own multiplicity contract?",
+      "why_it_matters": "The scatter contract (all positive multiplicities odd) is a different object settled by scatter-parity-contract-audit and its successors; a shared formal layer would let both boundaries share one kernel argument.",
+      "first_step": "Formalize the scatter read/write pair and relate it to the same XOR-fold lemma.",
+      "blocked_by": "The scatter schema's record-level read/write shape is not the gate shape; it needs its own operator definitions."
+    }
+  ]
+}
diff --git a/research/gate-operand-parity-lean/VERIFY.json b/research/gate-operand-parity-lean/VERIFY.json
new file mode 100644
index 0000000000..4c45a075e5
--- /dev/null
+++ b/research/gate-operand-parity-lean/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e8-bit-p111-tuned/code/xcheck_p.py",
+    "research/e8-bit-carrier-skeleton/code/bit/export_records.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Lean source byte pin, axiom-command binding and proof-escape scan; the two frozen operator line groups (checker accumulate-then-write, exporter per-source ADD); and the bounded finite census cross-checking the contract predicate against direct simulation on all 1364 (d, srcs) pairs with 4 registers, lists of length <= 4, and every valuation. The all-size kernel build is a separate declared mode (--lean) certified by this package's own dispatched workflow, not by this registered command."
+    }
+  ]
+}
diff --git a/research/gate-operand-parity-lean/lean/GateParity.lean b/research/gate-operand-parity-lean/lean/GateParity.lean
new file mode 100644
index 0000000000..06ac1b630c
--- /dev/null
+++ b/research/gate-operand-parity-lean/lean/GateParity.lean
@@ -0,0 +1,374 @@
+/-
+  Gate-operand parity between the pinned symbolic checker operator and the
+  pinned record exporter operator, machine-checked for all register counts,
+  all source lists and all initial valuations.
+
+  The two operators are the pinned ones of the PR589 checker/exporter boundary:
+
+  * Sym (`research/e8-bit-p111-tuned/code/xcheck_p.py`): accumulate the XOR of
+    the listed sources read before the gate, then write the destination once.
+  * Exp (`research/e8-bit-carrier-skeleton/code/bit/export_records.py`): one
+    `ADD(d, s)` per listed source, replayed sequentially over current values.
+
+  This file depends only on Lean's core library.  It is the kernel-checked
+  companion of the bounded census in the gate-operand parity contract package:
+  the contract below is proved for every source list, not only on a bounded
+  census domain.
+-/
+import Init
+
+namespace GateParity
+
+/-! ### Core boolean and list helpers -/
+
+/-- Explicit boolean XOR (avoids any notation ambiguity). -/
+def bxor (a b : Bool) : Bool := Bool.xor a b
+
+theorem bxor_false (b : Bool) : bxor false b = b := by cases b <;> rfl
+
+theorem bxor_assoc (a b c : Bool) : bxor a (bxor b c) = bxor (bxor a b) c := by
+  cases a <;> cases b <;> cases c <;> rfl
+
+theorem bxor_comm (a b : Bool) : bxor a b = bxor b a := by cases a <;> cases b <;> rfl
+
+theorem bxor_self (a : Bool) : bxor a a = false := by cases a <;> rfl
+
+theorem bxor_false_right (a : Bool) : bxor a false = a := by cases a <;> rfl
+
+/-- If `bxor a b = b` then `a` is false. -/
+theorem bxor_eq_right {a b : Bool} (h : bxor a b = b) : a = false := by
+  calc a = bxor a false := (bxor_false_right a).symm
+       _ = bxor a (bxor b b) := by rw [bxor_self]
+       _ = bxor (bxor a b) b := bxor_assoc a b b
+       _ = bxor b b := by rw [h]
+       _ = false := bxor_self b
+
+/-- Cancellation of the middle term. -/
+theorem bxor_mid (a b c : Bool) : bxor a (bxor b (bxor a c)) = bxor b c := by
+  cases a <;> cases b <;> cases c <;> rfl
+
+/-- XOR fold of a boolean list. -/
+def xfold (l : List Bool) : Bool := l.foldr bxor false
+
+theorem xfold_nil : xfold [] = false := rfl
+
+theorem xfold_cons (a : Bool) (l : List Bool) : xfold (a :: l) = bxor a (xfold l) := rfl
+
+theorem xfold_append (a b : List Bool) : xfold (a ++ b) = bxor (xfold a) (xfold b) := by
+  induction a with
+  | nil => exact (bxor_false (xfold b)).symm
+  | cons x t ih => rw [List.cons_append, xfold_cons, ih, xfold_cons, bxor_assoc]
+
+theorem map_congr_mem {f g : Nat → Bool} {l : List Nat} (h : ∀ x ∈ l, f x = g x) :
+    l.map f = l.map g := List.map_congr_left h
+
+/-! ### Parity counts -/
+
+/-- Parity predicates over `Nat`, kept local so the file needs no Mathlib. -/
+def EvenCount (n : Nat) : Prop := n % 2 = 0
+
+def OddCount (n : Nat) : Prop := n % 2 = 1
+
+instance (n : Nat) : Decidable (EvenCount n) := inferInstanceAs (Decidable (n % 2 = 0))
+
+instance (n : Nat) : Decidable (OddCount n) := inferInstanceAs (Decidable (n % 2 = 1))
+
+theorem oddCount_of_not_evenCount {n : Nat} (h : ¬ EvenCount n) : OddCount n := by
+  have hlt : n % 2 < 2 := Nat.mod_lt n (by omega)
+  unfold EvenCount at h
+  unfold OddCount
+  omega
+
+theorem oddCount_succ_iff (n : Nat) : OddCount (n + 1) ↔ ¬ OddCount n := by
+  unfold OddCount
+  constructor
+  · intro h hn
+    omega
+  · intro h
+    have hlt : n % 2 < 2 := Nat.mod_lt n (by omega)
+    omega
+
+theorem decide_oddCount_succ (n : Nat) :
+    decide (OddCount (n + 1)) = !decide (OddCount n) := by
+  by_cases h : OddCount n
+  · have hn : ¬ OddCount (n + 1) := fun h' => (oddCount_succ_iff n).mp h' h
+    rw [decide_eq_false_iff_not.mpr hn, decide_eq_true_eq.mpr h]
+    rfl
+  · have hn : OddCount (n + 1) := (oddCount_succ_iff n).mpr h
+    rw [decide_eq_true_eq.mpr hn, decide_eq_false_iff_not.mpr h]
+    rfl
+
+theorem count_cons_eq (x y : Nat) (l : List Nat) :
+    (x :: l).count y = l.count y + (if y = x then 1 else 0) := by
+  by_cases h : y = x
+  · subst h
+    rw [List.count_cons_self]
+    simp
+  · rw [List.count_cons_of_ne (fun hxy => h hxy.symm)]
+    simp [h]
+
+theorem count_insert_two (x y : Nat) (a b : List Nat) :
+    ((x :: a) ++ (x :: b)).count y = (a ++ b).count y + (if y = x then 2 else 0) := by
+  simp only [count_cons_eq, List.count_append]
+  split <;> omega
+
+theorem evenCount_of_count_insert_two {x y : Nat} {a b : List Nat}
+    (h : EvenCount (((x :: a) ++ (x :: b)).count y)) : EvenCount ((a ++ b).count y) := by
+  rw [count_insert_two] at h
+  unfold EvenCount at *
+  split at h <;> omega
+
+/-- A member of `t` is not the absent `d`. -/
+theorem ne_of_mem_not_mem {x d : Nat} {t : List Nat} (hx : x ∈ t) (hd : d ∉ t) : x ≠ d := by
+  intro h
+  subst h
+  exact hd hx
+
+/-- A nonempty list splits at a first occurrence of `x`. -/
+theorem exists_first_split {x : Nat} : ∀ {l : List Nat}, x ∈ l →
+    ∃ a b, l = a ++ (x :: b) ∧ x ∉ a
+  | [], h => by simp at h
+  | y :: t, h => by
+      by_cases hyx : y = x
+      · subst hyx
+        exact ⟨[], t, rfl, by simp⟩
+      · have hxy : x ≠ y := fun hxy => hyx hxy.symm
+        have hxt : x ∈ t := by
+          rcases List.mem_cons.mp h with h' | h'
+          · exact absurd h' hxy
+          · exact h'
+        obtain ⟨a, b, hab, hxa⟩ := exists_first_split hxt
+        refine ⟨y :: a, b, ?_, ?_⟩
+        · rw [hab, List.cons_append]
+        · intro hmem
+          rcases List.mem_cons.mp hmem with h' | h'
+          · exact hxy h'
+          · exact hxa h'
+
+/-- A nonempty list splits after a last occurrence of `d`. -/
+theorem exists_last_split {d : Nat} : ∀ {l : List Nat}, d ∈ l →
+    ∃ p t, l = p ++ (d :: t) ∧ d ∉ t
+  | [], h => by simp at h
+  | y :: t, h => by
+      by_cases hdt : d ∈ t
+      · obtain ⟨p, t', hsplit, hnt⟩ := exists_last_split hdt
+        exact ⟨y :: p, t', by rw [hsplit, List.cons_append], hnt⟩
+      · have hy : y = d := by
+          rcases List.mem_cons.mp h with h' | h'
+          · exact h'.symm
+          · exact absurd h' hdt
+        subst hy
+        exact ⟨[], t, rfl, hdt⟩
+
+/-! ### The all-even parity lemma
+
+If every register occurs an even number of times in a list, the XOR fold of any
+valuation over that list is `false`.  The proof is the pairing argument: remove
+the first occurrence of the head register and its next occurrence, which is a
+shorter list with the same all-even property, and apply strong induction on the
+length. -/
+
+theorem allEvenCount_xfold (l : List Nat) (h : ∀ r, EvenCount (l.count r))
+    (v : Nat → Bool) : xfold (l.map v) = false := by
+  have main : ∀ n, ∀ l : List Nat, l.length = n → (∀ r, EvenCount (l.count r)) →
+      ∀ v : Nat → Bool, xfold (l.map v) = false := by
+    intro n
+    refine Nat.strongRecOn n ?_
+    intro m ih l hlen h v
+    match l with
+    | [] => rfl
+    | x :: t =>
+        have hc := h x
+        rw [count_cons_eq] at hc
+        have hc' : EvenCount (t.count x + 1) := by simpa using hc
+        have hxodd : OddCount (t.count x) := oddCount_of_not_evenCount (by
+          intro he
+          unfold EvenCount at he hc'
+          omega)
+        have hxpos : 0 < t.count x := by
+          unfold OddCount at hxodd
+          omega
+        have hxmem : x ∈ t := List.count_pos_iff.mp hxpos
+        obtain ⟨a, b, hab, hxa⟩ := exists_first_split hxmem
+        have hlen2 : (a ++ b).length < m := by
+          rw [← hlen, hab]
+          simp [List.length_append, List.length_cons]
+          omega
+        have halleven : ∀ y, EvenCount ((a ++ b).count y) := by
+          intro y
+          have hcy := h y
+          rw [hab] at hcy
+          exact evenCount_of_count_insert_two hcy
+        have hid : xfold ((x :: t).map v) = xfold ((a ++ b).map v) := by
+          rw [hab]
+          simp only [List.map_append, List.map_cons, xfold_cons, xfold_append]
+          rw [bxor_mid]
+        rw [hid]
+        exact ih (a ++ b).length hlen2 (a ++ b) rfl halleven v
+  exact main l.length l rfl h v
+
+/-- For the indicator valuation of a register, the XOR fold is the parity of
+that register's multiplicity. -/
+theorem xfold_indicator (r : Nat) (l : List Nat) :
+    xfold (l.map (fun x => decide (x = r))) = decide (OddCount (l.count r)) := by
+  induction l with
+  | nil => rfl
+  | cons s t ih =>
+      rw [List.map_cons, xfold_cons, ih]
+      by_cases hsr : s = r
+      · rw [hsr, List.count_cons_self, decide_oddCount_succ]
+        have hd : decide (r = r) = true := decide_eq_true_eq.mpr rfl
+        rw [hd]
+        cases decide (OddCount (t.count r)) <;> rfl
+      · rw [List.count_cons_of_ne (a := r) hsr]
+        have hdec : decide (s = r) = false := decide_eq_false_iff_not.mpr hsr
+        rw [hdec, bxor_false]
+
+/-! ### The two gate operators -/
+
+/-- One sequential exporter step: `ADD(d, s)` over current values. -/
+def step (d : Nat) (x : Nat → Bool) (s : Nat) : Nat → Bool :=
+  fun r => if r = d then bxor (x d) (x s) else x r
+
+/-- The pinned exporter operator: one `ADD(d, s)` per listed source, in order. -/
+def exp (d : Nat) (srcs : List Nat) (v : Nat → Bool) : Nat → Bool :=
+  srcs.foldl (step d) v
+
+/-- The pinned checker operator: pre-gate XOR accumulation, then one write. -/
+def sym (d : Nat) (srcs : List Nat) (v : Nat → Bool) : Nat → Bool :=
+  fun r => if r = d then bxor (v d) (xfold (srcs.map v)) else v r
+
+theorem step_self (d : Nat) (x : Nat → Bool) (s : Nat) : step d x s d = bxor (x d) (x s) := by
+  simp [step]
+
+theorem step_ne {r d : Nat} (h : r ≠ d) (x : Nat → Bool) (s : Nat) :
+    step d x s r = x r := by
+  simp [step, h]
+
+theorem exp_cons (d : Nat) (s : Nat) (srcs : List Nat) (v : Nat → Bool) :
+    exp d (s :: srcs) v = exp d srcs (step d v s) := rfl
+
+theorem exp_append (d : Nat) (a b : List Nat) (v : Nat → Bool) :
+    exp d (a ++ b) v = exp d b (exp d a v) := by
+  simp only [exp, List.foldl_append]
+
+theorem exp_ne {r d : Nat} (h : r ≠ d) (srcs : List Nat) (v : Nat → Bool) :
+    exp d srcs v r = v r := by
+  induction srcs generalizing v with
+  | nil => rfl
+  | cons s t ih => rw [exp_cons, ih, step_ne h]
+
+theorem sym_d (d : Nat) (srcs : List Nat) (v : Nat → Bool) :
+    sym d srcs v d = bxor (v d) (xfold (srcs.map v)) := by
+  simp [sym]
+
+theorem sym_ne {r d : Nat} (h : r ≠ d) (srcs : List Nat) (v : Nat → Bool) :
+    sym d srcs v r = v r := by
+  simp [sym, h]
+
+/-- Destination-free gates: the exporter only ever adds pre-gate values, so the
+sequential accumulation equals the checker's single write. -/
+theorem exp_dest_free {d : Nat} (srcs : List Nat) (h : d ∉ srcs) (v : Nat → Bool) :
+    exp d srcs v d = bxor (v d) (xfold (srcs.map v)) := by
+  induction srcs generalizing v with
+  | nil => exact (bxor_false_right (v d)).symm
+  | cons s t ih =>
+      have hdt : d ∉ t := fun hmem => h (List.mem_cons.mpr (Or.inr hmem))
+      have hsd : s ≠ d := fun hsd => h (hsd ▸ List.mem_cons_self ..)
+      have hstep : (step d v s) d = bxor (v d) (v s) := step_self d v s
+      rw [exp_cons, ih hdt, hstep, List.map_cons, xfold_cons]
+      have hmap : t.map (step d v s) = t.map v :=
+        map_congr_mem (fun x hx => step_ne (ne_of_mem_not_mem hx hdt) v s)
+      rw [hmap, bxor_assoc]
+
+/-- In a split `p ++ [d] ++ t` with `d` absent from `t`, the exporter state at
+`d` is exactly the XOR fold of the valuation over `t`. -/
+theorem exp_split_d {d : Nat} (p t : List Nat) (h : d ∉ t) (v : Nat → Bool) :
+    exp d (p ++ (d :: t)) v d = xfold (t.map v) := by
+  rw [show p ++ (d :: t) = (p ++ [d]) ++ t from (List.append_assoc p [d] t).symm,
+    exp_append]
+  have hz : exp d (p ++ [d]) v d = false := by
+    rw [exp_append]
+    simp only [exp, List.foldl_cons, List.foldl_nil, step_self, bxor_self]
+  have hmap : t.map (exp d (p ++ [d]) v) = t.map v :=
+    map_congr_mem (fun x hx => exp_ne (ne_of_mem_not_mem hx h) (p ++ [d]) v)
+  rw [exp_dest_free t h, hmap, hz, bxor_false]
+
+/-! ### The exact agreement contract -/
+
+/-- The exact agreement condition of the pinned checker/exporter operators: the
+destination is absent from the source list, or the list splits at the
+destination with every register in the prefix occurring an even number of times
+and no destination in the suffix. -/
+def Contract (d : Nat) (srcs : List Nat) : Prop :=
+  d ∉ srcs ∨ ∃ p t, srcs = p ++ (d :: t) ∧ d ∉ t ∧ ∀ r, EvenCount (p.count r)
+
+/-- **Main theorem.**  The pinned checker operator `sym` and the pinned exporter
+operator `exp` agree on every initial valuation exactly for the source lists
+satisfying `Contract`. -/
+theorem sym_eq_exp_iff_contract (d : Nat) (srcs : List Nat) :
+    Contract d srcs ↔ ∀ v : Nat → Bool, sym d srcs v = exp d srcs v := by
+  constructor
+  · intro hc v
+    funext r
+    rcases hc with hfree | ⟨p, t, hsplit, hdt, heven⟩
+    · by_cases hrd : r = d
+      · rw [hrd]
+        rw [sym_d, exp_dest_free srcs hfree]
+      · rw [sym_ne hrd, exp_ne hrd]
+    · subst hsplit
+      by_cases hrd : r = d
+      · rw [hrd]
+        rw [sym_d, exp_split_d p t hdt]
+        have hp : xfold (p.map v) = false := allEvenCount_xfold p heven v
+        have hmap : (p ++ (d :: t)).map v = p.map v ++ (v d :: t.map v) := by simp
+        rw [hmap, xfold_append, xfold_cons, hp]
+        cases (v d) <;> cases (xfold (t.map v)) <;> rfl
+      · rw [sym_ne hrd, exp_ne hrd]
+  · intro h
+    by_cases hmem : d ∈ srcs
+    · obtain ⟨p, t, hsplit, hdt⟩ := exists_last_split hmem
+      by_cases hall : ∀ r, EvenCount (p.count r)
+      · exact Or.inr ⟨p, t, hsplit, hdt, hall⟩
+      · exfalso
+        obtain ⟨r, hr⟩ := Classical.not_forall.mp hall
+        have hodd : OddCount (p.count r) := oddCount_of_not_evenCount hr
+        have hv := congrFun (h (fun x => decide (x = r))) d
+        rw [hsplit, sym_d, exp_split_d p t hdt] at hv
+        have hmap : (p ++ (d :: t)).map (fun x => decide (x = r))
+            = p.map (fun x => decide (x = r)) ++ (decide (d = r) :: t.map (fun x => decide (x = r))) := by
+          simp
+        rw [hmap, xfold_append, xfold_cons, xfold_indicator, xfold_indicator] at hv
+        rw [bxor_mid] at hv
+        have hcancel : decide (OddCount (p.count r)) = false := bxor_eq_right hv
+        have htrue : decide (OddCount (p.count r)) = true := decide_eq_true_eq.mpr hodd
+        rw [hcancel] at htrue
+        cases htrue
+    · exact Or.inl hmem
+
+/-! ### Kernel-evaluated examples -/
+
+example : sym 0 [1, 2] (fun r => r = 1) 0 = exp 0 [1, 2] (fun r => r = 1) 0 := by
+  decide
+
+example : sym 0 [1, 1] (fun r => r = 1) 0 = exp 0 [1, 1] (fun r => r = 1) 0 := by
+  decide
+
+example : ¬ (sym 0 [0, 0] (fun _ => true) 0 = exp 0 [0, 0] (fun _ => true) 0) := by
+  decide
+
+example : ¬ (sym 0 [1, 0] (fun _ => true) 0 = exp 0 [1, 0] (fun _ => true) 0) := by
+  decide
+
+example : sym 0 [0] (fun _ => true) 0 = exp 0 [0] (fun _ => true) 0 := by
+  decide
+
+end GateParity
+
+/-! ### Kernel axiom reports for the registered audit -/
+
+#print axioms GateParity.sym_eq_exp_iff_contract
+#print axioms GateParity.allEvenCount_xfold
+#print axioms GateParity.xfold_indicator
+#print axioms GateParity.exp_dest_free
+#print axioms GateParity.exp_split_d
diff --git a/research/gate-operand-parity-lean/test_package.py b/research/gate-operand-parity-lean/test_package.py
new file mode 100644
index 0000000000..a058c7b30e
--- /dev/null
+++ b/research/gate-operand-parity-lean/test_package.py
@@ -0,0 +1,98 @@
+"""Negative controls for research/gate-operand-parity-lean/verify.py.
+
+Each control must be rejected for its own reason, so a passing verify run is
+not a run of a checker that accepts anything.  Standard library only.
+Prepared by Nick Petalas with AI assistance.  Apache-2.0.
+"""
+from pathlib import Path
+import importlib.util
+
+HERE = Path(__file__).resolve().parent
+spec = importlib.util.spec_from_file_location("gate_verify", HERE / "verify.py")
+verify = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(verify)
+
+FAILURES = []
+
+
+def expect_error(label, function, needle):
+    try:
+        function()
+    except ValueError as error:
+        if needle not in str(error):
+            FAILURES.append("control rejected for the wrong reason: %s (%s)"
+                            % (label, str(error)[:60]))
+        return label
+    FAILURES.append("control accepted: " + label)
+    return label
+
+
+good = verify.LEAN_SOURCE.read_text()
+
+
+# 1. A `sorry` in the proof body must be rejected.
+sorry_source = good.replace("theorem xfold_nil : xfold [] = false := rfl",
+                            "theorem xfold_nil : xfold [] = false := by sorry")
+expect_error("sorry escape", lambda: verify.check_lean_source(sorry_source), "sorry")
+
+# 2. A dropped axiom report must be rejected.
+dropped = good.replace("#print axioms GateParity.exp_split_d\n", "")
+expect_error("missing axiom report",
+             lambda: verify.check_lean_source(dropped), "missing axiom report")
+
+# 3. A changed contract body must be rejected.
+changed = good.replace("d ∉ srcs ∨ ∃ p t, srcs = p ++ (d :: t) ∧ d ∉ t ∧ ∀ r, EvenCount (p.count r)",
+                       "d ∉ srcs")
+expect_error("changed Contract body",
+             lambda: verify.check_lean_source(changed), "statement binding missing")
+
+# 4. A changed checker operator line must be rejected.
+real_root = verify.ROOT
+
+
+
+
+def tampered_pins():
+    original = verify.PINNED
+    verify.PINNED = [(original[0][0], original[0][1],
+                      original[0][2] + ["acc ^= val[d]"])]
+    try:
+        verify.check_pins(real_root)
+    finally:
+        verify.PINNED = original
+
+
+expect_error("changed pinned operator line", tampered_pins, "pinned operator line missing")
+
+# 5. The finite census must reject a wrong contract predicate.
+expect_error("wrong contract predicate",
+             lambda: verify.census(registers=3, max_len=3, contract=lambda d, s: True),
+             "contract mismatch")
+
+# 6. Axiom parsing: unexpected axiom, sorryAx, and missing target.
+expect_error("unexpected axiom",
+             lambda: verify.parse_axioms(
+                 "'GateParity.x' depends on axioms: [Foo.sorryAx]",
+                 ["GateParity.x"]),
+             "unexpected axiom")
+expect_error("sorryAx report",
+             lambda: verify.parse_axioms(
+                 "'GateParity.x' depends on axioms: [propext]\nsorryAx",
+                 ["GateParity.x"]),
+             "unchecked proof")
+expect_error("missing target report",
+             lambda: verify.parse_axioms("'GateParity.y' does not depend on any axioms",
+                                         ["GateParity.x"]),
+             "axiom report set mismatch")
+
+# Positive control: the real package passes all six underlying checks.
+verify.check_lean_source()
+verify.check_pins(real_root)
+total, agree, diverge = verify.census(registers=3, max_len=3)
+assert total > 0 and agree + diverge == total
+
+if FAILURES:
+    for line in FAILURES:
+        print("FAIL " + line)
+    raise SystemExit(1)
+print("PASS_GATE_OPERAND_PARITY_LEAN_CONTROLS controls=6 positive_total=%d" % total)
diff --git a/research/gate-operand-parity-lean/verify.py b/research/gate-operand-parity-lean/verify.py
new file mode 100644
index 0000000000..fc4d243853
--- /dev/null
+++ b/research/gate-operand-parity-lean/verify.py
@@ -0,0 +1,236 @@
+"""Kernel-checked gate-operand parity between the pinned checker and exporter.
+
+Three layers, separately labelled:
+
+* source pins: the frozen operator lines that `sym` and `exp` formalize, and
+  the Lean source bytes;
+* a bounded finite census (standard library, independent of the Lean run) that
+  cross-checks the contract predicate against direct simulation;
+* kernel mode (`--lean`): a fresh Lean build of `lean/GateParity.lean` with the
+  axiom reports of the five named theorems.
+
+The default command never claims Lean ran.  Kernel mode requires the pinned
+Lean 4.21.0 executable.
+
+Prepared by Nick Petalas with AI assistance.  Apache-2.0.
+"""
+from pathlib import Path
+import argparse
+import hashlib
+import re
+import subprocess
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+LEAN_SOURCE = HERE / "lean" / "GateParity.lean"
+LEAN_SHA256 = "f4ec5064bcdf1b0ab255e5d92271041ae1503bb83744a633d1eeed3170c59266"
+LEAN_VERSION = "4.21.0"
+AXIOM_TARGETS = [
+    "GateParity.sym_eq_exp_iff_contract",
+    "GateParity.allEvenCount_xfold",
+    "GateParity.xfold_indicator",
+    "GateParity.exp_dest_free",
+    "GateParity.exp_split_d",
+]
+ALLOWED_AXIOMS = {"propext", "Classical.choice", "Quot.sound"}
+
+# Frozen operator lines that the Lean definitions formalize.
+PINNED = [
+    (
+        "research/e8-bit-p111-tuned/code/xcheck_p.py",
+        "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e",
+        ["acc = 0", "for s in srcs:", "acc ^= val[s]", "val[d] ^= acc"],
+    ),
+    (
+        "research/e8-bit-carrier-skeleton/code/bit/export_records.py",
+        "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3",
+        ["for s in srcs: rec.append((1,d,s,1,f,ph))"],
+    ),
+]
+
+# Statement bindings: exact normalized definition bodies of the Lean formalization.
+STATEMENT_BINDINGS = [
+    "def Contract (d : Nat) (srcs : List Nat) : Prop := "
+    "d ∉ srcs ∨ ∃ p t, srcs = p ++ (d :: t) ∧ d ∉ t ∧ ∀ r, EvenCount (p.count r)",
+    "def sym (d : Nat) (srcs : List Nat) (v : Nat → Bool) : Nat → Bool := "
+    "fun r => if r = d then bxor (v d) (xfold (srcs.map v)) else v r",
+    "def step (d : Nat) (x : Nat → Bool) (s : Nat) : Nat → Bool := "
+    "fun r => if r = d then bxor (x d) (x s) else x r",
+    "def exp (d : Nat) (srcs : List Nat) (v : Nat → Bool) : Nat → Bool := "
+    "srcs.foldl (step d) v",
+]
+
+ESCAPES = ["sorry", "axiom", "admit", "unsafe", "partial", "opaque",
+           "native_decide", "run_tac", "elab", "macro", "syntax"]
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def sha256(path):
+    return hashlib.sha256(Path(path).read_bytes()).hexdigest()
+
+
+def lean_code(source):
+    """Remove nested Lean comments; keep newlines and code tokens."""
+    out, depth, i = [], 0, 0
+    while i < len(source):
+        if source.startswith("/-", i):
+            depth += 1
+            i += 2
+        elif depth and source.startswith("-/", i):
+            depth -= 1
+            i += 2
+        elif not depth and source.startswith("--", i):
+            end = source.find("\n", i)
+            i = len(source) if end < 0 else end
+        else:
+            out.append(source[i] if not depth or source[i] == "\n" else " ")
+            i += 1
+    need(depth == 0, "unterminated Lean comment")
+    return "".join(out)
+
+
+def normalize(text):
+    return re.sub(r"\s+", " ", text).strip()
+
+
+def check_lean_source(source=None, digest=None):
+    """Byte pin, axiom-command binding and proof-escape scan."""
+    if source is None:
+        need(sha256(LEAN_SOURCE) == LEAN_SHA256, "Lean source bytes changed")
+        source = LEAN_SOURCE.read_text()
+    code = lean_code(source)
+    lines = code.splitlines()
+    for target in AXIOM_TARGETS:
+        need(any(line.strip() == "#print axioms " + target for line in lines),
+             "missing axiom report for " + target)
+    body = "\n".join(line for line in lines if not line.strip().startswith("#print "))
+    for name in ESCAPES:
+        need(not re.search(r"\b" + name + r"\b", body), "proof escape present: " + name)
+    text = normalize(body)
+    for binding in STATEMENT_BINDINGS:
+        need(normalize(binding) in text, "statement binding missing: " + binding[:40])
+    return len(AXIOM_TARGETS)
+
+
+def check_pins(root=ROOT):
+    for rel, digest, lines in PINNED:
+        path = root / rel
+        need(path.is_file(), "pinned source missing: " + rel)
+        need(sha256(path) == digest, "pinned source bytes changed: " + rel)
+        text = path.read_text()
+        for line in lines:
+            need(line in text, "pinned operator line missing in %s: %s" % (rel, line))
+    return len(PINNED)
+
+
+def b_sym(d, srcs, val):
+    off = False
+    for s in srcs:
+        off ^= val[s]
+    out = list(val)
+    out[d] ^= off
+    return out
+
+
+def b_exp(d, srcs, val):
+    out = list(val)
+    for s in srcs:
+        out[d] ^= out[s]
+    return out
+
+
+def b_contract(d, srcs):
+    if d not in srcs:
+        return True
+    k = max(i for i, s in enumerate(srcs) if s == d)
+    prefix, suffix = srcs[:k], srcs[k + 1:]
+    return d not in suffix and all(prefix.count(r) % 2 == 0 for r in set(prefix))
+
+
+def census(registers=4, max_len=4, contract=b_contract):
+    """Agreement for every valuation iff the contract, over every list."""
+    total = agree = diverge = 0
+    vals = [[(mask >> i) & 1 == 1 for i in range(registers)]
+            for mask in range(1 << registers)]
+    lists = []
+    stack = [[]]
+    while stack:
+        cur = stack.pop()
+        lists.append(cur)
+        if len(cur) < max_len:
+            for r in range(registers):
+                stack.append(cur + [r])
+    for srcs in lists:
+        for d in range(registers):
+            total += 1
+            same_all = all(b_sym(d, srcs, val) == b_exp(d, srcs, val) for val in vals)
+            need(same_all == contract(d, srcs),
+                 "contract mismatch at d=%d srcs=%r" % (d, srcs))
+            if contract(d, srcs):
+                agree += 1
+            else:
+                diverge += 1
+    return total, agree, diverge
+
+
+def parse_axioms(output, targets=AXIOM_TARGETS):
+    found = {}
+    for name, raw in re.findall(r"'([^']+)' depends on axioms:\s*\[([^\]]*)\]", output):
+        need(name not in found, "duplicate axiom report: " + name)
+        axioms = sorted(x.strip() for x in raw.split(",") if x.strip())
+        need(set(axioms) <= ALLOWED_AXIOMS, "unexpected axiom for %s: %r" % (name, axioms))
+        found[name] = axioms
+    for name in re.findall(r"'([^']+)' does not depend on any axioms", output):
+        need(name not in found, "duplicate axiom report: " + name)
+        found[name] = []
+    need(set(found) == set(targets),
+         "axiom report set mismatch: missing %r extra %r"
+         % (sorted(set(targets) - set(found)), sorted(set(found) - set(targets))))
+    need("sorryAx" not in output, "unchecked proof reported")
+    return found
+
+
+def kernel_build(lean):
+    need(lean.is_file(), "Lean executable missing: " + str(lean))
+    version = subprocess.check_output([str(lean), "--version"], text=True)
+    need(LEAN_VERSION in version, "wrong Lean version: " + version.strip())
+    result = subprocess.run([str(lean), str(LEAN_SOURCE)], capture_output=True,
+                            text=True, timeout=900)
+    output = result.stdout + result.stderr
+    need(result.returncode == 0, "Lean build failed:\n" + output[-2000:])
+    reports = parse_axioms(output)
+    return version.strip(), reports
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--lean", type=Path, default=None,
+                        help="path to the pinned Lean 4.21.0 executable")
+    args = parser.parse_args()
+
+    targets = check_lean_source()
+    pins = check_pins()
+    total, agree, diverge = census()
+    if args.lean is None:
+        print("PASS_GATE_OPERAND_PARITY_LEAN pins=%d targets=%d census_pairs=%d "
+              "census_agreements=%d census_divergences=%d contract_matches=1 "
+              "lean_kernel=not_run" % (pins, targets, total, agree, diverge))
+    else:
+        version, reports = kernel_build(args.lean)
+        summary = ",".join(sorted({a for ax in reports.values() for a in ax}))
+        parsed = re.search(r"version (\S+?)[,)]", version)
+        print("PASS_GATE_OPERAND_PARITY_LEAN_KERNEL pins=%d targets=%d census_pairs=%d "
+              "census_agreements=%d census_divergences=%d contract_matches=1 "
+              "lean=%s axioms=%s sorry_free=true"
+              % (pins, targets, total, agree, diverge,
+                 parsed.group(1) if parsed else version.split()[0], summary or "none"))
+
+
+if __name__ == "__main__":
+    main()