From d68db890c1944a7bcbf5217b59e8771568db20e0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:43:18 +0000 Subject: [PATCH 1/2] feat(research): prove nine-XOR five-role cyclic parity minimum --- research/five-role-cyclic-parity/PROOF.md | 99 ++++++++++++ research/five-role-cyclic-parity/README.md | 102 +++++++++++++ research/five-role-cyclic-parity/SOURCES.json | 18 +++ research/five-role-cyclic-parity/TASK.json | 84 ++++++++++ research/five-role-cyclic-parity/VERIFY.json | 34 +++++ research/five-role-cyclic-parity/verify.py | 143 ++++++++++++++++++ 6 files changed, 480 insertions(+) create mode 100644 research/five-role-cyclic-parity/PROOF.md create mode 100644 research/five-role-cyclic-parity/README.md create mode 100644 research/five-role-cyclic-parity/SOURCES.json create mode 100644 research/five-role-cyclic-parity/TASK.json create mode 100644 research/five-role-cyclic-parity/VERIFY.json create mode 100644 research/five-role-cyclic-parity/verify.py diff --git a/research/five-role-cyclic-parity/PROOF.md b/research/five-role-cyclic-parity/PROOF.md new file mode 100644 index 0000000000..3f744cefe4 --- /dev/null +++ b/research/five-role-cyclic-parity/PROOF.md @@ -0,0 +1,99 @@ +# Nine XORs are necessary and sufficient + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Endpoint and alphabet + +There are five registers containing independent arbitrary vectors over F2. +Register indices are zero-based. The only paid instruction is +`r_dst += r_src`, with distinct source and destination. Each 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 workspace, free permutation, basis change, initialization, erasure or +nonlinear/data-dependent instruction is allowed. The endpoint coefficient +matrix has row masks `(7,14,28,25,19)`, with bit j denoting input x_j. + +## Attainment + +The following ordered word has nine instructions. The left index is the +source; the right index is the destination. + +``` +0 -> 2 +0 -> 4 +3 -> 0 +4 -> 3 +1 -> 4 +0 -> 1 +2 -> 1 +1 -> 0 +3 -> 2 +``` + +Literal substitution of symbolic row masks gives the required matrix. The +verifier also executes this word on all 32 independent scalar bit inputs. +These scalar inputs exhaust F2^5 and include a basis. A linear identity on +this basis holds on arbitrary vector payloads, coordinatewise. The word is +invertible because every instruction is an involution; reversing it recovers +all five arbitrary inputs. Thus nine is an upper bound. + +## Exhaustive lower bound + +Encode a 5-by-5 binary matrix by its five consecutive five-bit rows in a +25-bit unsigned integer. A directed addition from s to d changes the state +by XORing the s-th row into the d-th row. This is exactly `step` in verify.py. +There are twenty distinct allowed gates. They are all involutions. + +For a center M, define B_0(M)={M}. Iteratively form all twenty neighbors of +every matrix at exact distance k, discard matrices seen at smaller distance, +and retain the new matrices as layer k+1. Induction on k proves that this +algorithm enumerates every state reachable by at most k+1 instructions: +a word of positive length consists of a shorter word followed by an allowed +gate. Discarding a repeated state cannot remove a shorter path or its possible +continuations. No length ordering, pivot heuristic or symmetry quotient prunes +the search. The domain has at most 2^25 matrices. + +The exact layer sizes through radius four are + +``` +center radius 0 1 2 3 4 total +identity 1 20 260 2570 19680 22531 +target (7,14,28,25,19) 1 20 260 2570 19680 22531 +``` + +The two complete balls have empty intersection. These counts and the empty +intersection are enumerated afresh by the standalone verifier, rather than +accepted from a saved search report. + +If a word of length l<=8 connected the identity to the target, cut it after +min(l,4) gates. Its intermediate matrix would lie within four gates of the +identity. It would also lie within four gates of the target, by reversing +the remaining involutions. It would therefore belong to both balls, a +contradiction. Thus the minimum is at least nine. Together with the explicit +word, the exact minimum is nine. + +This is a finite computer-assisted certificate with a written reduction to +arbitrary vector inputs. The exhaustive enumeration and its Python execution +are trusted; no proof kernel or independent human review is claimed. + +## Checks and boundaries + +A separate literal bit interpreter checks every input, full input recovery, +and a counterexample after deletion of each of the nine instructions. It does +not use the packed-matrix update to compute the truth table. An eight-gate +prefix of the witness supplies a positive control for the neighborhood method: +its known four-gate midpoint belongs to both radius-four balls. Nine malformed +input/program controls reject. All checks use explicit exceptions under -O. + +The result is a scalar binary linear-circuit minimum. It is not a native +operator identity with phases, a physically priced adapter, a recursive paid +child minimum, a new kappa or a complete multiplication theorem. Ali Romman's +PR #5793 supplies the related bounded synthesis interface and its four-role +limit, cited as motivation. No predecessor executable or certificate is +imported, rechecked or modified. Classical shortest paths and the +meet-in-the-middle argument retain their usual mathematical credit. Global +literature priority for this endpoint is unclaimed. diff --git a/research/five-role-cyclic-parity/README.md b/research/five-role-cyclic-parity/README.md new file mode 100644 index 0000000000..8e146fe83e --- /dev/null +++ b/research/five-role-cyclic-parity/README.md @@ -0,0 +1,102 @@ +# The five-role cyclic parity stencil needs exactly nine XORs + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: finite certificate with a written reduction to arbitrary binary +vector inputs. The complete invertible map + +``` +y_i = x_i + x_(i+1 mod 5) + x_(i+2 mod 5), 0 <= i < 5, +``` + +has exact minimum cost nine when each directed register addition costs one. +All five initial registers are arbitrary. No workspace or free basis operation +is allowed. [PROOF.md](PROOF.md) displays a nine-instruction word and explains +the exhaustive lower bound. The complete radius-four neighborhoods of the +identity and target each contain 22,531 matrices and are disjoint, excluding +every word of length at most eight. + +This answers one concrete larger-domain synthesis question beyond the four-role +limit in [Ali Romman's PR #5793](https://github.com/CrocSwap/integer-mult-bounds/pull/5793), +head `9ddb022cc1d879a5d3173f8f1f526a2ff504e7b3`. That predecessor is motivation, +not a scientific input or executable dependency. The new endpoint and finite +exclusion are the contribution here. Finite-group shortest paths and +meet-in-the-middle exclusion are classical; 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 used CPython 3.12.15 on macOS 27.0.1 arm64. +Another CPython 3.12 interpreter may replace that absolute path. Both registered +commands have a 120-second bound. The direct verifier needs neither Git nor +network and writes no files. It emits `PASS_FIVE_ROLE_CYCLIC_PARITY` in a generated +JSON receipt containing the SHA256 hashes of all six package files. No receipt +is handwritten. Historical catalogue and selected-record pins in +[SOURCES.json](SOURCES.json) provide provenance; they are not live math inputs. + +The verifier re-enumerates all three radius-four balls, including the known +eight-gate positive control, then checks all 32 literal input bit patterns, +the reversed word, nine deleted-gate controls and nine malformed-input controls. +The counts measure labeled matrices, with no quotient by wire permutations. +The lower bound quantifies over every finite word shorter than nine, not merely +one search grammar or a selected list of Gaussian eliminations. + +## Scope and limits + +The original `complex-rank-shape-decoder` card is explicitly changed to this +scalar linear-synthesis side result in [TASK.json](TASK.json). Current selected +metadata orientation passed on canonical main +`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. The selected +conditional kappa is unchanged. This package does not bind the stencil to an +actual source-native caller or meet the card's complete-supplier gate. + +Other endpoints, additional dirty or clean roles, free basis changes, nonlinear +instructions, odd characteristic and unequal gate prices are outside scope. +Native phases, route and ownership legality, restoration costs, rounding, +physical tapes, full recursive invoices and supplier admission remain open. +No selected cold replay, Lean or Docker run is needed or claimed. Independent +human and formal proof-kernel review are unclaimed. + +Power of Ten inspection is confined to the new verifier. All loops are bounded +by five roles, twenty gates, four search layers, 32 inputs or nine witness gates. +Each search ball contains at most `1+20+20^2+20^3+20^4=168421` generated-word +endpoints, before deduplication. The actual retained ball has 22,531 matrices. +Functions fit within 60 lines, use no recursion, subprocesses or dynamic code, +and keep all mutable search state local. Boundary checks reject malformed +literal inputs. Mathematical checks remain active under optimization. Rule 3 +has a managed-runtime deviation: Python allocates bounded integers, tuples +and sets during the finite command. The fixed domains above bound retained +storage; this is not a steady service. Warning-strict ordinary and optimized +execution and in-memory syntax compilation provide diagnostics. + +## Open next questions + +Can one actual native caller use this stencil as a cheaper complete adapter? +First identify its exact five-role source and target boundary, then charge +aliases, native phases, conversions, ownership and every restoration operation. +No compatible caller or complete paid invoice is supplied. A nine-XOR scalar +minimum alone does not imply a recursive gain. No follow-up is reserved. + +## Related work and credit + +Ali Romman #5793 supplies the custom-alphabet finite-group synthesis interface +and its explicit four-role boundary. Its cited zero-frame feedback censuses +retain their separate source contracts and attribution. No predecessor code is +copied or replayed. PR #5898 concerns four arbitrary data inputs and a zero +helper with a bank-exchange endpoint; this contribution has five arbitrary +inputs and a nonpermutation full-rank endpoint. The two scalar minima are for +different contracts. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216913) +preceded the substantive search. Live PR bodies, recent account submissions, +main README formulas, merged PRs, current Discussions and local reservations +were checked. Cached overlap coverage has freshness and sparse-checkout limits; +these searches cannot establish absence of unpublished overlap. diff --git a/research/five-role-cyclic-parity/SOURCES.json b/research/five-role-cyclic-parity/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/five-role-cyclic-parity/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/five-role-cyclic-parity/TASK.json b/research/five-role-cyclic-parity/TASK.json new file mode 100644 index 0000000000..5793102daf --- /dev/null +++ b/research/five-role-cyclic-parity/TASK.json @@ -0,0 +1,84 @@ +{ + "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 nine directed scalar XOR additions for the complete five-role binary cyclic three-tap parity map, with no workspace or free basis operations.", + "scope_change_reason": "The assigned decoder card is narrowed to a scalar linear-synthesis side result beyond the four-role limit of another contributor's PR5793. No legal native supplier or signed-moment gain is claimed.", + "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 attaining word and complete radius-four exclusion of every word of length at most eight.", + "outcome": "completed", + "evidence": "PROOF.md and warning-strict normal/optimized verify.py; all 32 input bit patterns and complete finite 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 complete five-role stencil as a cheaper linear adapter?", + "why_it_matters": "The exact scalar minimum alone does not improve the complete recursive invoice.", + "first_step": "Identify one actual five-role source/target boundary and include native phases, aliases and every conversion and restoration cost.", + "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." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216913" +} diff --git a/research/five-role-cyclic-parity/VERIFY.json b/research/five-role-cyclic-parity/VERIFY.json new file mode 100644 index 0000000000..96242d2a27 --- /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 nine-step endpoint, full radius-four meet-in-the-middle exclusion, all 32 literal inputs, inverse and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same finite certificate with optimization enabled; all mathematical checks use explicit exceptions." + } + ] +} diff --git a/research/five-role-cyclic-parity/verify.py b/research/five-role-cyclic-parity/verify.py new file mode 100644 index 0000000000..5a94106d6b --- /dev/null +++ b/research/five-role-cyclic-parity/verify.py @@ -0,0 +1,143 @@ +#!/usr/bin/env python3 +"""Exact nine-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, dst) for src in range(WIDTH) + for dst in range(WIDTH) if src != dst) +WORD = ((0, 2), (0, 4), (3, 0), (4, 3), (1, 4), + (0, 1), (2, 1), (1, 0), (3, 2)) +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): + """Enumerate all words of length at most four, merging equal matrices.""" + seen = {center} + frontier = {center} + counts = [1] + for _ in range(4): + 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) <= 9 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(9): + 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": 9, + "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) + backward, bcounts = ball(target) + require(fcounts == [1, 20, 260, 2570, 19680], "identity radius counts") + require(bcounts == fcounts, "target radius counts") + intersection = forward.intersection(backward) + require(not intersection, "a word of at most eight XORs exists") + # A known eight-gate endpoint must be detected by the same exclusion method. + midpoint = identity + for gate in WORD[:4]: + midpoint = step(midpoint, gate) + require(midpoint in forward, "known four-gate midpoint missing") + short_endpoint = literal_matrix(WORD[:8], identity) + nearby, nearcounts = ball(short_endpoint) + require(midpoint in nearby and nearcounts == fcounts, "false-negative control") + require(not (forward & backward), "negative certificate changed") + 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": 9, "target_rows": rows, "word": WORD, + "forward_layers": fcounts, "backward_layers": bcounts, + "ball_size": len(forward), "intersection_size": len(intersection), + "eight_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() From d3d1e2155620e2a491523c759e1569587678b922 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:49:09 +0000 Subject: [PATCH 2/2] feat(research): prove twenty-XOR clockwise parity minimum --- research/five-role-cyclic-parity/PROOF.md | 135 +++++++++-------- research/five-role-cyclic-parity/README.md | 137 ++++++++---------- research/five-role-cyclic-parity/SOURCES.json | 6 + research/five-role-cyclic-parity/TASK.json | 22 ++- research/five-role-cyclic-parity/VERIFY.json | 4 +- research/five-role-cyclic-parity/verify.py | 57 ++++---- 6 files changed, 179 insertions(+), 182 deletions(-) diff --git a/research/five-role-cyclic-parity/PROOF.md b/research/five-role-cyclic-parity/PROOF.md index 3f744cefe4..e7225bd917 100644 --- a/research/five-role-cyclic-parity/PROOF.md +++ b/research/five-role-cyclic-parity/PROOF.md @@ -1,99 +1,96 @@ -# Nine XORs are necessary and sufficient +# Twenty clockwise XORs are necessary and sufficient This contribution was produced by Nick Petalas. Apache-2.0. ## Endpoint and alphabet -There are five registers containing independent arbitrary vectors over F2. -Register indices are zero-based. The only paid instruction is -`r_dst += r_src`, with distinct source and destination. Each instruction costs -one. The requested complete output is +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 workspace, free permutation, basis change, initialization, erasure or -nonlinear/data-dependent instruction is allowed. The endpoint coefficient +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 nine instructions. The left index is the -source; the right index is the destination. +The following ordered word has twenty instructions. Each pair is source, +destination, and every pair is one of the five allowed clockwise edges. ``` -0 -> 2 -0 -> 4 -3 -> 0 -4 -> 3 -1 -> 4 -0 -> 1 -2 -> 1 -1 -> 0 -3 -> 2 +(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 substitution of symbolic row masks gives the required matrix. The -verifier also executes this word on all 32 independent scalar bit inputs. -These scalar inputs exhaust F2^5 and include a basis. A linear identity on -this basis holds on arbitrary vector payloads, coordinatewise. The word is -invertible because every instruction is an involution; reversing it recovers -all five arbitrary inputs. Thus nine is an upper bound. +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 a 5-by-5 binary matrix by its five consecutive five-bit rows in a -25-bit unsigned integer. A directed addition from s to d changes the state -by XORing the s-th row into the d-th row. This is exactly `step` in verify.py. -There are twenty distinct allowed gates. They are all involutions. +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. -For a center M, define B_0(M)={M}. Iteratively form all twenty neighbors of -every matrix at exact distance k, discard matrices seen at smaller distance, -and retain the new matrices as layer k+1. Induction on k proves that this -algorithm enumerates every state reachable by at most k+1 instructions: -a word of positive length consists of a shorter word followed by an allowed -gate. Discarding a repeated state cannot remove a shorter path or its possible -continuations. No length ordering, pivot heuristic or symmetry quotient prunes -the search. The domain has at most 2^25 matrices. +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 exact layer sizes through radius four are +The complete enumerated exact-distance layers are ``` -center radius 0 1 2 3 4 total -identity 1 20 260 2570 19680 22531 -target (7,14,28,25,19) 1 20 260 2570 19680 22531 +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 two complete balls have empty intersection. These counts and the empty -intersection are enumerated afresh by the standalone verifier, rather than -accepted from a saved search report. +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<=8 connected the identity to the target, cut it after -min(l,4) gates. Its intermediate matrix would lie within four gates of the -identity. It would also lie within four gates of the target, by reversing -the remaining involutions. It would therefore belong to both balls, a -contradiction. Thus the minimum is at least nine. Together with the explicit -word, the exact minimum is nine. +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 inputs. The exhaustive enumeration and its Python execution -are trusted; no proof kernel or independent human review is claimed. - -## Checks and boundaries - -A separate literal bit interpreter checks every input, full input recovery, -and a counterexample after deletion of each of the nine instructions. It does -not use the packed-matrix update to compute the truth table. An eight-gate -prefix of the witness supplies a positive control for the neighborhood method: -its known four-gate midpoint belongs to both radius-four balls. Nine malformed -input/program controls reject. All checks use explicit exceptions under -O. - -The result is a scalar binary linear-circuit minimum. It is not a native -operator identity with phases, a physically priced adapter, a recursive paid -child minimum, a new kappa or a complete multiplication theorem. Ali Romman's -PR #5793 supplies the related bounded synthesis interface and its four-role -limit, cited as motivation. No predecessor executable or certificate is -imported, rechecked or modified. Classical shortest paths and the -meet-in-the-middle argument retain their usual mathematical credit. Global -literature priority for this endpoint is unclaimed. +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 index 8e146fe83e..35099fd622 100644 --- a/research/five-role-cyclic-parity/README.md +++ b/research/five-role-cyclic-parity/README.md @@ -1,27 +1,28 @@ -# The five-role cyclic parity stencil needs exactly nine XORs +# 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. The complete invertible map +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 nine when each directed register addition costs one. -All five initial registers are arbitrary. No workspace or free basis operation -is allowed. [PROOF.md](PROOF.md) displays a nine-instruction word and explains -the exhaustive lower bound. The complete radius-four neighborhoods of the -identity and target each contain 22,531 matrices and are disjoint, excluding -every word of length at most eight. - -This answers one concrete larger-domain synthesis question beyond the four-role -limit in [Ali Romman's PR #5793](https://github.com/CrocSwap/integer-mult-bounds/pull/5793), -head `9ddb022cc1d879a5d3173f8f1f526a2ff504e7b3`. That predecessor is motivation, -not a scientific input or executable dependency. The new endpoint and finite -exclusion are the contribution here. Finite-group shortest paths and -meet-in-the-middle exclusion are classical; literature priority is unclaimed. +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 @@ -34,69 +35,55 @@ From the worktree root, with the CPython 3.12 standard library: /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 used CPython 3.12.15 on macOS 27.0.1 arm64. -Another CPython 3.12 interpreter may replace that absolute path. Both registered -commands have a 120-second bound. The direct verifier needs neither Git nor -network and writes no files. It emits `PASS_FIVE_ROLE_CYCLIC_PARITY` in a generated -JSON receipt containing the SHA256 hashes of all six package files. No receipt -is handwritten. Historical catalogue and selected-record pins in -[SOURCES.json](SOURCES.json) provide provenance; they are not live math inputs. - -The verifier re-enumerates all three radius-four balls, including the known -eight-gate positive control, then checks all 32 literal input bit patterns, -the reversed word, nine deleted-gate controls and nine malformed-input controls. -The counts measure labeled matrices, with no quotient by wire permutations. -The lower bound quantifies over every finite word shorter than nine, not merely -one search grammar or a selected list of Gaussian eliminations. +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 original `complex-rank-shape-decoder` card is explicitly changed to this -scalar linear-synthesis side result in [TASK.json](TASK.json). Current selected -metadata orientation passed on canonical main -`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. The selected -conditional kappa is unchanged. This package does not bind the stencil to an -actual source-native caller or meet the card's complete-supplier gate. - -Other endpoints, additional dirty or clean roles, free basis changes, nonlinear -instructions, odd characteristic and unequal gate prices are outside scope. -Native phases, route and ownership legality, restoration costs, rounding, -physical tapes, full recursive invoices and supplier admission remain open. -No selected cold replay, Lean or Docker run is needed or claimed. Independent -human and formal proof-kernel review are unclaimed. - -Power of Ten inspection is confined to the new verifier. All loops are bounded -by five roles, twenty gates, four search layers, 32 inputs or nine witness gates. -Each search ball contains at most `1+20+20^2+20^3+20^4=168421` generated-word -endpoints, before deduplication. The actual retained ball has 22,531 matrices. -Functions fit within 60 lines, use no recursion, subprocesses or dynamic code, -and keep all mutable search state local. Boundary checks reject malformed -literal inputs. Mathematical checks remain active under optimization. Rule 3 -has a managed-runtime deviation: Python allocates bounded integers, tuples -and sets during the finite command. The fixed domains above bound retained -storage; this is not a steady service. Warning-strict ordinary and optimized -execution and in-memory syntax compilation provide diagnostics. +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 one actual native caller use this stencil as a cheaper complete adapter? -First identify its exact five-role source and target boundary, then charge -aliases, native phases, conversions, ownership and every restoration operation. -No compatible caller or complete paid invoice is supplied. A nine-XOR scalar -minimum alone does not imply a recursive gain. No follow-up is reserved. - -## Related work and credit - -Ali Romman #5793 supplies the custom-alphabet finite-group synthesis interface -and its explicit four-role boundary. Its cited zero-frame feedback censuses -retain their separate source contracts and attribution. No predecessor code is -copied or replayed. PR #5898 concerns four arbitrary data inputs and a zero -helper with a bank-exchange endpoint; this contribution has five arbitrary -inputs and a nonpermutation full-rank endpoint. The two scalar minima are for -different contracts. - -The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216913) -preceded the substantive search. Live PR bodies, recent account submissions, -main README formulas, merged PRs, current Discussions and local reservations -were checked. Cached overlap coverage has freshness and sparse-checkout limits; -these searches cannot establish absence of unpublished overlap. +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 index fdb80ada25..7365e4a5ac 100644 --- a/research/five-role-cyclic-parity/SOURCES.json +++ b/research/five-role-cyclic-parity/SOURCES.json @@ -13,6 +13,12 @@ "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 index 5793102daf..60f520fe75 100644 --- a/research/five-role-cyclic-parity/TASK.json +++ b/research/five-role-cyclic-parity/TASK.json @@ -55,20 +55,20 @@ ] }, "scope_status": "changed", - "actual_scope": "Prove the exact minimum of nine directed scalar XOR additions for the complete five-role binary cyclic three-tap parity map, with no workspace or free basis operations.", - "scope_change_reason": "The assigned decoder card is narrowed to a scalar linear-synthesis side result beyond the four-role limit of another contributor's PR5793. No legal native supplier or signed-moment gain is claimed.", + "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 attaining word and complete radius-four exclusion of every word of length at most eight.", + "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 warning-strict normal/optimized verify.py; all 32 input bit patterns and complete finite matrix neighborhoods.", + "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 complete five-role stencil as a cheaper linear adapter?", - "why_it_matters": "The exact scalar minimum alone does not improve the complete recursive invoice.", - "first_step": "Identify one actual five-role source/target boundary and include native phases, aliases and every conversion and restoration cost.", + "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." } ], @@ -78,7 +78,13 @@ "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" + "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 index 96242d2a27..6ca49b094c 100644 --- a/research/five-role-cyclic-parity/VERIFY.json +++ b/research/five-role-cyclic-parity/VERIFY.json @@ -15,7 +15,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Exact nine-step endpoint, full radius-four meet-in-the-middle exclusion, all 32 literal inputs, inverse and rejection controls." + "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": [ @@ -28,7 +28,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Same finite certificate with optimization enabled; all mathematical checks use explicit exceptions." + "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 index 5a94106d6b..4e8ad2b981 100644 --- a/research/five-role-cyclic-parity/verify.py +++ b/research/five-role-cyclic-parity/verify.py @@ -1,15 +1,17 @@ #!/usr/bin/env python3 -"""Exact nine-XOR cyclic parity minimum. Produced by Nick Petalas; Apache-2.0.""" +"""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, dst) for src in range(WIDTH) - for dst in range(WIDTH) if src != dst) -WORD = ((0, 2), (0, 4), (3, 0), (4, 3), (1, 4), - (0, 1), (2, 1), (1, 0), (3, 2)) +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") @@ -31,12 +33,13 @@ def step(state, gate): return state ^ (((state >> (WIDTH * src)) & MASK) << (WIDTH * dst)) -def ball(center): - """Enumerate all words of length at most four, merging equal matrices.""" +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(4): + for _ in range(radius): following = set() for state in frontier: for gate in GATES: @@ -52,7 +55,7 @@ def ball(center): def literal_word(value, word): require(type(value) is int and 0 <= value <= MASK, "invalid input") - require(len(word) <= 9 and all(g in GATES for g in word), "invalid word") + 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] @@ -76,7 +79,7 @@ def check_word_and_controls(identity, target): 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(9): + 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") @@ -93,7 +96,7 @@ def check_word_and_controls(identity, target): except ValueError: continue raise ValueError("invalid matrix accepted") - return {"truth_table_inputs": 32, "deleted_gate_controls": 9, + return {"truth_table_inputs": 32, "deleted_gate_controls": 20, "invalid_input_controls": 9} @@ -103,21 +106,18 @@ def main(): | (1 << ((i + 2) % WIDTH)) for i in range(WIDTH)] target = encode(rows) controls = check_word_and_controls(identity, target) - forward, fcounts = ball(identity) - backward, bcounts = ball(target) - require(fcounts == [1, 20, 260, 2570, 19680], "identity radius counts") - require(bcounts == fcounts, "target radius counts") + 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 eight XORs exists") - # A known eight-gate endpoint must be detected by the same exclusion method. - midpoint = identity - for gate in WORD[:4]: - midpoint = step(midpoint, gate) - require(midpoint in forward, "known four-gate midpoint missing") - short_endpoint = literal_matrix(WORD[:8], identity) - nearby, nearcounts = ball(short_endpoint) - require(midpoint in nearby and nearcounts == fcounts, "false-negative control") - require(not (forward & backward), "negative certificate changed") + 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: @@ -125,10 +125,11 @@ def main(): 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": 9, "target_rows": rows, "word": WORD, + "minimum_xors": 20, "alphabet": GATES, "target_rows": rows, "word": WORD, "forward_layers": fcounts, "backward_layers": bcounts, - "ball_size": len(forward), "intersection_size": len(intersection), - "eight_gate_positive_controls": 1, **controls, "sha256": hashes} + "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))