Prove exact 20-XOR clockwise cyclic parity minimum (no new κ)

research/five-role-cyclic-parity/PROOF.md

@@ -0,0 +1,96 @@
+# Twenty clockwise XORs are necessary and sufficient
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Endpoint and alphabet
+
+Five labeled registers contain independent arbitrary vectors over F2. The
+only allowed instructions are `r_(i+1 mod 5) += r_i`, for i=0,...,4. Every
+instruction costs one. The requested complete output is
+
+```
+y_i = x_i + x_(i+1 mod 5) + x_(i+2 mod 5),   0 <= i < 5.
+```
+
+No additional registers, free wire permutations, basis changes, initialization,
+erasure or nonlinear/data-dependent instructions are allowed. The endpoint
+matrix has row masks `(7,14,28,25,19)`, with bit j denoting input x_j.
+The alphabet has exactly five generators, all involutions. Reverse-direction
+neighboring additions and nonneighboring additions are excluded.
+
+## Attainment
+
+The following ordered word has twenty instructions. Each pair is source,
+destination, and every pair is one of the five allowed clockwise edges.
+
+```
+(0,1) (2,3) (4,0) (0,1) (1,2)
+(0,1) (3,4) (2,3) (4,0) (3,4)
+(2,3) (1,2) (0,1) (3,4) (2,3)
+(4,0) (0,1) (1,2) (0,1) (3,4)
+```
+
+Literal symbolic row substitution gives the specified complete matrix. A
+separate bit interpreter executes the word on all 32 scalar inputs and checks
+the same endpoint. A linear identity on the five input basis vectors extends
+coordinatewise to arbitrary binary vector payloads. Reversing the involutions
+recovers all five independent inputs. Thus twenty is an upper bound.
+
+## Exhaustive lower bound
+
+Encode each binary 5-by-5 matrix in a 25-bit integer, with five consecutive
+five-bit rows. Adding row s to row d is exactly the `step` operation in
+verify.py. Define B_r(M) to be all states reachable from center M in at most
+r allowed instructions.
+
+Starting with {M}, form all five neighbors of every state in the latest
+layer, discard previously seen states and repeat r times. Induction proves
+this enumerates exactly B_r(M): every positive-length word is a shorter
+word followed by one allowed gate. Keeping only the shortest occurrence of a
+state preserves every possible continuation. The search uses no symmetry
+quotient, pivot heuristic or pruning beyond equality of complete matrices.
+Its domain is contained in the 2^25 binary matrices.
+
+The complete enumerated exact-distance layers are
+
+```
+radius     0  1   2   3    4    5    6     7     8     9     10
+layer      1  5  15  40  100  240  555  1230  2665  5715  12010
+```
+
+The identity ball B_9(I) has 10,566 matrices. The target ball B_10(T) has
+22,576 matrices. Their intersection is empty. Both balls and every layer
+count are computed afresh by the standalone verifier, without accepting any
+saved distance table or discovery output.
+
+If a word of length l<=19 connected I to T, cut it after min(l,9) gates.
+The intermediate matrix would lie in B_9(I). Reversing the remaining at most
+ten involutions would place it in B_10(T), contradicting disjointness.
+Therefore at least twenty instructions are necessary, matching the witness.
+
+This is a finite computer-assisted certificate with a written reduction to
+arbitrary vector payloads. It trusts the explicit enumerator and Python
+execution; independent human and proof-kernel review are unclaimed.
+
+## Controls and prior work
+
+The literal bit interpreter uses a list of five bits, independently of packed
+matrix arithmetic. It checks all 32 inputs, inverse recovery and a failure
+after deletion of each of the twenty gates. The first nineteen witness gates
+supply a positive control for the same 9+10 exclusion method: their known
+nine-gate midpoint belongs to both corresponding balls. Nine malformed
+input/program cases reject. All checks use explicit exceptions under -O.
+
+Gareth Davidson's merged PR #1188 already certifies every unrestricted
+five-role distance using all twenty directed row additions. This contribution
+does not claim a new unrestricted metric or replay that predecessor. Restricting
+the generator alphabet changes which paths exist; a shortest unrestricted
+path does not determine the present optimum. Ali Romman's PR #5793 supplies
+the related custom-alphabet synthesis interface, limited to four roles.
+Classical shortest paths and meet-in-the-middle exclusion retain their credit.
+Global literature priority for this endpoint is unclaimed.
+
+The result prices scalar binary register additions in the stated cyclic
+layout. It supplies no native tensor identity with phases, physical routing
+invoice, recursive paid-child minimum, new kappa or complete multiplication
+theorem. Other layouts, extra registers and altered alphabets are outside scope.

