Research: gate-operand export parity — dest-free always agrees; dest-in can diverge (answers #3004 OQ2; no new kappa)

research/gate-operand-export-parity/CERTIFICATE.json

@@ -0,0 +1,146 @@
+{
+  "claim": {
+    "dest_free_always_agree": true,
+    "dest_in_can_disagree": true,
+    "named_witnesses": {
+      "dest_with_src": {
+        "d": 0,
+        "exp": [
+          0,
+          3,
+          5
+        ],
+        "srcs": [
+          1,
+          0
+        ],
+        "sym": [
+          3,
+          3,
+          5
+        ],
+        "val0": [
+          7,
+          3,
+          5
+        ]
+      },
+      "self_even": {
+        "d": 0,
+        "exp": [
+          0,
+          3,
+          5
+        ],
+        "srcs": [
+          0,
+          0
+        ],
+        "sym": [
+          7,
+          3,
+          5
+        ],
+        "val0": [
+          7,
+          3,
+          5
+        ]
+      }
+    },
+    "small_domain": {
+      "dest_free_agree": 4686,
+      "dest_free_disagree": 0,
+      "dest_in_agree": 1152,
+      "dest_in_disagree": 3492,
+      "disagree_witnesses": [
+        [
+          0,
+          [
+            0,
+            0
+          ]
+        ],
+        [
+          1,
+          [
+            0,
+            1
+          ]
+        ],
+        [
+          2,
+          [
+            0,
+            2
+          ]
+        ],
+        [
+          3,
+          [
+            0,
+            3
+          ]
+        ],
+        [
+          4,
+          [
+            0,
+            4
+          ]
+        ],
+        [
+          5,
+          [
+            0,
+            5
+          ]
+        ],
+        [
+          0,
+          [
+            1,
+            0
+          ]
+        ],
+        [
+          1,
+          [
+            1,
+            1
+          ]
+        ]
+      ]
+    }
+  },
+  "controls": {
+    "checker_rejects": [
+      "self_even",
+      "dest_with_src",
+      "dup_src",
+      "self_once"
+    ],
+    "dup_src_section_agrees": true,
+    "scatter_only_guard_misses_gate_self_operand": true,
+    "self_even_export_records": 27235,
+    "self_once_section_agrees": true
+  },
+  "kappa_decimal": "0.001672660197076918",
+  "no_new_kappa": true,
+  "schema_version": 1,
+  "selected_word": {
+    "B0": [
+      127,
+      111,
+      [
+        3
+      ]
+    ],
+    "distinct_operand_gates": 5472,
+    "export_records": 27234,
+    "gates": 5472,
+    "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
+    "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+  },
+  "status": "PASS_GATE_OPERAND_EXPORT_PARITY"
+}

research/gate-operand-export-parity/MASTER-HANDOFF.md

@@ -0,0 +1,45 @@
+# MASTER-HANDOFF — gate-operand-export-parity
+
+## Claim (one sentence)
+
+At the selected PR589 checker/exporter boundary, destination-free gate source
+lists always make accumulate-XOR and sequential ADD agree, while
+destination-in-sources lists can diverge; the checker rejects them and the
+exporter does not.
+
+## Closest prior
+
+- #2977 scatter multiplicity counterexample
+- #3004 scatter odd-multiplicity agreement; OQ2 left gate operands open
+- #2992 / #3273 / #3346 scatter successor schemas (scatter-only)
+
+## New checkable fact
+
+Exact Sym/Exp lemma with exhaustive 4686 dest-free agreements, named
+`self_even` / `dest_with_src` witnesses, selected-word 5472 distinct gates,
+four checker rejects, exporter +1 record on `self_even`.
+
+## Evidence commands
+
+```sh
+python3.12 -I -B research/gate-operand-export-parity/verify.py
+python3.12 -I -O -Werror -B research/gate-operand-export-parity/verify.py
+python3.12 -I -B research/gate-operand-export-parity/independent.py
+python3.12 -I -B research/gate-operand-export-parity/test_package.py
+python3.12 -B scripts/research_package.py --package research/gate-operand-export-parity
+```
+
+## Soft-overlap vs leave-alones
+
+Clear of stock-leaf / router / flag-0 / C5 / side-correction / present-head /
+groups B–D native clusters. Touches only the #2977 supplier-boundary cascade
+at the unanswered #3004 gate-operand OQ.
+
+## Attribution
+
+Author Wentao Li `<wentaol4@illinois.edu>`. Neutral AI assistance disclosure.
+No `Co-authored-by: Victor Li`. No CrocSwap PR from this worker (master publishes).
+
+## Disposition
+
+Ready for master independent review / publish decision. Kappa unchanged.

research/gate-operand-export-parity/PROOF.md

@@ -0,0 +1,69 @@
+# Gate operand symbolic/export parity
+
+## Claim
+
+Let a multi-source gate be a triple `(f, d, srcs)` with destination register
+`d` and ordered source list `srcs`. Over `F_2`, compare two operators that both
+start from a pre-gate valuation `val0`:
+
+- **Sym** (selected symbolic checker): read every source from `val0`, form
+  `acc = ⊕_{s ∈ srcs} val0[s]`, then set `val[d] ← val0[d] ⊕ acc`.
+- **Exp** (selected record exporter): for each `s` in `srcs` in order, set
+  `val[d] ← val[d] ⊕ val[s]` using the *current* valuation.
+
+Then:
+
+1. If `d ∉ srcs`, then Sym and Exp agree for every `val0` (even when `srcs`
+   contains repeated indices).
+2. If `d ∈ srcs`, they need not agree. Concrete finite witnesses include
+   `srcs = [d, d]` and `srcs = [a, d]` for any `a ≠ d`.
+
+The selected PR589 checker rejects every gate with
+`len(set([d] + srcs)) ≠ len([d] + srcs)` before export. The exporter does not
+enforce distinctness. Scatter-only uniqueness guards therefore leave this gap
+open.
+
+Selected kappa is unchanged.
+
+## Proof of (1)
+
+Assume `d ∉ srcs`. In Exp, every assignment writes only register `d`. Every
+source read therefore observes `val0[s]`. The net update is
+
+```text
+val[d] ← val0[d] ⊕ (⊕_{s ∈ srcs} val0[s]),
+```
+
+counting multiplicity. That is exactly Sym. Agreement is independent of order
+and of whether source multiplicities are odd or even.
+
+## Proof of (2) by witness
+
+Take registers valued in `F_2` (or any `F_2`-vector space) and `d = 0`.
+
+- `srcs = [0, 0]`. Sym: `acc = val0[0] ⊕ val0[0] = 0`, so `val[0]` is unchanged.
+  Exp: first ADD forces `val[0] ← 0`; second ADD leaves it `0`. These differ
+  whenever `val0[0] ≠ 0`.
+- `srcs = [1, 0]` with `a = 1 ≠ 0`. Sym: `acc = val0[1] ⊕ val0[0]`, so
+  `val[0] ← val0[1]`. Exp: after ADD from 1 one has `val[0] = val0[0] ⊕ val0[1]`;
+  the subsequent self-ADD forces `val[0] ← 0`. These differ whenever
+  `val0[1] ≠ 0`.
+
+## Relation to scatter parity (#2977 / #3004)
+
+For scatter rows the symbolic loop XORs once per occurrence while the exporter
+emits one ADD per membership. They agree exactly when every positive
+multiplicity is odd. Gate lists are different: both operators are
+occurrence-based, yet they still diverge when the destination appears among
+the sources because Exp re-reads the updated destination. #3004's open
+question on gate operands treated distinctness as schema hygiene with "no
+known divergent word"; the witnesses above are divergent under export-without
+the checker. Accepted words cannot carry them only because the checker rejects
+`bad operands` first.
+
+## What this does not claim
+
+- No production adoption and no new kappa.
+- No claim that the selected word is defective: every D/A/B/C gate on the
+  pinned tuned word has distinct operands.
+- No native C++ replay and no change to frozen exporters.

research/gate-operand-export-parity/README.md

@@ -0,0 +1,82 @@
+# Gate operand symbolic/export parity
+
+**Card `supplier-boundary-audit`, priority revision 6**, refined to PR
+[#3004](https://github.com/CrocSwap/integer-mult-bounds/pull/3004) open question 2
+under the [#2977](https://github.com/CrocSwap/integer-mult-bounds/pull/2977)
+checker/exporter cascade. No new kappa
+(`0.001672660197076918`).
+
+#3004 characterised scatter rows and left gate operand lists as a schema-consistency
+question, stating that accepted words cannot diverge and that “no known divergent
+word exists.” This package supplies the missing gate-side contract:
+
+- **Sym** (checker): accumulate source XOR from the pre-gate valuation, then XOR
+  into the destination.
+- **Exp** (exporter): sequential `ADD` of each listed source into the destination,
+  re-reading the current valuation.
+
+If the destination is absent from the source list, Sym and Exp always agree — even
+with repeated sources. If the destination appears among the sources, they can
+disagree. Concrete witnesses include `srcs = [d, d]` and `srcs = [a, d]`.
+
+The selected checker rejects every non-distinct operand list (`bad operands`)
+before export. The exporter does not enforce distinctness and will emit the
+extra `ADD`s. A scatter-only uniqueness guard therefore misses this gap.
+
+```sh
+python3.12 -I -B research/gate-operand-export-parity/verify.py
+```
+
+Expected:
+
+```text
+PASS_GATE_OPERAND_EXPORT_PARITY dest_free_agree=4686 dest_in_disagree_witnesses=2 selected_distinct_gates=5472 checker_rejects=4 no_new_kappa
+```
+
+## Evidence
+
+- Exhaustive census on 6 registers and source lists of length 0..4: **4686/4686**
+  destination-free patterns agree; destination-in patterns include disagreements.
+- Named witnesses `self_even` and `dest_with_src` diverge on integer valuations;
+  destination-free duplicate sources still agree.
+- Pinned selected tuned word: all **5472** D/A/B/C gates have distinct operands;
+  baseline export has **27234** records.
+- Mutating `B[0]` from `[127, 111, [3]]` to self-operand forms: checker rejects
+  all four mutants with `bad operands`; exporter still runs and the `self_even`
+  mutant emits **27235** records.
+- Scatter rows of the self-operand mutant remain unique, so a scatter-only guard
+  accepts them.
+
+Default verify is read-only against `CERTIFICATE.json`. Admission uses `need()`
+and stays enforced under `python -O`. Explicit `--write` regenerates the
+certificate only.
+
+## Reproduce
+
+```sh
+python3.12 -I -B research/gate-operand-export-parity/verify.py
+python3.12 -I -O -Werror -B research/gate-operand-export-parity/verify.py
+python3.12 -I -B research/gate-operand-export-parity/independent.py
+python3.12 -I -B research/gate-operand-export-parity/test_package.py
+python3.12 -B scripts/research_package.py --package research/gate-operand-export-parity
+```
+
+## Open next questions
+
+1. **Should a successor schema reject destination-in-sources gates at export time?**
+   First step: compose the distinct-operand check with an existing opt-in boundary
+   (`simple-scatter-v1` / `integer-xor-scatter-v1`) before export. Blocked by
+   maintainer schema adoption, not by arithmetic.
+2. **Does native legality independently reject self-operand gates?** First step:
+   feed the `self_even` export into the native column checker. Blocked by a C++
+   toolchain in this session; not required for the Sym/Exp lemma.
+
+## Credit
+
+Nick Petalas / #2977 named the scatter multiplicity gap. Kumagi / #3004 gave the
+exact scatter agreement contract and left the gate-operand question open. Dylan
+Crow authored the exporter; eumemic the symbolic checker; the tuned PR589 word
+is the retained selected bit supplier. Predecessor notices are unchanged.
+
+Prepared by Wentao Li with substantial AI assistance. Apache-2.0.
+No independent human or proof-assistant review is claimed.