Kernel-checked gate-operand parity: the all-size agreement contract in Lean (no new kappa)

.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

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.

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

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

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