research/five-role-cyclic-parity/README.md

@@ -0,0 +1,89 @@
+# A five-role cyclic parity stencil needs twenty clockwise XORs
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: finite certificate with a written reduction to arbitrary binary
+vector inputs. For five arbitrary labeled registers, the complete map
+
+```
+y_i = x_i + x_(i+1 mod 5) + x_(i+2 mod 5),   0 <= i < 5,
+```
+
+has exact minimum cost twenty when the only allowed operations are
+`r_(i+1 mod 5) += r_i`, each at unit cost. No workspace, free wire permutation
+or free basis change is allowed. [PROOF.md](PROOF.md) gives a twenty-step word.
+The complete radius-nine identity ball and radius-ten target ball contain
+10,566 and 22,576 matrices and are disjoint, excluding every shorter word.
+
+The contribution is this restricted-alphabet optimum. Gareth Davidson's
+[merged PR #1188](https://github.com/CrocSwap/integer-mult-bounds/pull/1188)
+already gives a complete unrestricted five-role metric with twenty generators;
+that result is credited and not replayed here. [Ali Romman's PR #5793](https://github.com/CrocSwap/integer-mult-bounds/pull/5793),
+head `9ddb022cc1d879a5d3173f8f1f526a2ff504e7b3`, supplies the custom-alphabet
+synthesis interface and its four-role limit. Classical finite-group search and
+meet-in-the-middle exclusion are inherited methods. Literature priority is
+unclaimed.
+
+## Reproduce
+
+From the worktree root, with the CPython 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/five-role-cyclic-parity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/five-role-cyclic-parity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/five-role-cyclic-parity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/five-role-cyclic-parity --check-source-history
+```
+
+Local validation uses CPython 3.12.15 on macOS 27.0.1 arm64. Another Python
+3.12 interpreter may replace the absolute path. Each registered command has
+a 120-second timeout. The standalone verifier requires neither Git nor network,
+writes no files and emits `PASS_FIVE_ROLE_CYCLIC_PARITY` in a generated JSON
+receipt bound to all six package files' SHA256 hashes. No receipt is handwritten.
+[SOURCES.json](SOURCES.json) pins historical provenance, including #1188's README.
+No predecessor executable or mathematical certificate is imported or replayed.
+
+The checker enumerates the two exclusion balls and a separate known
+nineteen-gate positive-control ball. It checks all 32 literal inputs, inverse
+recovery, twenty deleted-gate controls and nine malformed-input rejections.
+All counts concern labeled complete matrices, without a symmetry quotient.
+Every word shorter than twenty in the declared alphabet is excluded.
+
+## Scope and limits
+
+The `complex-rank-shape-decoder` card changes to this scalar linear-synthesis
+side result in [TASK.json](TASK.json). Source-binding orientation passed at
+canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+No native caller or complete signed invoice is supplied. The selected conditional
+kappa and its five inherited framework assumptions remain unchanged.
+
+The [original CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216913)
+proposed unrestricted synthesis. The [scope correction](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217027)
+withdraws originality for that covered case and restricts the operation alphabet.
+Only the clockwise optimum is claimed as new. Live PRs, main README formulas,
+merged work, Discussions and local reservations were checked. Cached/sparse
+and unpublished coverage remains limited; no-match searches do not prove novelty.
+
+Extra roles, free bases/permutations, other endpoints, nonlinear instructions,
+odd characteristic and unequal gate prices are outside scope. Native phases,
+ownership, routing, dirty return, rounding, tape movement and complete recursive
+costs remain open. No selected cold replay, Lean, Docker or complete multiplier
+is claimed. Independent human and formal proof-kernel review are unclaimed.
+
+Power of Ten inspection is confined to the new verifier. Loops are bounded by
+five roles/gates, at most ten search layers, 32 inputs or twenty witness gates.
+The conservative generated-word bound per ball is `sum(5^k,k=0..10)=12207031`;
+the largest retained ball here contains only 22,576 matrices. Functions fit
+within 60 lines, mutable search state is local, and there is no recursion,
+subprocess, network call or dynamic code generation. Explicit checks remain
+active under -O. Rule 3 has a managed-runtime deviation for Python's bounded
+integer, tuple and set allocation. Warning-strict normal/optimized execution
+and in-memory syntax compilation supply diagnostics.
+
+## Open next questions
+
+Can a concrete native caller use this clockwise-local stencil as a cheaper
+complete adapter? First identify its five-role cyclic layout and exact boundary,
+then price conversions, phases, aliases, ownership and every restoration.
+No compatible caller or complete invoice is supplied. A scalar XOR optimum
+alone does not imply a recursive gain. No follow-up is reserved.

research/five-role-cyclic-parity/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/r439-gl5-shortest/README.md",
+      "usage": "provenance",
+      "git_blob": "492ee4766f95660621c38ef3b339e71d4a854cfa",
+      "sha256": "51030d14b06b1434319b014f19c5e44e17896881831d4d2b4893330e3f7bd668"
+    }
+  ]
+}

research/five-role-cyclic-parity/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the exact minimum of twenty unit XOR additions for the complete five-role binary cyclic three-tap parity map when only the five clockwise neighboring additions are allowed, with no workspace or free bases.",
+  "scope_change_reason": "The assigned decoder card changes to a restricted scalar linear-synthesis side result beyond PR5793's four-role domain. PR1188 already covers unrestricted five-role distances; the original unrestricted novelty claim is withdrawn in the linked progress correction. This contribution changes the generator alphabet and claims only its new optimum.",
+  "bottleneck_link": "Exact whole-register linear replacements can reduce adapter work, but this finite scalar benchmark has no bound transfer without a concrete physical caller and all added costs.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first explicit twenty-gate restricted word and complete disjoint radius-nine and radius-ten balls excluding every shorter word.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and normal/optimized verify.py; all 32 literal inputs, twenty gate-deletion controls and complete restricted matrix neighborhoods.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a concrete native caller use this clockwise-local stencil as a cheaper complete adapter?",
+      "why_it_matters": "The exact scalar optimum does not by itself price native delivery or reduce a recursive invoice.",
+      "first_step": "Identify one actual five-role cyclic layout and its source/target boundary; charge every conversion, native phase, alias and restoration.",
+      "blocked_by": "No compatible physical caller, ownership contract or complete invoice is supplied."
+    }
+  ],
+  "related_work": [
+    {
+      "pr": 5793,
+      "head": "9ddb022cc1d879a5d3173f8f1f526a2ff504e7b3",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5793",
+      "role": "Classical finite-group synthesis interface limited to four roles; motivation only, not imported or replayed."
+    },
+    {
+      "pr": 1188,
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1188",
+      "role": "Prior complete unrestricted twenty-generator GL5 metric, credited and cited without replay; it does not determine the five-generator clockwise metric."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216913",
+  "scope_correction_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217027"
+}

research/five-role-cyclic-parity/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact twenty-step clockwise endpoint; complete 9+10 meet-in-the-middle exclusion; all 32 inputs, reversed word, twenty deletion controls, nine malformed inputs and a known nineteen-gate positive meet."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact twenty-step clockwise endpoint; complete 9+10 meet-in-the-middle exclusion; all 32 inputs, reversed word, twenty deletion controls, nine malformed inputs and a known nineteen-gate positive meet."
+    }
+  ]
+}