Cut rank-two clean compilation from 16 to 10 CNOTs (no κ)

research/clean-rank-two-conjugators/PROOF.md

@@ -0,0 +1,79 @@
+# Shared conjugators for a rank-two clean operation
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Work over any vector space in characteristic two and let g be a linear
+involution. Put t=1+g, so t squared is zero. All identities below are formal
+identities in F2[C2], hence hold without any finite-address assumption.
+Each CNOT is one scalar role addition; each G applies g to the helper h.
+
+Write A1 for `h += c`, A2 for `h += d`, B1 for `a += h`, B2 for `b += h`,
+C1 for `a += c` and C2 for `b += d`. Strings in this proof are chronological.
+Set A12=A1 A2 and B12=B1 B2; these pairs commute internally.
+
+JoyboyBrian #5007 constructs the following three idempotents, with role
+order a,b,c,d,h:
+
+```text
+x1 = a+h,       y1 = d*+h*
+x2 = b+h,       y2 = c*+h*
+x3 = a+b+h,     y3 = c*+d*+h*
+```
+
+Here stars denote coordinate covectors. Their sum is
+`a c* + b d* + h h*`. The inherited construction and minimum retain
+#5007's credit. Because t squared is zero, the three factors I+t xj yj
+commute. Reorder them 1,3,2 and use #5007's literal conjugators:
+
+```text
+B1 A2 G A2 B1
+B12 A12 G A12 B12
+B2 A1 G A1 B2
+```
+
+The two boundary scalar strings simplify without moving any reflection:
+
+```text
+A2 B1 B12 A12 = A2 B2 A2 A1 = B2 C2 A1
+A12 B12 B2 A1 = A2 A1 B1 A1 = A2 B1 C1
+```
+
+The only noncommuting rewrite is `Ai Bi Ai = Bi Ci`. It follows directly
+by applying the three scalar additions to arbitrary inputs. The other
+rewrites cancel repeated involutions or commute disjoint-source additions.
+The resulting complete stream is
+
+```text
+B1 A2 G B2 C2 A1 G A2 B1 C1 G A1 B2
+```
+
+There are ten CNOTs and three G calls. The complete factor product is
+`I+t(a c*+b d*+h h*)`. Thus a and b acquire t times c and d, both sources
+are restored and the full helper action is `h+t h=g(h)`. A clean zero
+helper returns to zero. No data role starts clean, is erased or is discarded.
+
+For a proof independent of the conjugator notation, put t=1+g and track
+the new stream. Immediately after the first G, h is `g(h0+d)` and a is
+`a0+h0`. Immediately before the second G, h is `g(h0+d)+c`. Just after it,
+h is `h0+d+g(c)` and b is `b0+g(h0)+t d`. Before the third G, h is
+`h0+g(c)` and a has become `a0+t c`. The last two scalar additions restore
+h to `g(h0)` and b to `b0+t d`. c and d are never destinations. This proves
+the full five-input identity directly for any involutory linear g.
+
+At stationary complete prices the clean bill is `3R+10C+H`. The cited
+dirty stream is the separate echo on each pair,
+
+```text
+a += c; c <- g(c); a += c; c <- g(c)
+b += d; d <- g(d); b += d; d <- g(d)
+```
+
+Its bill is `4R+4C`. Its two pieces use disjoint roles, so concatenation
+creates no adjacent cancellation; no global scalar lower bound is claimed
+for either stream. Subtracting the specified bills gives `-R+6C+H`,
+establishing the strict comparison exactly when R>6C+H. The earlier
+specified clean stream's sixteen CNOTs gave R>12C+H. Shared conjugators
+remove six counted CNOTs while preserving all three reflections and every
+input/output obligation. A common data-basis conjugation adds its complete
+forward and inverse scalar costs to both bills and does not change this
+comparison. No physical caller or primitive price is assumed available.

research/clean-rank-two-conjugators/README.md

