diff --git a/research/a5-eight-bit-carrier/OVERLAP.json b/research/a5-eight-bit-carrier/OVERLAP.json new file mode 100644 index 0000000000..bdee855b2c --- /dev/null +++ b/research/a5-eight-bit-carrier/OVERLAP.json @@ -0,0 +1,41 @@ +{ + "coverage": { + "discussions": { + "complete_pagination": true, + "fetched_at": "2026-10-23T09:30:12.163990+00:00", + "records": 4238 + }, + "local": { + "complete_head_inventory": false, + "head": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "head_records": 6824, + "records": 129, + "unsearched_head_paths_count": 6695 + }, + "open_prs": { + "complete_pagination": true, + "fetched_at": "2026-10-23T09:29:21.757181+00:00", + "records": 322 + } + }, + "focused_query": { + "any_of": [ + "SL2(F4)", + "eight-bit", + "regular orbit" + ], + "required": "A5" + }, + "matches": { + "discussions": [], + "open_prs": [] + }, + "related_open_work": [ + { + "number": 3914, + "relation": "Additive-caller collapse obstruction; this construction changes to an explicit nonabelian binary affine carrier.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3914" + } + ], + "scope": "Historical coordination snapshot, not a novelty certificate or mathematical verification. No arbitrary diffs or unpublished work covered." +} diff --git a/research/a5-eight-bit-carrier/README.md b/research/a5-eight-bit-carrier/README.md new file mode 100644 index 0000000000..aa13ba0a0b --- /dev/null +++ b/research/a5-eight-bit-carrier/README.md @@ -0,0 +1,194 @@ +# An eight-bit algebra-faithful A5 address carrier + +This contribution is produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Result and boundary + +The formal A5 alphabet in Wentao Li's [#4089](https://github.com/CrocSwap/integer-mult-bounds/pull/4089) +has an explicit action on eight binary address bits whose extension to +`F2[A5]` is injective. The two generators have literal address circuits of +4 and 12 CNOTs. On a 256-entry array, fixed in-place programs implement the +same permutations with 360 and 510 data XORs, using no extra data bit. +Every input entry may be arbitrary. One natural four-bit copy distinguishes +the 60 group elements but fails to preserve the formal group algebra. +Two copies are therefore necessary and sufficient within this particular +natural-module replication family. + +Claim type: a finite exact construction with a scoped algebraic proof. +This supplies a concrete nonabelian address carrier for the escape route +identified by Cinna Davis's [#3914](https://github.com/CrocSwap/integer-mult-bounds/pull/3914). +It does not supply an admitted BIT supplier, a recursive child invoice, +a physical fixed-tape implementation, or a new kappa. No minimum over all +binary affine representations, or optimal CNOT circuit, is asserted. + +## Construction + +Write `F4=F2[w]/(w^2+w+1)`, encode `a+bw` as `a+2b`, and set + +```text +X = [1 1] Y = [ 0 w] + [0 1] [w^2 1]. +``` + +Their determinants are one. They correspond to the predecessor's generators +`x=(1 2)(3 4)` and `y=(1 3 5)`. The standalone verifier constructs the paired +closure, obtaining a bijection between all 60 even permutations and all 60 +determinant-one matrices. It checks all 3,600 multiplication pairs, so the +identification uses an exact finite isomorphism rather than an assumed +presentation. The classical isomorphism `A5=SL2(F4)` is not a novelty claim. +No predecessor endpoint search or lower-bound program is replayed. + +Let the address set be `M2(F4)`, a set of 256 elements encoded by eight bits. +A group matrix acts by `M -> gM`, or by its natural four-bit action on +each of the two columns. Define `P_g e_M=e_(gM)` on array basis vectors. +Then `P_g P_h=P_(gh)`. The orbit of the identity matrix is precisely +`SL2(F4)`, and its stabilizer is trivial. Consequently, + +```text +(sum_g c_g P_g) e_I = sum_g c_g e_g. +``` + +The 60 vectors on the right are distinct array basis vectors. Thus a zero +operator forces every `c_g=0`, proving injectivity of the algebra map. +Entrywise application therefore also preserves every matrix identity and +inequality in `M_r(F2[A5])` for arbitrary finite register count `r`. +Here inequality means distinct formal matrices remain distinct operators; +no norm, numerical inequality or implementation tariff is transferred. + +The complete eight-bit orbit inventory is one singleton, five orbits of +size 15, and three regular orbits of size 60. The rank-zero matrix gives +the singleton. A rank-one matrix has one of five row-space lines, and each +such class has 15 elements. Each nonzero determinant gives a 60-element +regular orbit. These disjoint classes account for all 256 addresses. + +## Why one natural copy is insufficient + +On `F4^2`, the natural action has the orbits `{0}` and its 15 nonzero +vectors. The nonzero formal element `J=sum_(g in A5) [g]` acts as zero. +At zero it has multiplicity 60; at every nonzero orbit image it has +multiplicity `60/15=4`. Both are even, so every coefficient vanishes in +`F2`. Yet the action is faithful as a group action: a matrix fixing every +vector fixes a basis and equals the identity. + +This is the obstruction the second copy removes. A faithful group action +alone is insufficient for transferring a full formal group-algebra model. +The regular-orbit criterion is classical; this package provides its explicit +carrier, generator circuits and data programs for the repository's A5 labels. + +## Literal address and data invoices + +For one column use bits `(u0,u1,v0,v1)` with +`u=u0+w*u1`, `v=v0+w*v1`. An ordered pair below means +`target ^= control`. Execute left to right. + +```text +X: (2,0), (3,1) +Y: (0,1), (1,2), (2,1), (3,1), (0,3), (3,0) +``` + +The resulting outputs are + +```text +X: (u0+v0, u1+v1, v0, v1) +Y: (v1, v0+v1, u0+u1+v0, u0+v1). +``` + +Execute each word on bits 0..3 and again with every index increased by +four. This gives 4 and 12 address CNOTs. Address-coordinate instructions +compute a destination index; they are not data-array XOR instructions. + +For an actual data permutation, enumerate each generator's disjoint cycles. +A cycle `(a0,a1,...,ak)` uses swaps `(a0,a1),...,(a0,ak)` in that order. +Each swap uses the three data instructions `A[a]^=A[b]`, `A[b]^=A[a]`, +`A[a]^=A[b]`. No clean temporary or discarded data is needed. The resulting +push action sends the old entry at `M` to `gM`, in the stated orientation. + +X fixes 16 addresses and has 120 two-cycles, giving 120 swaps and 360 data +XORs. Y fixes only zero and has 85 three-cycles, giving 170 swaps and 510 +data XORs. The verifier compares every symbolic input column of both full +programs. These are explicit upper invoices, not optimality claims. + +For q-bit records at each address, run the same data program on each lane. +The counts scale to `360q` and `510q` bit XORs and preserve every input bit. +The tables are fixed finite lists of 120 or 170 pairs of eight-bit addresses. +Their generation, storage and reads have not been lowered to the selected +tape machine. Arbitrary role mixing, non-coordinate rank-one projectors, +source/target frames, ownership, routing, precision, compiler closure and +outer transfer have no paid native implementation supplied here. Those +unknown costs cannot be set to zero. No larger mechanism search is proposed. + +## Reproduction and evidence + +From the repository root, with CPython 3.12 and the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a5-eight-bit-carrier +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a5-eight-bit-carrier/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/a5-eight-bit-carrier/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a5-eight-bit-carrier --check-source-history +``` + +Each direct replay prints `PASS_A5_EIGHT_BIT_CARRIER`. It checks the exact +60-element isomorphism and all multiplication pairs, both complete orbit +inventories, all 60 regular-orbit coefficient columns, the one-copy norm +obstruction on every address, every address circuit input and every symbolic +dirty-data input of both swap programs. Eleven semantic controls cover all eight +single-copy CNOT omissions, noncommutation and the two norm-element tests. +Normal replay authenticates the generated `RESULT.json` against all six +source-file hashes and never rewrites evidence. Only explicit `--write` +regenerates it. Finite enumeration certifies the fixed group and circuits; +the regular-orbit argument proves algebra faithfulness. + +## Sources and overlap + +Scientific base `81e9bd69e4a5b00ba9c713a1620e36d576d5522e`, priority revision 7. +The selected conditional kappa remains 0.00302015. The historical task card +and selected record are provenance, not scientific inputs. SOURCES.json +pins Wentao Li's retained README; its endpoint theorem is cited, not audited. +Cinna Davis's #3914 is a public contextual reference, not a runtime dependency +or an unmerged Git pin. The verifier imports no predecessor code. + +The cached intake covers 322 open PR bodies at 09:29:21 UTC and 4,238 +Discussion records at 09:30:12 UTC on October 23, 2026. +[OVERLAP.json](OVERLAP.json) retains the generated coverage and focused-query +results; the original complete remote snapshot remains local-only. Only 129 local notes +were initially materialized out of 6,824 tracked notes. Main-tree searches +and merged/all-state PR searches supplemented that incomplete local scope. +No matching eight-bit A5 carrier was found within that coverage; arbitrary +diffs and unpublished work remain outside it. The canonical investigation +is [the advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19142735). +The native-carrier question is refined to a fixed finite address realization, +with its missing supplier and tape obligations explicitly retained. + +Credit Wentao Li #4089 for the explicit native-carrier question, Cinna Davis +#2246 for the A5 labels and #3914 for the additive-caller distinction, +and eumemic, Ali Romman and the retained register-model lineage. +Classical finite-field, group representation and reversible XOR-swap +constructions retain their mathematical credit. The new contribution is +this exact carrier and its full local address/data programs. + +## Open next questions + +1. Can one actual BIT caller use the 256-address carrier while preserving its + source/target frames, independent owners and dirty restoration? Start with + one literal rank-one-projector call and price all scalar role changes and + address movement. A source-bound caller and full native tariff are absent. +2. Can an algebra-faithful binary affine A5 action use fewer than eight address + bits? The present one-copy obstruction excludes only the specified natural + four-bit action. Start by classifying candidate six- or seven-bit modules + and checking their full group-algebra kernel. No classification or minimum + over other representations has been established here. + +## Code constraints + +The verifier has no recursion, dynamic code evaluation, network, subprocesses +or predecessor imports. Its finite collections have explicit bounds: 256 +addresses, 60 group states, 3,600 multiplication pairs and at most 170 swaps. +Functions fit within 60 physical lines. `need` checks remain active under +optimization. Python necessarily allocates managed integers and collections; +this is a bounded-runtime deviation from fixed-allocation Power of Ten rule 3. +At most 256 symbolic rows of 256 bits are live in a data-program check, plus +the fixed group and address tables. The interpreter and JSON library allocate +internally. Warning-strict normal and optimized replay are the available +language diagnostics; no repository-wide analyzer configuration is changed. diff --git a/research/a5-eight-bit-carrier/RESULT.json b/research/a5-eight-bit-carrier/RESULT.json new file mode 100644 index 0000000000..3c87bf8767 --- /dev/null +++ b/research/a5-eight-bit-carrier/RESULT.json @@ -0,0 +1,46 @@ +{ + "result": { + "double_copy_orbits": { + "1": 1, + "15": 5, + "60": 3 + }, + "faithful_formal_basis_columns": 60, + "group_order": 60, + "invoices": { + "x": { + "address_cnots": 4, + "cycle_lengths": { + "1": 16, + "2": 120 + }, + "data_swaps": 120, + "data_xors": 360 + }, + "y": { + "address_cnots": 12, + "cycle_lengths": { + "1": 1, + "3": 85 + }, + "data_swaps": 170, + "data_xors": 510 + } + }, + "multiplication_pairs": 3600, + "regular_orbit_seed": 65, + "semantic_controls": 11, + "single_copy_orbits": { + "1": 1, + "15": 1 + } + }, + "source_sha256": { + "OVERLAP.json": "c39383b19e7487e64710c5fc77624f36bbc70a6a3b7084970e11d588d5298cf6", + "README.md": "b6de9f9cdf6da13fb5e7d9b7b145c9fbf5dcf9a96a1c53f5308d846e9107ce18", + "SOURCES.json": "b3d1a91c111053e47cde4962d30be2d2b56b52f7248476ced46a5929bec4c0b1", + "TASK.json": "ed6a3325add8b8e3d7ddaa94985cc9f25f74f198230fd675f3e218e272abf109", + "VERIFY.json": "e6ecce85edb7bd7025ee8261e89736705496939dd25fa3de0b7cfe26896092d7", + "verify.py": "b188de3af8d8292a100316ebebc4c9c4c53b447d275eaf3994ee94fe1ba37236" + } +} diff --git a/research/a5-eight-bit-carrier/SOURCES.json b/research/a5-eight-bit-carrier/SOURCES.json new file mode 100644 index 0000000000..3ee0816c1c --- /dev/null +++ b/research/a5-eight-bit-carrier/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/a5-conjugate-any-registers/README.md", + "usage": "input", + "git_blob": "92fa82d936248c7e3485e4ea3aecac88f42988f9", + "sha256": "26246a1b0448048f59d2a80e09addcf80950d728f2c768e56d32f145c59fd773" + } + ] +} diff --git a/research/a5-eight-bit-carrier/TASK.json b/research/a5-eight-bit-carrier/TASK.json new file mode 100644 index 0000000000..b7e7f5cdbe --- /dev/null +++ b/research/a5-eight-bit-carrier/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "An explicit eight-bit affine A5 carrier with injective formal group-algebra action, a one-natural-copy obstruction and literal address/data programs.", + "scope_change_reason": "Answer only the address-realization part of the other-contributor native-carrier handoff. Do not repeat a formal word search or claim full native admission.", + "bottleneck_link": "A nonabelian formal word cannot serve an additive address caller unchanged; this supplies a faithful concrete address action while retaining the missing full physical and recursive invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified algebra-faithful carrier and exact local programs; no search over smaller representations or larger mechanisms.", + "outcome": "completed", + "evidence": "README.md gives the scoped proof. verify.py checks the explicit isomorphism, all address and dirty-data columns and rejection controls. RESULT.json is generated and hash-bound.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual BIT caller use this carrier with a complete native tariff?", + "why_it_matters": "A finite address action alone is not an admitted recursive supplier.", + "first_step": "Bind one literal rank-one-projector call and price scalar role changes and address movement.", + "blocked_by": "No source-bound caller or full native invoice is provided." + }, + { + "question": "Can an algebra-faithful binary affine A5 action use fewer than eight address bits?", + "why_it_matters": "The specified replication family does not decide other representations.", + "first_step": "Classify six- and seven-bit candidate modules and their full group-algebra kernels.", + "blocked_by": "A module classification and dimension lower bound are absent." + } + ], + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + } +} diff --git a/research/a5-eight-bit-carrier/VERIFY.json b/research/a5-eight-bit-carrier/VERIFY.json new file mode 100644 index 0000000000..cd316318aa --- /dev/null +++ b/research/a5-eight-bit-carrier/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a5-conjugate-any-registers/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact carrier isomorphism, full address and symbolic dirty-data programs, one-copy kernel and eleven controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks with assertions disabled; generated source-hash receipt remains read-only." + } + ] +} diff --git a/research/a5-eight-bit-carrier/verify.py b/research/a5-eight-bit-carrier/verify.py new file mode 100644 index 0000000000..d495e8fa80 --- /dev/null +++ b/research/a5-eight-bit-carrier/verify.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact finite checks for the A5 carrier; no predecessor program is imported.""" +from collections import Counter +from hashlib import sha256 +from itertools import product +import argparse +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +IDENTITY = (1, 0, 0, 1) +X = (1, 1, 0, 1) +Y = (0, 2, 3, 1) +X_WORD = ((2, 0), (3, 1)) +Y_WORD = ((0, 1), (1, 2), (2, 1), (3, 1), (0, 3), (3, 0)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(a, b): + """F4=F2[w]/(w^2+w+1), with a+b*w encoded as a+2*b.""" + value = (a if b & 1 else 0) ^ (a << 1 if b & 2 else 0) + return value ^ (7 if value & 4 else 0) + + +def matrix_product(a, b): + return tuple(multiply(a[2*i], b[j]) ^ multiply(a[2*i+1], b[j+2]) + for i in range(2) for j in range(2)) + + +def determinant(a): + return multiply(a[0], a[3]) ^ multiply(a[1], a[2]) + + +def vector_action(a, value): + u, v = value & 3, value >> 2 + return ((multiply(a[0], u) ^ multiply(a[1], v)) + | ((multiply(a[2], u) ^ multiply(a[3], v)) << 2)) + + +def address_action(a, value, copies): + return sum(vector_action(a, (value >> (4*j)) & 15) << (4*j) + for j in range(copies)) + + +def permutation_product(a, b): + return tuple(a[b[j]] for j in range(5)) + + +def identified_group(): + """Generate paired A5 permutations and matrices with a fixed 120-step cap.""" + start = (tuple(range(5)), IDENTITY) + generators = (((1, 0, 3, 2, 4), X), ((2, 1, 4, 3, 0), Y)) + seen, queue = {start}, [start] + for index in range(120): + if index == len(queue): + break + p, a = queue[index] + for q, b in generators: + state = (permutation_product(q, p), matrix_product(b, a)) + if state not in seen: + seen.add(state) + queue.append(state) + need(len(queue) <= 60, 'generator identification is inconsistent') + need(len(queue) == 60, 'paired group must have order sixty') + need(len({p for p, _ in queue}) == 60, 'permutation projection not injective') + matrices = tuple(a for _, a in queue) + all_sl2 = {a for a in product(range(4), repeat=4) if determinant(a) == 1} + need(set(matrices) == all_sl2, 'matrix projection must equal SL2(F4)') + return tuple(queue) + + +def cnot_action(value, word): + for control, target in word: + value ^= ((value >> control) & 1) << target + return value + + +def cycles_of(permutation): + need(sorted(permutation) == list(range(len(permutation))), 'not a permutation') + seen, cycles = set(), [] + for start in range(len(permutation)): + if start in seen: + continue + cycle, value = [], start + for _ in range(len(permutation)): + if value in seen: + break + seen.add(value) + cycle.append(value) + value = permutation[value] + need(value == start, 'cycle did not close') + cycles.append(tuple(cycle)) + return tuple(cycles) + + +def swap_word(permutation): + swaps = tuple((cycle[0], value) for cycle in cycles_of(permutation) + for value in cycle[1:]) + # Symbolic rows carry every possible dirty data input, without a clean bit. + rows = [1 << j for j in range(len(permutation))] + for a, b in swaps: + rows[a] ^= rows[b] + rows[b] ^= rows[a] + rows[a] ^= rows[b] + need(all(rows[permutation[j]] == 1 << j for j in range(len(rows))), + 'XOR-swap program has the wrong complete endpoint') + return len(swaps) + + +def orbit_inventory(matrices, copies): + remaining = set(range(1 << (4*copies))) + lengths = [] + for start in range(1 << (4*copies)): + if start not in remaining: + continue + orbit = {address_action(a, start, copies) for a in matrices} + need(orbit <= remaining, 'orbits overlap without coinciding') + remaining.difference_update(orbit) + lengths.append(len(orbit)) + need(not remaining, 'orbit inventory incomplete') + return dict(sorted(Counter(lengths).items())) + + +def norm_column(matrices, start, copies): + value = 0 + for a in matrices: + value ^= 1 << address_action(a, start, copies) + return value + + +def semantic_controls(matrices): + count = 0 + # Every literal address CNOT matters, on both copies. + for a, word in ((X, X_WORD), (Y, Y_WORD)): + for omitted in range(len(word)): + mutant = word[:omitted] + word[omitted+1:] + need(any(cnot_action(z, mutant) != vector_action(a, z) + for z in range(16)), 'omitted CNOT escaped') + count += 1 + need(matrix_product(X, Y) != matrix_product(Y, X), 'labels commute') + count += 1 + # A group-faithful single copy still kills the nonzero formal norm element. + need(all(norm_column(matrices, z, 1) == 0 for z in range(16)), + 'single-copy obstruction was lost') + count += 1 + need(norm_column(matrices, 65, 2).bit_count() == 60, + 'regular orbit must detect the formal norm element') + count += 1 + return count + + +def build_result(): + paired = identified_group() + matrices = tuple(a for _, a in paired) + # All multiplication pairs check the explicit isomorphism, not a word census. + correspondence = dict(paired) + for p, a in paired: + for q, b in paired: + need(correspondence[permutation_product(p, q)] == matrix_product(a, b), + 'generator correspondence fails multiplication') + need(len({tuple(vector_action(a, z) for z in range(16)) for a in matrices}) + == 60, 'single-copy group action not faithful') + # Identity matrix has columns (1,0) and (0,1), encoded as 1+16*4=65. + images = tuple(address_action(a, 65, 2) for a in matrices) + need(len(set(images)) == 60, 'identity orbit must be regular') + need({tuple((z >> (2*j)) & 3 for j in (0, 2, 1, 3)) for z in images} + == set(matrices), 'regular orbit must be the determinant-one matrices') + invoices = {} + for name, a, word in (('x', X, X_WORD), ('y', Y, Y_WORD)): + need(all(cnot_action(z, word) == vector_action(a, z) for z in range(16)), + 'four-bit address circuit incorrect') + doubled = word + tuple((c+4, t+4) for c, t in word) + permutation = tuple(address_action(a, z, 2) for z in range(256)) + need(all(cnot_action(z, doubled) == permutation[z] for z in range(256)), + 'eight-bit address circuit incorrect') + swaps = swap_word(permutation) + invoices[name] = {'address_cnots': len(doubled), 'data_swaps': swaps, + 'data_xors': 3*swaps, + 'cycle_lengths': dict(sorted(Counter(map(len, cycles_of(permutation))).items()))} + return {'group_order': 60, 'multiplication_pairs': 3600, + 'single_copy_orbits': orbit_inventory(matrices, 1), + 'double_copy_orbits': orbit_inventory(matrices, 2), + 'regular_orbit_seed': 65, 'faithful_formal_basis_columns': len(images), + 'invoices': invoices, 'semantic_controls': semantic_controls(matrices)} + + +def source_hashes(): + return {name: sha256((HERE/name).read_bytes()).hexdigest() for name in + ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py', 'OVERLAP.json')} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='explicitly regenerate RESULT.json') + args = parser.parse_args() + receipt = {'result': build_result(), 'source_sha256': source_hashes()} + encoded = json.dumps(receipt, indent=2, sort_keys=True) + '\n' + if args.write: + (HERE/'RESULT.json').write_text(encoded) + else: + need((HERE/'RESULT.json').read_text() == encoded, 'receipt mismatch; do not overwrite during replay') + print('PASS_A5_EIGHT_BIT_CARRIER ' + json.dumps(receipt['result'], sort_keys=True)) + + +if __name__ == '__main__': + main()