diff --git a/research/five-role-cyclic-parity/PROOF.md b/research/five-role-cyclic-parity/PROOF.md new file mode 100644 index 0000000000..e7225bd917 --- /dev/null +++ b/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. diff --git a/research/five-role-cyclic-parity/README.md b/research/five-role-cyclic-parity/README.md new file mode 100644 index 0000000000..35099fd622 --- /dev/null +++ b/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. diff --git a/research/five-role-cyclic-parity/SOURCES.json b/research/five-role-cyclic-parity/SOURCES.json new file mode 100644 index 0000000000..7365e4a5ac --- /dev/null +++ b/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" + } + ] +} diff --git a/research/five-role-cyclic-parity/TASK.json b/research/five-role-cyclic-parity/TASK.json new file mode 100644 index 0000000000..60f520fe75 --- /dev/null +++ b/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" +} diff --git a/research/five-role-cyclic-parity/VERIFY.json b/research/five-role-cyclic-parity/VERIFY.json new file mode 100644 index 0000000000..6ca49b094c --- /dev/null +++ b/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." + } + ] +} diff --git a/research/five-role-cyclic-parity/verify.py b/research/five-role-cyclic-parity/verify.py new file mode 100644 index 0000000000..4e8ad2b981 --- /dev/null +++ b/research/five-role-cyclic-parity/verify.py @@ -0,0 +1,144 @@ +#!/usr/bin/env python3 +"""Exact clockwise twenty-XOR cyclic parity minimum. Produced by Nick Petalas; Apache-2.0.""" +from hashlib import sha256 +import json +from pathlib import Path + +WIDTH = 5 +MASK = 31 +GATES = tuple((src, (src + 1) % WIDTH) for src in range(WIDTH)) +WORD = ((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)) +LAYERS = (1, 5, 15, 40, 100, 240, 555, 1230, 2665, 5715, 12010) +FILES = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def encode(rows): + require(len(rows) == WIDTH, "exactly five rows required") + require(all(type(r) is int and 0 <= r <= MASK for r in rows), "invalid row") + return sum(row << (WIDTH * i) for i, row in enumerate(rows)) + + +def step(state, gate): + src, dst = gate + require(type(state) is int and 0 <= state < 1 << 25, "invalid matrix") + require(gate in GATES, "invalid directed XOR") + return state ^ (((state >> (WIDTH * src)) & MASK) << (WIDTH * dst)) + + +def ball(center, radius): + """Enumerate every allowed word through a bounded radius, merging matrices.""" + require(type(radius) is int and 0 <= radius <= 10, "invalid radius") + seen = {center} + frontier = {center} + counts = [1] + for _ in range(radius): + following = set() + for state in frontier: + for gate in GATES: + nxt = step(state, gate) + if nxt not in seen: + following.add(nxt) + require(not seen.intersection(following), "distance layers overlap") + seen.update(following) + frontier = following + counts.append(len(frontier)) + return seen, counts + + +def literal_word(value, word): + require(type(value) is int and 0 <= value <= MASK, "invalid input") + require(len(word) <= 20 and all(g in GATES for g in word), "invalid word") + registers = [(value >> i) & 1 for i in range(WIDTH)] + for src, dst in word: + registers[dst] ^= registers[src] + return sum(bit << i for i, bit in enumerate(registers)) + + +def literal_target(value): + return sum((((value >> i) ^ (value >> ((i + 1) % WIDTH)) + ^ (value >> ((i + 2) % WIDTH))) & 1) << i + for i in range(WIDTH)) + + +def check_word_and_controls(identity, target): + state = identity + for gate in WORD: + old = state + state = step(state, gate) + require(step(state, gate) == old, "gate is not involutive") + require(state == target, "word has the wrong complete endpoint") + outputs = [literal_word(value, WORD) for value in range(32)] + require(outputs == [literal_target(value) for value in range(32)], "truth table") + require(len(set(outputs)) == 32, "endpoint loses arbitrary input information") + require(all(literal_word(outputs[v], WORD[::-1]) == v for v in range(32)), "inverse") + for omitted in range(20): + shorter = WORD[:omitted] + WORD[omitted + 1:] + require(any(literal_word(v, shorter) != literal_target(v) + for v in range(32)), "omitted gate was undetected") + for value, word in ((-1, WORD), (32, WORD), (True, WORD), (0, ((0, 0),)), + (0, ((5, 0),)), (0, WORD + WORD)): + try: + literal_word(value, word) + except ValueError: + continue + raise ValueError("invalid literal program accepted") + for rows in ((1, 2), (1, 2, 4, 8, 32), (True, 2, 4, 8, 16)): + try: + encode(rows) + except ValueError: + continue + raise ValueError("invalid matrix accepted") + return {"truth_table_inputs": 32, "deleted_gate_controls": 20, + "invalid_input_controls": 9} + + +def main(): + identity = encode([1 << i for i in range(WIDTH)]) + rows = [(1 << i) | (1 << ((i + 1) % WIDTH)) + | (1 << ((i + 2) % WIDTH)) for i in range(WIDTH)] + target = encode(rows) + controls = check_word_and_controls(identity, target) + forward, fcounts = ball(identity, 9) + backward, bcounts = ball(target, 10) + require(fcounts == list(LAYERS[:10]), "identity radius counts") + require(bcounts == list(LAYERS), "target radius counts") + intersection = forward.intersection(backward) + require(not intersection, "a word of at most nineteen XORs exists") + # Detect a known nineteen-gate endpoint using the same 9+10 method. + midpoint = literal_matrix(WORD[:9], identity) + require(midpoint in forward, "known nine-gate midpoint missing") + short_endpoint = literal_matrix(WORD[:19], identity) + nearby, nearcounts = ball(short_endpoint, 10) + require(midpoint in nearby and nearcounts == bcounts, "false-negative control") + root = Path(__file__).resolve().parent + hashes = {} + for name in FILES: + path = root / name + require(path.is_file() and path.stat().st_size <= 1 << 20, "source size") + hashes[name] = sha256(path.read_bytes()).hexdigest() + receipt = {"status": "PASS_FIVE_ROLE_CYCLIC_PARITY", "claim_type": "finite certificate", + "minimum_xors": 20, "alphabet": GATES, "target_rows": rows, "word": WORD, + "forward_layers": fcounts, "backward_layers": bcounts, + "forward_ball_size": len(forward), "backward_ball_size": len(backward), + "intersection_size": len(intersection), + "nineteen_gate_positive_controls": 1, **controls, "sha256": hashes} + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +def literal_matrix(word, identity): + state = identity + for gate in word: + state = step(state, gate) + return state + + +if __name__ == "__main__": + main()