From 99ed6d2fc13101cb5ec0d3b1cdc826b75bc27fc7 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 13:31:15 +0100 Subject: [PATCH] feat(research): prove exact order-21 normal-subgroup tariff --- research/order21-normal-tariff/PROOF.md | 141 +++++++++ research/order21-normal-tariff/README.md | 140 +++++++++ research/order21-normal-tariff/SOURCES.json | 24 ++ research/order21-normal-tariff/TASK.json | 77 +++++ research/order21-normal-tariff/VERIFY.json | 34 +++ research/order21-normal-tariff/verify.py | 303 ++++++++++++++++++++ 6 files changed, 719 insertions(+) create mode 100644 research/order21-normal-tariff/PROOF.md create mode 100644 research/order21-normal-tariff/README.md create mode 100644 research/order21-normal-tariff/SOURCES.json create mode 100644 research/order21-normal-tariff/TASK.json create mode 100644 research/order21-normal-tariff/VERIFY.json create mode 100644 research/order21-normal-tariff/verify.py diff --git a/research/order21-normal-tariff/PROOF.md b/research/order21-normal-tariff/PROOF.md new file mode 100644 index 0000000000..7826687018 --- /dev/null +++ b/research/order21-normal-tariff/PROOF.md @@ -0,0 +1,141 @@ +# Exact normal-subgroup tariff in the order-21 algebra + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and model + +Let G be the group C7 semidirect C3 with elements a^i b^j, where +0 <= i < 7, 0 <= j < 3, and b a b^-1 = a^2. Multiplication is + +```text +(i,j)(k,l) = (i + 2^j k mod 7, j+l mod 3). +``` + +Work in the full formal algebra Mat_r(F2[G]). There are w active roles, +with 1 <= w <= r, and arbitrary exponents 1 <= e_t <= 6. The required +operator is + +```text +T = diag([a^e_1], ..., [a^e_w], 1, ..., 1). +``` + +Every role has arbitrary input. The last r-w roles must be restored as +operators. A paid call is D_N(g) = I + ([g]+[1])N for any g != 1 in G +and any rank-one binary idempotent N in Mat_r(F2). Each call costs one. +Arbitrary GL_r(F2) scalar maps may be interleaved for free. No other +address maps, clean workspace, COPY or ERASE are free. + +**Theorem.** The exact minimum number of paid calls is w, for every +finite r and every stated exponent list. In particular, +diag([a],[a^2],[a^4],[a],1,...,1) requires exactly four calls, regardless +of the number of restored dirty roles. + +More precisely, if a word uses c7 paid labels in the normal subgroup +C7 minus identity, and c3 paid labels outside C7, then + +```text +3 c7 + 2 c3 >= 3w. +``` + +Consequently an optimal w-call word uses only normal-subgroup labels. +This does not claim an exact optimum subject to a prescribed positive c3. + +## Representation and rank budget + +The polynomial x^3+x+1 has neither zero nor one as a root in F2. +A reducible cubic over a field has a linear factor, so this polynomial +is irreducible. Let F8=F2[alpha] with alpha^3=alpha+1. Its multiplicative +group has order seven. Since alpha is neither zero nor one, its order +is seven. + +For g=a^i b^j, define the binary linear map on F8 + +```text +rho(g)(z) = alpha^i z^(2^j). +``` + +Frobenius is F2-linear and its third power is identity. Composing the +displayed maps gives the group multiplication above, so rho extends +linearly to an algebra homomorphism F2[G] -> Mat_3(F2). In the basis +1,alpha,alpha^2 its two generators, encoded as binary integer rows, are + +```text +rho(a) = (4,5,2), rho(b) = (1,4,6). +``` + +For 1 <= i <= 6, rho(a^i)+I is multiplication by the nonzero field +element alpha^i+1, hence has rank three. + +For j=1 or 2, a nonzero fixed point of rho(a^i b^j) satisfies +z^(2^j-1)=alpha^-i. The exponents 2^j-1 are respectively one and three, +both coprime to seven. Raising to either power therefore permutes F8's +nonzero elements. There is exactly one nonzero fixed point, together +with zero. Its kernel as a binary linear map has dimension one, so +rank(rho(a^i b^j)+I)=2. This proves all represented ranks without a census. + +Apply rho to every entry of an r-role operator, viewing the result as +an ordinary 3r by 3r binary matrix. One paid call has difference from +identity + +```text +N tensor (rho(g)+I). +``` + +The rank of a tensor product over a field is the product of the ranks. +Thus each normal-subgroup call contributes rank three and every other +paid label contributes rank two. Meanwhile rank(rho(T)+I)=3w, since +its active diagonal blocks are invertible and its dirty blocks are zero. + +For any equally sized matrices A and B, + +```text +AB-I = (A-I)B + (B-I), +rank(AB-I) <= rank(A-I) + rank(B-I). +``` + +Induction over any finite paid word proves the stated rank budget. +It is a necessary condition for formal equality. Faithfulness of the +algebra homomorphism is unnecessary, and no equality in the represented +algebra is used to certify a formal endpoint. + +## Free scalar maps and arbitrary dirty workspace + +A scalar map S satisfies S D_N(g) = D_(S N S^-1)(g) S. Moving each free +scalar map to the right therefore conjugates the paid binary idempotents +and leaves them inside the declared alphabet. Augmentation [g] -> 1 +sends every paid factor and T to identity. Hence the remaining product +of free scalar maps must be identity. The normalized word has the same +paid labels and number of calls, so the rank budget applies unchanged. + +The proof holds for every finite r. Identity-target dirty roles add +zero to the represented target rank. No compression, clean-input +assumption or bound on the number of workspace roles is used. + +Since 3 c7+2 c3 <= 3(c7+c3), the rank budget forces at least w calls. +If exactly w calls occur, any c3>0 would make the rank budget fail. + +## Attainment in the full formal algebra + +For each active role t, take N=E_tt and g=a^e_t. This call acts by +[a^e_t] on that role and identity on every other role. The product of +these w coordinate calls is exactly T coefficient by coefficient in +F2[G]. It uses no additional roles and restores every dirty role. +This establishes the upper bound in the full formal algebra and +completes the proof. + +## Sources and limits + +Cinna Davis's PR2011 fixes this group, paid alphabet and conjugacy-orbit +endpoint, and explicitly leaves four outputs open. The new statement +settles that question and removes both the fixed role count and the +restriction against free scalar maps. The original three-role finite +census is not rerun or claimed as new. Cinna Davis's PR3893 supplies an +S3 example of the classical representation-rank telescoping method. +The present contribution is its fixed-point-free F8 application and +uniform exact order-21 tariff. The F8 and rank facts are elementary +linear algebra, not new general methods. + +Mixed order-three target profiles, nonuniform tariffs, native realization, +physical movement, precision, stock, recursive costs and the complete +multiplication theorem are outside this proof. The selected frontier +is unchanged. No proof-kernel or independent human review is claimed. diff --git a/research/order21-normal-tariff/README.md b/research/order21-normal-tariff/README.md new file mode 100644 index 0000000000..eaa7bb551e --- /dev/null +++ b/research/order21-normal-tariff/README.md @@ -0,0 +1,140 @@ +# Exact order-21 normal-subgroup call tariff + +Scoped algebraic proof with exact finite corroboration. No new kappa. +This contribution was produced by Nick Petalas. Apache-2.0. + +In the full formal algebra F2[C7 semidirect C3], any w nonidentity +normal-C7 outputs require exactly w paid rank-one idempotent calls. +This holds for any finite number of arbitrary restored dirty registers +and with arbitrary free binary scalar mixing. In particular, + +```text +diag([a], [a^2], [a^4], [a], 1, ..., 1) +``` + +costs exactly four calls. This settles the four-register question left +by Cinna Davis's [PR2011](https://github.com/CrocSwap/integer-mult-bounds/pull/2011). +Its three-register census is a cited predecessor and is not replayed. + +[PROOF.md](PROOF.md) defines the complete model. Multiplication and +Frobenius on F8 give a three-dimensional binary representation. Every +nonidentity normal-C7 target contributes rank three to the endpoint +minus identity. A normal-C7 paid label contributes rank three, while +an outside label contributes rank two. Rank telescoping therefore gives + +```text +3 * normal_calls + 2 * outside_calls >= 3 * target_count. +``` + +Coordinate calls attain the bound in the full formal algebra. Every +optimal word uses only normal-C7 labels. The lower bound is uniform +in target count, word length and restored workspace size. The finite +checks corroborate the proof; they do not replace its induction. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/order21-normal-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/order21-normal-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/order21-normal-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/order21-normal-tariff --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. +The verifier prints `PASS_ORDER21_NORMAL_TARIFF` in a generated JSON +receipt bound to the SHA256 of all six package files. It writes no files. +There is no handwritten receipt. Local checks used CPython 3.12.15 on +macOS arm64. [VERIFY.json](VERIFY.json) registers the normal and optimized +warning-strict runs, each with a 60-second limit. + +The verifier performs these exact checks: + +- All 441 products in the new F8 representation, with represented + difference ranks zero, three and two on identity, the six nonidentity + normal labels and the fourteen outside labels respectively. +- All 12,320 paid factors on four and five roles. These are all 120 and + 496 binary rank-one idempotents respectively, at all twenty paid labels. + Every represented difference has the proved rank. +- All 1,296 four-target exponent lists from {1,...,6}, each with one + arbitrary dirty role, plus six larger witnesses at widths 5, 8 and 12, + each with zero or two dirty roles. All 1,302 products equal their + required endpoints coefficient by coefficient in the full formal algebra. +- One conjugated four-target witness mixes the dirty input through free + scalar maps and restores the full operator. A separate 105-dimensional + faithful regular-action execution agrees with the formal result. +- Ten controls reject four call omissions, either missing free scalar map, + a changed dirty-role operator, a wrong target exponent, reversed + Frobenius and an incorrect outside-label rank charge. All checks remain + active under optimized Python. + +The complete four-target formal stream is hashed in the generated receipt. +The predecessor's pair census and certificate numbers are not recomputed. +No selected operator replay, Lean or Docker run is needed for this theorem, +and none was run. + +## Scope and provenance + +The paid alphabet contains every nonidentity group label and every binary +rank-one idempotent. Its unit call price does not account for native +realization, routing, frames, precision, stock or recursive child costs. +Those physical obligations remain unknown. Mixed order-three target +profiles and nonuniform prices are outside the exact tariff. No supplier +admission, complete multiplication theorem or selected-frontier change +follows. Independent human and formal proof-kernel review are unclaimed. + +[SOURCES.json](SOURCES.json) binds historical provenance at canonical main +`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority revision 7. +The selected-record and task-card pins are historical. The verifier uses +no predecessor files or external libraries. [TASK.json](TASK.json) +records the scope change from bit-new-register-model to this formal +obstruction. The card's current generic baseline returned +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. The first scientific fixture was +the four-output endpoint above with one restored dirty role. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145540) +records the question. Live open PRs, recent handoffs, merged PR searches +and main README terms were checked. The overlap helper covered 315 open +PRs and 4,392 Discussion records with complete remote pagination. Its +sparse local search covered only 170 of 6,996 HEAD notes; targeted main +searches supplement it. These checks do not establish exhaustive novelty. + +Build the Lever led to the rerunnable formal and represented checks. +Prove It Works led to full dirty-operator execution and omission controls. +Power of Ten kept the replay bounded and read-only. Every function is +below 60 lines, and no recursion, dynamic evaluation or subprocess is used. +Matrices have at most 128 rows, formal words at most twelve calls and +formal executions at most fourteen roles. The faithful regular replay has +five roles and 105 rows. Loops have bounds from these fixed domains. +Python allocation is a managed-runtime deviation from static allocation; +all live collections are bounded by these limits, and input files are +limited to one MiB each. Warning-strict normal and optimized execution +provide diagnostics. No separate static analyzer is installed. + +## Open next questions + +1. What is the exact tariff for mixed normal-C7 and outside order-three + target profiles? Begin with one target of each type and combine this + represented-rank budget with the quotient C3 character. The current + rank budget does not by itself prove that their separate calls are + optimal. A full formal attainment or stronger lower bound is needed. +2. Can a literal native producer and consumer implement these group + labels at a useful complete cost? First fix their address action, + ownership, routing and restoration contracts, then charge the whole + boundary. No physical cost model is supplied here. + +The structured questions are in [TASK.json](TASK.json). + +## Credit + +Cinna Davis's PR2011 supplies the group, formal alphabet, three-output +problem and explicit four-output question. Its retained register-model +lineage includes eumemic's PR288 and the original bit-model work. +Cinna Davis's [PR3893](https://github.com/CrocSwap/integer-mult-bounds/pull/3893) +provides the S3 example of representation-rank telescoping. Finite-field +multiplication, Frobenius and the rank inequality are classical. The new +claim is their uniform exact tariff for normal-subgroup targets in the +order-21 model, including arbitrary restored workspace and free scalar +mixing. Every predecessor retains its attribution; no predecessor file +or credit line is changed. diff --git a/research/order21-normal-tariff/SOURCES.json b/research/order21-normal-tariff/SOURCES.json new file mode 100644 index 0000000000..e42d3d47d0 --- /dev/null +++ b/research/order21-normal-tariff/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "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/bit-semidir21-orbit-seed8f89/README.md", + "usage": "provenance", + "git_blob": "13e399921e5dd556a7ce8645362ffb5d550b5e75", + "sha256": "534422d3f152b0f1e4a8357056036d1629b0aee75e58301c7436f5b723260eb0" + } + ] +} diff --git a/research/order21-normal-tariff/TASK.json b/research/order21-normal-tariff/TASK.json new file mode 100644 index 0000000000..9440cd6d16 --- /dev/null +++ b/research/order21-normal-tariff/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "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": "changed", + "actual_scope": "Prove exact cost w for any w nonidentity normal-C7 targets in F2[C7 semidirect C3], for every finite restored dirty workspace and free binary scalar mixing.", + "scope_change_reason": "Take Cinna Davis PR2011's explicitly open four-register question, using a representation-rank obstruction rather than a new native supplier or a replay of the three-register census.", + "bottleneck_link": "This formal side result closes the normal-subgroup multi-output sharing route in the stated alphabet. Native realization and a fully charged recursive invoice remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact uniform tariff; do not search mixed target profiles or construct a native supplier.", + "outcome": "completed", + "evidence": "Written F8 representation and rank-telescoping proof. Exact verifier checks 441 representation products, 12320 paid factors, 1302 full formal coordinate endpoints, one dirty-mixed faithful regular endpoint and ten rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact tariff for mixed normal-C7 and outside order-three target profiles?", + "why_it_matters": "The current theorem excludes sharing only for all-normal targets.", + "first_step": "Study one target of each type using the represented-rank budget and quotient-C3 character, with a full formal endpoint.", + "blocked_by": "A stronger lower bound or a cheaper full formal word is missing." + }, + { + "question": "Can a literal native caller implement these labels at a useful complete cost?", + "why_it_matters": "Only a physical implementation could affect the recursive supplier bill.", + "first_step": "Specify the address action, ownership, routing and restoration of one producer/consumer pair and charge every operation.", + "blocked_by": "No native boundary contract or complete cost model is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145540", + "claim_type": "scoped algebraic proof with exact finite corroboration", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + } +} diff --git a/research/order21-normal-tariff/VERIFY.json b/research/order21-normal-tariff/VERIFY.json new file mode 100644 index 0000000000..f8459b0a6a --- /dev/null +++ b/research/order21-normal-tariff/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "F8 representation rank proof corroboration, all four/five-role paid factors, full formal attaining endpoints, dirty mixing, regular action and ten controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat the full proof corroboration and rejection controls with Python assertions disabled." + } + ] +} diff --git a/research/order21-normal-tariff/verify.py b/research/order21-normal-tariff/verify.py new file mode 100644 index 0000000000..8583bc544c --- /dev/null +++ b/research/order21-normal-tariff/verify.py @@ -0,0 +1,303 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the normal-C7 call tariff; standard library only.""" + +import hashlib +import itertools +import json +from pathlib import Path + +MAX_DIM = 128 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + require(1 <= n <= MAX_DIM, 'matrix dimension outside fixed replay limit') + return tuple(1 << i for i in range(n)) + + +def xor(a, b): + require(len(a) == len(b), 'matrix sum dimensions') + return tuple(x ^ y for x, y in zip(a, b)) + + +def multiply(a, b): + n = len(a) + require(1 <= n <= MAX_DIM and len(b) == n, 'matrix product dimensions') + require(all(0 <= row < 1 << n for row in a + b), 'matrix row range') + out = [] + for row in a: + value = 0 + for j in range(n): + if row >> j & 1: + value ^= b[j] + out.append(value) + return tuple(out) + + +def rank(rows): + require(1 <= len(rows) <= MAX_DIM, 'rank dimension') + pivots = [0] * MAX_DIM + answer = 0 + for row in rows: + require(0 <= row < 1 << MAX_DIM, 'rank row range') + value = row + for j in range(MAX_DIM - 1, -1, -1): + if value >> j & 1: + if pivots[j]: + value ^= pivots[j] + else: + pivots[j] = value + answer += 1 + break + return answer + + +def outer(x, y, n): + require(0 < x < 1 << n and 0 < y < 1 << n, 'outer vector range') + return tuple(y if x >> i & 1 else 0 for i in range(n)) + + +def kron(a, b): + n, d = len(a), len(b) + require(1 <= n * d <= MAX_DIM, 'tensor dimension') + return tuple(sum((b[u] << (j * d)) for j in range(n) if a[i] >> j & 1) + for i in range(n) for u in range(d)) + + +def field_multiply(x, y): + require(0 <= x < 8 and 0 <= y < 8, 'F8 element range') + result = 0 + for _ in range(3): + if y & 1: + result ^= x + y >>= 1 + x <<= 1 + if x & 8: + x ^= 0b1011 + return result + + +def group_multiply(g, h): + require(0 <= g < 21 and 0 <= h < 21, 'group label range') + i, j = g % 7, g // 7 + k, ell = h % 7, h // 7 + return (i + (1 << j) * k) % 7 + 7 * ((j + ell) % 3) + + +def representation(g): + i, j = g % 7, g // 7 + coefficient = 1 + for _ in range(i): + coefficient = field_multiply(coefficient, 2) + columns = [] + for bit in range(3): + value = 1 << bit + for _ in range(j): + value = field_multiply(value, value) + columns.append(field_multiply(coefficient, value)) + return tuple(sum(((columns[c] >> r) & 1) << c for c in range(3)) + for r in range(3)) + + +def check_group(): + matrices = tuple(representation(g) for g in range(21)) + a, b = (4, 5, 2), (1, 4, 6) + require(matrices[1] == a and matrices[7] == b, 'generator matrices') + require(len(set(matrices)) == 21, 'representation is faithful') + for g, h in itertools.product(range(21), repeat=2): + require(multiply(matrices[g], matrices[h]) == matrices[group_multiply(g, h)], + 'representation multiplication') + deltas = tuple(rank(xor(m, identity(3))) for m in matrices) + require(deltas == (0,) + (3,) * 6 + (2,) * 14, 'represented delta ranks') + return matrices, deltas + + +def check_factors(matrices, deltas): + count = 0 + for n in (4, 5): + for x, y in itertools.product(range(1, 1 << n), repeat=2): + if (x & y).bit_count() % 2 == 0: + continue + coupling = outer(x, y, n) + require(multiply(coupling, coupling) == coupling, 'idempotent') + require(rank(coupling) == 1, 'scalar coupling rank') + for g in range(1, 21): + delta = kron(coupling, xor(matrices[g], identity(3))) + require(rank(delta) == deltas[g], 'paid represented rank') + count += 1 + return count + + +def zero_coefficients(n): + require(1 <= n <= 14, 'formal role limit') + return [(0,) * n for _ in range(21)] + + +def endpoint(labels): + result = zero_coefficients(len(labels)) + for i, g in enumerate(labels): + require(0 <= g < 21, 'endpoint group label') + rows = list(result[g]) + rows[i] ^= 1 << i + result[g] = tuple(rows) + return tuple(result) + + +def execute(word, n, left=None, right=None): + require(len(word) <= 12, 'formal call limit') + result = zero_coefficients(n) + result[0] = identity(n) if left is None else left + for g, coupling in word: + require(1 <= g < 21 and len(coupling) == n, 'paid call dimensions') + require(rank(coupling) == 1, 'paid scalar rank') + require(multiply(coupling, coupling) == coupling, 'paid idempotence') + updated = list(result) + for h in range(21): + delta = multiply(result[h], coupling) + updated[h] = xor(updated[h], delta) + target = group_multiply(h, g) + updated[target] = xor(updated[target], delta) + result = updated + if right is not None: + result = [multiply(coefficient, right) for coefficient in result] + return tuple(result) + + +def coordinate_word(labels): + n = len(labels) + return tuple((g, outer(1 << i, 1 << i, n)) + for i, g in enumerate(labels) if g) + + +def scalar_mix(n): + shear_list = [] + for i in range(n - 1): + for row, column in ((i, n - 1), (n - 1, i)): + shear = list(identity(n)) + shear[row] ^= 1 << column + shear_list.append(tuple(shear)) + forward = reverse = identity(n) + for shear in shear_list: + forward = multiply(forward, shear) + for shear in reversed(shear_list): + reverse = multiply(reverse, shear) + require(multiply(forward, reverse) == identity(n), 'inverse scalar mixes') + return forward, reverse + + +def regular_operator(coefficients): + n = len(coefficients[0]) + require(n <= 5, 'faithful regular replay role limit') + out = [0] * (21 * n) + for g, scalar in enumerate(coefficients): + for i, row in enumerate(scalar): + for j in range(n): + if row >> j & 1: + for h in range(21): + out[21 * i + group_multiply(g, h)] ^= 1 << (21 * j + h) + return tuple(out) + + +def check_witnesses(): + count = 0 + digest = hashlib.sha256() + for exponents in itertools.product(range(1, 7), repeat=4): + labels = exponents + (0,) + actual = execute(coordinate_word(labels), len(labels)) + require(actual == endpoint(labels), 'four-target full formal endpoint') + digest.update(json.dumps(actual, separators=(',', ':')).encode()) + count += 1 + for width, dirty in itertools.product((5, 8, 12), (0, 2)): + labels = tuple(1 + i % 6 for i in range(width)) + (0,) * dirty + require(execute(coordinate_word(labels), len(labels)) == endpoint(labels), + 'additional full formal endpoint') + count += 1 + return count, digest.hexdigest() + + +def check_mixing(): + labels = (1, 2, 4, 1, 0) + n = len(labels) + forward, reverse = scalar_mix(n) + word = tuple((g, multiply(multiply(forward, p), reverse)) + for g, p in coordinate_word(labels)) + actual = execute(word, n, reverse, forward) + require(actual == endpoint(labels), 'dirty-mixed full formal endpoint') + literal = kron(reverse, identity(21)) + for g, coupling in word: + permutation = tuple(1 << group_multiply(g, h) for h in range(21)) + # The row encoding of left multiplication is the transpose of this column list. + action = tuple(sum(((permutation[c] >> r) & 1) << c for c in range(21)) + for r in range(21)) + call = xor(identity(21 * n), kron(coupling, xor(action, identity(21)))) + literal = multiply(literal, call) + literal = multiply(literal, kron(forward, identity(21))) + require(literal == regular_operator(actual), 'faithful full operator comparison') + return labels, word, forward, reverse + + +def reject_check(predicate, message): + try: + require(predicate, message) + except ValueError: + return message + raise ValueError('control was not rejected: ' + message) + + +def check_controls(labels, word, forward, reverse, matrices): + controls = [] + n = len(labels) + target = endpoint(labels) + for i in range(4): + changed = word[:i] + word[i + 1:] + controls.append(reject_check(execute(changed, n, reverse, forward) == target, + 'omitted call ' + str(i))) + controls.append(reject_check(execute(word, n, None, forward) == target, + 'omitted entry scalar map')) + controls.append(reject_check(execute(word, n, reverse, None) == target, + 'omitted exit scalar map')) + controls.append(reject_check(endpoint(labels[:-1] + (1,)) == target, + 'unrestored dirty operator')) + controls.append(reject_check(endpoint((2,) + labels[1:]) == target, + 'wrong target exponent')) + bad_b = multiply(matrices[7], matrices[7]) + controls.append(reject_check(multiply(bad_b, matrices[1]) == + multiply(matrices[2], bad_b), 'reversed Frobenius')) + controls.append(reject_check(rank(xor(matrices[7], identity(3))) == 3, + 'order-three call charged rank three')) + return controls + + +def main(): + matrices, deltas = check_group() + factors = check_factors(matrices, deltas) + witnesses, digest = check_witnesses() + labels, word, forward, reverse = check_mixing() + controls = check_controls(labels, word, forward, reverse, matrices) + represented_target = kron(identity(5), (0, 0, 0)) + for i, g in enumerate(labels): + projector = outer(1 << i, 1 << i, 5) + represented_target = xor(represented_target, + kron(projector, xor(matrices[g], identity(3)))) + require(rank(represented_target) == 12, 'four-target represented rank') + package = Path(__file__).resolve().parent + hashes = {} + for name in ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', + 'VERIFY.json', 'verify.py'): + content = (package / name).read_bytes() + require(len(content) <= 1 << 20, 'package file size limit') + hashes[name] = hashlib.sha256(content).hexdigest() + print(json.dumps({'status': 'PASS_ORDER21_NORMAL_TARIFF', + 'group_products': 441, 'paid_factors': factors, + 'formal_witnesses': witnesses, 'mixed_regular_witnesses': 1, + 'four_target_delta_rank': rank(represented_target), + 'controls': controls, 'four_target_stream_sha256': digest, + 'source_sha256': hashes}, sort_keys=True)) + + +if __name__ == '__main__': + main()