@@ -0,0 +1,107 @@
+# Ten CNOTs for the three-reflection rank-two clean compiler
+
+This contribution was produced by Nick Petalas.
+
+The rank-two clean square-zero operation has a literal implementation with
+three coordinate reflections and **ten scalar CNOTs**, improving the sixteen
+CNOTs of JoyboyBrian's merged [#5007](https://github.com/CrocSwap/integer-mult-bounds/pull/5007).
+This is a scoped algebraic construction with a written proof and exact finite
+corroboration. No scalar-network minimum or new kappa is claimed.
+
+Let g be any linear involution in characteristic two. Four data roles
+`a,b,c,d` are arbitrary and helper `h` starts at zero. The complete action is
+
+```text
+a <- a + c + g(c)       b <- b + d + g(d)
+c <- c                  d <- d                  h <- 0
+```
+
+The full five-input action, even when h is dirty, is the displayed data map
+and `h <- g(h)`. Thus the clean return is exact; an arbitrary dirty helper
+does not satisfy the restored-workspace contract. [WORD.json](WORD.json)
+contains all thirteen primitives in chronological order, using role indices
+`a,b,c,d,h = 0,1,2,3,4`. Every scalar XOR and inverse operation is included.
+[PROOF.md](PROOF.md) derives the new stream by sharing scalar conjugators.
+
+At complete stationary coordinate-reflection price R, CNOT price C and
+additional clean-resource reservation/return charge H, the new local bill is
+`3R+10C+H`. The explicitly priced dirty rank-two stream in #5007 costs
+`4R+4C`; its two disjoint four-operation pieces have no adjacent cancellations.
+The new clean word is cheaper precisely when **R > 6C+H**, improving the
+previous specified-word comparison `R > 12C+H`. This compares specified streams,
+not globally optimal scalar networks. Common basis transport, if needed, must
+be charged equally on both sides. No native R, C or H is supplied.
+
+## Evidence and reproduction
+
+From the repository root, CPython 3.12 and its standard library suffice:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clean-rank-two-conjugators/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clean-rank-two-conjugators/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clean-rank-two-conjugators
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clean-rank-two-conjugators --check-source-history
+```
+
+Substitute a local CPython 3.12 path elsewhere. Expected output includes
+`PASS_CLEAN_RANK_TWO_CONJUGATORS reflections=3 CNOTs=10 no_new_kappa`.
+The read-only verifier generates a receipt bound to every package file and
+the cited live inputs. It does not import or execute predecessor code.
+
+The checker proves the complete five-input formal endpoint in F2[C2] by
+coefficient arithmetic. A separate literal bit-array interpreter checks all
+1,024 two-address states, including all 256 clean-helper states, and every
+basis column for every involutory permutation on one through six addresses.
+All thirteen individual primitive omissions and three boundary controls are
+checked. These finite domains corroborate the field-uniform written identity;
+they do not prove an unbounded statement by enumeration.
+
+## Scope, overlap and limitations
+
+This takes Open next question 2 of #5007, a changed compiler-side scope of
+`bit-new-register-model`. The change matters because the exact reflection
+count alone leaves scalar encoding and restoration costs unpaid. It does not
+meet the card's native-supplier acceptance gate. The first verified improvement
+is packaged without extending the search to other ranks or claiming optimality.
+
+Canonical base is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+The prescribed selected-baseline command passed after its inputs were
+materialized in this sparse checkout. It authenticates metadata only.
+The initial overlap cache paginated 405 open PRs and 5,290 Discussion records
+on October 27, 2026. Sparse local note coverage was incomplete; separate Git
+searches covered main's complete README tree, with additional merged-PR
+searches and the live #5007/#4912 bodies. No competing shared-conjugator
+result was found. Unpublished work, arbitrary diffs and omitted history remain
+limits; a no-match search is not a novelty certificate.
+
+Native reflection implementation, physical routing/frames/tapes/hosting,
+the availability and price of the clean function, recursive admission and
+the complete multiplication theorem remain unresolved. Lean, Docker,
+the selected scientific replay and predecessor executables are unrun.
+Independent human and formal proof-kernel review are unclaimed.
+
+The verifier uses bounded Python-managed allocations, a Power of Ten rule-3
+deviation. Width is fixed at five and address size is at most six. The largest
+state enumeration has 1,024 entries; permutation enumeration is at most 720
+per size. Functions are below sixty lines, checks use explicit exceptions
+under `-O`, and both registered runs treat warnings as errors. No external
+solver, recursion, subprocess or generated code is used.
+
+## Open next questions
+
+Can an actual native caller supply the stationary primitive prices and one
+returned clean role with `R > 6C+H`? Begin with one literal rank-two caller
+and price every data movement, inverse scalar map and clean reservation.
+Those native contracts and the complete invoice are the blockers.
+
+## Credit
+
+JoyboyBrian #5007 supplies the clean three-projector construction, its exact
+reflection-call minimum and the explicit scalar-optimization handoff.
+Nick Petalas #4912 supplies the dirty optimum and split compiler. ywz65
+#2716 supplies the involution-product identity and arbitrary-coupling compiler
+context. Adam Gall #1911, eumemic #288, Ali Romman #468, woklerx #1443,
+Gareth Davidson #1333, Arham Tahir #1589 and Cinna Davis #2290 retain the
+register-model lineage credit. The new contribution is the shared-conjugator
+ten-CNOT stream and its improved specified-word price comparison. New work
+is Apache-2.0.

research/clean-rank-two-conjugators/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/clean-square-zero-compiler/PROOF.md",
+      "usage": "input",
+      "git_blob": "3eaec47c2c249f3933d35f9693001b12bca80d42",
+      "sha256": "5638c02bdd988349fcfd02b6591ae80344c99e01f5f005740e4cea14c806675b"
+    },
+    {
+      "path": "research/clean-square-zero-compiler/README.md",
+      "usage": "input",
+      "git_blob": "7135e70c617678b1d01efd785863640bb8ffa65b",
+      "sha256": "1e1b231edb1bed1fafb0068cc63988007d92c264ab34f316637b69ede7ad52e7"
+    },
+    {
+      "path": "research/square-zero-idempotent-compiler/README.md",
+      "usage": "input",
+      "git_blob": "1fa5319015c2c79ac6819edf9f4d238fe7295993",
+      "sha256": "bec1e4187fd70cb9cebc447ec62da0676eda6f27f89aba0bdd1a7b17adce17ff"
+    }
+  ]
+}

research/clean-rank-two-conjugators/TASK.json

@@ -0,0 +1,69 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Shared scalar conjugators lower the canonical rank-two returned-clean compiler to three coordinate reflections and ten CNOTs.",
+  "scope_change_reason": "Take JoyboyBrian PR5007 Open next question 2 as a small compiler side result. This prices a specified literal boundary and does not claim a new native supplier.",
+  "bottleneck_link": "Scalar preparation and restoration costs determine whether saving one reflection survives a complete primitive bill.",
+  "budget_minutes": 60,
+  "stop_rule": "Package the first proved lower CNOT count without searching larger ranks or claiming scalar optimality.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the complete formal identity; verify.py independently checks literal finite address actions and failure controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a literal native caller supply complete prices satisfying R > 6C+H?",
+      "why_it_matters": "The lower formal scalar bill does not establish native savings or recursive admission.",
+      "first_step": "Bind one rank-two caller, every data movement and inverse scalar map, and the returned clean resource to stationary complete primitive prices.",
+      "blocked_by": "Native reflection/CNOT contracts and clean reservation/return price are not supplied."
+    }
+  ],
+  "environment": {
+    "python": "3.12.15",
+    "implementation": "CPython",
+    "platform": "macOS-27.0.1-arm64-arm-64bit"
+  }
+}

research/clean-rank-two-conjugators/VERIFY.json

@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/clean-square-zero-compiler/PROOF.md",
+    "research/clean-square-zero-compiler/README.md",
+    "research/square-zero-idempotent-compiler/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "New complete formal endpoint, all finite literal states and involutions, exact primitive bill and semantic rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "New complete formal endpoint, all finite literal states and involutions, exact primitive bill and semantic rejection controls."
+    }
+  ]
+}

research/clean-rank-two-conjugators/WORD.json

@@ -0,0 +1,15 @@
+[
+  ["xor", 0, 4],
+  ["xor", 4, 3],
+  ["g", 4],
+  ["xor", 1, 4],
+  ["xor", 1, 3],
+  ["xor", 4, 2],
+  ["g", 4],
+  ["xor", 4, 3],
+  ["xor", 0, 4],
+  ["xor", 0, 2],
+  ["g", 4],
+  ["xor", 4, 2],
+  ["xor", 1, 4]
+]