From 701cb14b7c461253d7ac8243d0722996918bc6c6 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 21:24:38 +0100 Subject: [PATCH] feat(research): prove sharp binary three-role product cost --- .../right-vector-three-role-products/PROOF.md | 165 +++++++++++ .../README.md | 91 ++++++ .../SOURCES.json | 30 ++ .../TASK.json | 74 +++++ .../VERIFY.json | 35 +++ .../verify.py | 271 ++++++++++++++++++ 6 files changed, 666 insertions(+) create mode 100644 research/right-vector-three-role-products/PROOF.md create mode 100644 research/right-vector-three-role-products/README.md create mode 100644 research/right-vector-three-role-products/SOURCES.json create mode 100644 research/right-vector-three-role-products/TASK.json create mode 100644 research/right-vector-three-role-products/VERIFY.json create mode 100644 research/right-vector-three-role-products/verify.py diff --git a/research/right-vector-three-role-products/PROOF.md b/research/right-vector-three-role-products/PROOF.md new file mode 100644 index 0000000000..d134559801 --- /dev/null +++ b/research/right-vector-three-role-products/PROOF.md @@ -0,0 +1,165 @@ +# A sharp five-factor bound for binary three-role products + +## Model and claim type + +Put K=F2 and R=K^k for a positive integer k. A paid factor on three roles is + +```text +P(u,b) = I + u b^T, u in R^3, b in K^3. +``` + +The embedding K into R is diagonal. Thus b is common to all k components, +whereas u may have a different binary three-vector in each component. Free +maps are common matrices in GL3(K), allowed anywhere. No extra roles are +allowed. This is the formal alphabet of Wentao Li #4099 following #2513, +with the free-map normal form retained in Nick Petalas #4243. ToikY #4334 +proved the sharp two-role field-product result and its common-direction +upper construction. + +This package supplies a complete finite certificate and a scoped algebraic +consequence of that certificate: + +1. Every invertible three-role target over F2^k costs at most five paid factors. +2. The target U over F2^168 whose components list GL3(F2) costs exactly five. + Therefore the uniform bound is sharp, also for every k>=168 by padding. +3. For that U the column lower bound delta(U) is exactly three. Its gap from + the exact cost is two. + +No minimum component count for cost five is asserted. No all-field, +extra-role, local-ring or native-supplier statement is asserted. + +## 1. Reduction to common direction words + +Conjugation by a free matrix S preserves the alphabet: + +```text +S P(u,b) S^-1 = P(Su, S^-T b). +``` + +Move all free maps to the right. A word of length L is a product of L paid +factors followed by one common free S. For chronological direction sequence +b1,...,bL, define the paid product as P_L ... P_1, with P_1 applied first. +A zero direction gives the identity. It can be replaced by b=e1,u=0. +Words shorter than four can likewise be padded to four. + +If a component of the target is invertible, every square factor in that +component must be invertible, by rank submultiplicativity. In K, write a +component paid factor as I+a b^T. It is invertible exactly when b.a=0. +Indeed when b.a=0 its square is I. When b.a=1, a is nonzero and the factor +kills a. For each nonzero b there are exactly four eligible a, including +zero. These are all possibilities, not a restriction to coordinate vectors +or to some chosen gate library. + +There are seven nonzero directions. For a fixed ordered word of length +four there are exactly 4^4 eligible parameter tuples. Its reachable set is +computed from {I} by left multiplication by each of the four eligible +factors at each step. There are exactly 7^4=2401 ordered direction words. + +## 2. The complete finite certificate + +`verify.py` encodes a binary matrix by its three rows, each a three-bit +integer, least significant row first. Thus I has encoding 273. It builds +GL3(F2) by rank-three elimination on all 512 matrices. Independently, it +builds every binary linear bijection on the eight vectors by enumerating +all ordered triples of nonzero basis images and retaining the bijections. +Both groups contain the same 168 matrices. + +The matrix calculation propagates reachable sets through all four steps. +The independent calculation composes permutations of the eight vectors: +first all 16 parameter choices for each two-direction word, then every +pair of two-step results. It explicitly enumerates all +7^4 * 4^4 = 614656 direction/parameter tuples. The two implementations agree +on the complete 168-bit endpoint mask for every one of the 2401 direction +words, rather than merely on cardinalities. + +The resulting complete histogram is: + +| Reachable group elements | 4 | 16 | 24 | 64 | 96 | 144 | +|---|---:|---:|---:|---:|---:|---:| +| Ordered four-direction words | 7 | 126 | 420 | 504 | 672 | 672 | + +In particular no four-direction word reaches all 168 matrices. + +For the fixed chronological sequence + +```text +b1,b2,b3,b4,b5 = e1,e2,e3,e1,e2, +``` + +the matrix calculation constructs one literal five-factor witness for each +of the 168 matrices. The action calculation independently enumerates all +4^5=1024 parameter tuples and reaches all 168 endpoints. Every constructed +witness is also evaluated on all eight binary inputs, giving 1344 complete +component/input checks. This proves the upper-bound certificate. The +verifier hashes the complete four-word endpoint table and the complete +five-factor witness table. It also emits a generated receipt bound to the +six package files and two pinned predecessor inputs. + +The computations are exact and use no randomness, numerical tolerance, +symmetry reduction or pruning. All validations remain active under -O. +They are executable finite evidence, not formal proof-kernel checking. + +## 3. Sharpness with arbitrary free maps + +For any common S in GL3(F2), the components of U S^-1 again list every +element of GL3(F2), since right translation permutes the group. If U had a +word with at most four paid factors and any free maps, Section 1 would give +a common four-direction word for U S^-1 after identity padding. Its +components would then have to lie in a reachable set of at most 144 +elements. They contain all 168, a contradiction. + +For any invertible M over F2^k, each component M_i has the Section 2 witness +with the same five directions. At step j assemble its k left coefficients +into u_j in R^3. Componentwise multiplication now gives M in five paid +factors. Arbitrary componentwise left coefficients are permitted by the +stated model; componentwise free maps or right directions are never used. +This proves the quantified upper bound and cost(U)=5. Appending arbitrary +invertible components to U preserves its lower bound by projection and its +five-factor upper bound by the same construction. + +## 4. The column-bound gap + +The predecessor's general column bound is + +```text +delta(M) = min over T in GL3(F2) of dim_F2 ((M T - I) F2^3) <= cost(M). +``` + +For U and any T, its translated components range over every group element. +If a nonzero v were in the common kernel, every A in GL3(F2) would satisfy +A v=v. But GL3(F2) sends a given nonzero v to every nonzero vector. This is +impossible. Hence that map from F2^3 is injective and delta(U)=3. The +verifier separately stacks all component rows and checks rank three for +every one of the 168 free choices. It also checks all 4704 labelled +factor/free-map conjugations, including the seven identity labels. + +Thus the column bound does not give an exact cost, or a uniform +three-factor bound, even for invertible targets over a product of copies +of the base field on only three roles. This is compatible with the exact +local-algebra result in #4787: F2^168 is not local. + +## Attribution and relation to classical work + +This contribution was produced by Nick Petalas. The new contribution is +the complete common-direction certificate and its sharp cost consequence +in the repository's alphabet. ToikY #4334 supplied the field-product +question, the shared-direction viewpoint and the two-role predecessor. +Nick Petalas #4243/#4265/#4276 and #4749 supplied the retained normal form, +column bound applications, general-target question and semilocal context. +The alphabet and original column expansion are Wentao Li #4099 following +#2513. Their packages are preserved unchanged. + +Short linear register-update programs have a classical literature. See +Gadouleau and Riis, [Memoryless computation: new results, constructions, +and extensions, Section 3.3](https://arxiv.org/html/1111.6026#S3.SS3), and +Cameron, Fairbairn and Gadouleau, +[Computing in matrix groups without memory](https://arxiv.org/abs/1310.6009). +The general idea of short update programs and the generic 2n-1 upper-bound +phenomenon are not claimed as original here. Our finite lower certificate +ranges over every common binary covector sequence, with a common free +GL3 map absorbed at the end. It concerns simultaneous product components. + +Native preparation, access, reversible restoration, precision, stock, +physical implementation and a complete recursive invoice remain unknown. +No complete multiplication theorem, supplier admission or new kappa follows. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/right-vector-three-role-products/README.md b/research/right-vector-three-role-products/README.md new file mode 100644 index 0000000000..836cd177da --- /dev/null +++ b/research/right-vector-three-role-products/README.md @@ -0,0 +1,91 @@ +# Exact five-factor cost for binary three-role products + +A complete finite certificate gives a sharp formal-alphabet result. Every +invertible three-role target over F2^k costs at most five paid factors +I+u b^T, where b is a common binary vector and u may vary by component. +The target over F2^168 listing all elements of GL3(F2) costs exactly five, +even with arbitrary free GL3(F2) maps anywhere. Its column lower bound is +only three. No new kappa or native supplier is claimed. + +The chronological upper directions are e1,e2,e3,e1,e2. All 2401 ordered +four-direction words reach at most 144 of the 168 group elements. The +[proof and scope](PROOF.md) explain why this finite census gives the +all-k upper bound and survives arbitrary interleaved free maps. This +extends ToikY's #4334 two-role product-field result. The contribution is +the exact common-direction obstruction and certificate in this model; +classical short register-update programs retain the credit listed there. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-three-role-products/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-three-role-products/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-three-role-products +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-three-role-products --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. +Expected scientific marker: + +```text +PASS_RIGHT_VECTOR_THREE_ROLE_PRODUCTS group=168 words4=2401 max4=144 upper=5 delta=3 controls=7 +``` + +Two algorithms compare every complete four-word endpoint set. The second +enumerates 614656 parameter tuples as permutations of the eight binary +vectors. The fixed upper word has 1024 parameter tuples and reaches all +168 endpoints; its chosen witnesses pass all 1344 component/input cases. +All 168 free right translations and delta cases, 4704 labelled +conjugations and seven rejection controls pass. A generated JSON receipt +binds results and file hashes; nothing is written into the checkout. + +The four-word histogram, indexed by reachable-set size, is +`{4:7,16:126,24:420,64:504,96:672,144:672}`. The verifier derives it afresh +and checks the complete masks with a second implementation. This is a +finite certificate with a scoped algebraic consequence. It is not a search +failure offered as a universal obstruction. + +## Limits and implementation discipline + +The field is F2, there are exactly three roles, and only invertible product +components are covered. The sharp witness uses 168 components; minimal +component count is open. Native preparation, routing, storage, dirty-state +restoration, precision, stock and the full supplier invoice remain unknown. +The selected construction is unchanged. Lean, Docker and a selected cold +replay are outside scope and unrun. Independent human and formal +proof-kernel review are unclaimed. + +The verifier uses bounded loops, explicit exceptions and no recursion. +Its largest direction census has 2401 states, each with at most 168 +endpoints; the action multiplication table has 168^2 entries. CPython +requires dynamic allocation, so fixed allocation is a documented managed +runtime deviation, with collection sizes bounded by those finite domains. +Functions stay under 60 lines. Warning-strict ordinary and optimized +commands are registered. The negative-control dispatcher has seven fixed +call targets; it is the only callback-based test dispatch. File errors +propagate, and all file handles are owned by pathlib's bounded read calls. +No package-wide configuration change is needed for this isolated script. + +## Open next questions + +1. What is the minimum k for which an invertible target over F2^k costs + five? This would replace the deliberately large universal witness. + Start with the complement sets of the already computed four-word masks + and their common right translates. This is a new covering problem; + the present certificate does not settle it. +2. Which changed physical contract realizes one of these shared-direction + factors? Start with a named producer and consumer and account for + coefficient preparation, overwrites and restoration. All such physical + costs are unknown; this formal result does not authorize a supplier + construction campaign. + +## Credit + +This contribution was produced by Nick Petalas. Credit ToikY #4334 for the +product-field question and two-role common-direction construction; +Nick Petalas #4243/#4265/#4276/#4749 for the retained cost framework; and +Wentao Li #4099 following #2513 for the alphabet and column bound. Classical +memoryless-computation work by Gadouleau, Riis, Cameron and Fairbairn is +linked in PROOF.md. Predecessor files and credit are unchanged. Apache-2.0. diff --git a/research/right-vector-three-role-products/SOURCES.json b/research/right-vector-three-role-products/SOURCES.json new file mode 100644 index 0000000000..086ba20b92 --- /dev/null +++ b/research/right-vector-three-role-products/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/right-vector-commutative-products/PROOF.md", + "usage": "input", + "git_blob": "f149515c1684ac16bcb1ef0fd014b98d6f92f5db", + "sha256": "b401a15bc3a11e2040cdde9d99d4a5b8ec7b4f92643eac547f21b7c667fbf408" + }, + { + "path": "research/right-vector-diagonal-free-basis/PROOF.md", + "usage": "input", + "git_blob": "0964deb3438280a08774d3de3f55de58ce6d9389", + "sha256": "e8bd7ab05fab6a929d0bb5303a823ba3d0105271d67af75e5d68b86601093a12" + } + ] +} diff --git a/research/right-vector-three-role-products/TASK.json b/research/right-vector-three-role-products/TASK.json new file mode 100644 index 0000000000..5b9c4c7f12 --- /dev/null +++ b/research/right-vector-three-role-products/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "The exact universal paid right-vector cost for invertible three-role targets over F2^k, including arbitrary common free GL3(F2) maps.", + "scope_change_reason": "This is an algebraic side question extending ToikY #4334 from two to three roles. It does not add a physically priced connector operation or claim a favorable complete supplier budget.", + "bottleneck_link": "Side result: the sharp common-direction obstruction rules out extending the two-role three-factor bound to three roles without extra cost. Native realization and complete recursive cost are unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified sharp finite result; do not minimize the component count or extend to other fields.", + "outcome": "completed", + "evidence": "All 2401 four-direction words reach at most 144 endpoints. The fixed five-direction word reaches all 168 GL3(F2) elements. Independent permutation enumeration agrees on every full mask. PROOF.md gives the all-k reduction and arbitrary-free-map lower bound.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the least k for which an invertible target over F2^k costs five?", + "why_it_matters": "It would make the universal 168-component obstruction smaller.", + "first_step": "Use complements of the computed four-word masks and their common right translates as a covering instance.", + "blocked_by": "The exact covering problem is unrun; the current witness is not claimed minimal." + }, + { + "question": "Can a literal physical producer and consumer implement one shared-direction factor at a favorable complete cost?", + "why_it_matters": "Formal factors alone do not imply native supplier savings.", + "first_step": "Specify coefficient acquisition, overwrite, access and reversible restoration before pricing the complete invoice.", + "blocked_by": "All physical preparation, routing, precision, stock and restoration costs remain unknown." + } + ], + "upstream_checkpoint": { + "commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "checked_at": "2026-10-22T20:23:34.456826+00:00", + "priority_revision": 7 + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132081" +} diff --git a/research/right-vector-three-role-products/VERIFY.json b/research/right-vector-three-role-products/VERIFY.json new file mode 100644 index 0000000000..45bda10b11 --- /dev/null +++ b/research/right-vector-three-role-products/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/right-vector-commutative-products/PROOF.md", + "research/right-vector-diagonal-free-basis/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact matrix and independent eight-vector-action endpoint masks; 614656 parameter tuples; fixed five-factor witnesses; all common free maps; delta; seven rejection controls; generated file-bound receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact matrix and independent eight-vector-action endpoint masks; 614656 parameter tuples; fixed five-factor witnesses; all common free maps; delta; seven rejection controls; generated file-bound receipt." + } + ] +} diff --git a/research/right-vector-three-role-products/verify.py b/research/right-vector-three-role-products/verify.py new file mode 100644 index 0000000000..3b1a79b267 --- /dev/null +++ b/research/right-vector-three-role-products/verify.py @@ -0,0 +1,271 @@ +#!/usr/bin/env python3 +"""Exact common-direction census; standard library only, no output files.""" + +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +IDENTITY = 273 # Three binary rows, least significant row first. +DIRECTIONS = tuple(range(1, 8)) +UPPER_WORD = (1, 2, 4, 1, 2) +EXPECTED = {4: 7, 16: 126, 24: 420, 64: 504, 96: 672, 144: 672} +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py" +) + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(left, right): + result = 0 + for row_index in range(3): + row = 0 + for column in range(3): + if left >> (3 * row_index + column) & 1: + row ^= right >> (3 * column) & 7 + result |= row << (3 * row_index) + return result + + +def rank(rows): + rows = list(rows) + check(len(rows) <= 504, "rank input exceeds fixed census capacity") + result = 0 + for bit in (1, 2, 4): + pivot = next((j for j in range(result, len(rows)) if rows[j] & bit), None) + if pivot is None: + continue + rows[result], rows[pivot] = rows[pivot], rows[result] + for j in range(result + 1, len(rows)): + if rows[j] & bit: + rows[j] ^= rows[result] + result += 1 + return result + + +def paid(left, direction): + check(0 <= left < 8 and 1 <= direction < 8, "factor outside binary alphabet") + check((left & direction).bit_count() % 2 == 0, "singular paid factor") + outer = sum((direction if left >> row & 1 else 0) << (3 * row) + for row in range(3)) + return IDENTITY ^ outer + + +def matrix_model(): + group = tuple(m for m in range(512) + if rank(tuple(m >> (3 * row) & 7 for row in range(3))) == 3) + check(len(group) == 168, "wrong matrix group order") + index = {matrix: i for i, matrix in enumerate(group)} + factors = {b: tuple(paid(a, b) for a in range(8) + if (a & b).bit_count() % 2 == 0) for b in DIRECTIONS} + transitions = {b: tuple(tuple(index[multiply(f, g)] for g in group) + for f in factors[b]) for b in DIRECTIONS} + return group, index, factors, transitions + + +def validate_census(masks): + check(set(masks) == set(product(DIRECTIONS, repeat=4)), "missing direction word") + check(all(0 <= mask < (1 << 168) for mask in masks.values()), "invalid endpoint mask") + histogram = dict(sorted(Counter(mask.bit_count() for mask in masks.values()).items())) + check(histogram == EXPECTED, "four-direction histogram mismatch") + return histogram + + +def matrix_census(index, transitions): + states = {(): frozenset((index[IDENTITY],))} + for _ in range(4): + states = {word + (b,): frozenset(table[g] for table in transitions[b] for g in s) + for word, s in states.items() for b in DIRECTIONS} + masks = {word: sum(1 << g for g in s) for word, s in states.items()} + return masks, validate_census(masks) + + +def compose(left, right): + return tuple(left[right[x]] for x in range(8)) + + +def encode_action(action): + # The images of the three basis vectors give the three columns. + return sum(((action[1 << col] >> row) & 1) << (3 * row + col) + for row in range(3) for col in range(3)) + + +def action_model(): + actions = [] + for basis in product(range(1, 8), repeat=3): + action = tuple((basis[0] if x & 1 else 0) + ^ (basis[1] if x & 2 else 0) + ^ (basis[2] if x & 4 else 0) for x in range(8)) + if len(set(action)) == 8: + actions.append(action) + actions.sort(key=encode_action) + check(len(actions) == 168 and len(set(actions)) == 168, "wrong action group") + index = {action: i for i, action in enumerate(actions)} + factor_ids = {} + for b in DIRECTIONS: + permitted = [] + for a in range(8): + action = tuple(x ^ (a if (b & x).bit_count() % 2 else 0) + for x in range(8)) + if len(set(action)) == 8: + permitted.append(index[action]) + check(len(permitted) == 4, "wrong independent factor count") + factor_ids[b] = tuple(permitted) + table = tuple(tuple(index[compose(a, b)] for b in actions) for a in actions) + return tuple(actions), factor_ids, table + + +def action_census(factor_ids, table): + pairs = {(b, c): tuple(table[g][f] for f in factor_ids[b] for g in factor_ids[c]) + for b in DIRECTIONS for c in DIRECTIONS} + masks = {} + evaluations = 0 + for word in product(DIRECTIONS, repeat=4): + mask = 0 + for first in pairs[word[:2]]: + for last in pairs[word[2:]]: + mask |= 1 << table[last][first] + evaluations += 1 + masks[word] = mask + check(evaluations == 614656, "incomplete independent parameter enumeration") + return masks, evaluations + + +def upper_witnesses(index): + witnesses = {IDENTITY: ()} + for b in UPPER_WORD: + next_witnesses = {} + for current, word in sorted(witnesses.items()): + for a in range(8): + if (a & b).bit_count() % 2 == 0: + endpoint = multiply(paid(a, b), current) + next_witnesses.setdefault(endpoint, word + (a,)) + witnesses = next_witnesses + check(set(witnesses) == set(index), "five-direction word is not universal") + return witnesses + + +def check_upper(actions, factor_ids, table, witnesses): + identity = actions.index(tuple(range(8))) + endpoints = set() + evaluations = 0 + for parameters in product(*(factor_ids[b] for b in UPPER_WORD)): + endpoint = identity + for factor in parameters: + endpoint = table[factor][endpoint] + endpoints.add(endpoint) + evaluations += 1 + check(len(endpoints) == 168 and evaluations == 1024, "independent upper word incomplete") + checks = 0 + for target, coefficients in sorted(witnesses.items()): + for x in range(8): + actual = x + for a, b in zip(coefficients, UPPER_WORD, strict=True): + actual ^= a if (b & actual).bit_count() % 2 else 0 + expected = sum(((target >> (3 * row) & x).bit_count() % 2) << row + for row in range(3)) + check(actual == expected, "literal component word changes the wrong input") + checks += 1 + check(checks == 1344, "incomplete arbitrary-input checks") + return checks + + +def free_maps_and_delta(group, factors): + all_factors = set(f for fs in factors.values() for f in fs) + conjugations = 0 + for free in group: + inverse = next(g for g in group if multiply(free, g) == IDENTITY) + check(multiply(inverse, free) == IDENTITY, "one-sided free inverse") + for fs in factors.values(): + for factor in fs: + check(multiply(multiply(free, factor), inverse) in all_factors, + "free conjugation leaves the paid alphabet") + conjugations += 1 + translated = tuple(multiply(m, free) for m in group) + check(set(translated) == set(group), "free right translation loses a target") + rows = tuple((m ^ IDENTITY) >> (3 * row) & 7 + for m in translated for row in range(3)) + check(rank(rows) == 3, "universal target does not have delta three") + check(conjugations == 4704, "incomplete conjugation checks") + return conjugations + + +def rejected(call): + try: + call() + except ValueError: + return 1 + raise ValueError("negative control was accepted") + + +def controls(masks, witnesses): + count = rejected(lambda: paid(1, 1)) + count += rejected(lambda: paid(0, 0)) + count += rejected(lambda: paid(8, 1)) + full = (1 << 168) - 1 + count += rejected(lambda: check(masks[(1, 2, 4, 1)] == full, "four is not five")) + altered = dict(masks) + del altered[(1, 1, 1, 1)] + count += rejected(lambda: validate_census(altered)) + altered = dict(masks) + altered[(1, 2, 4, 1)] = full + count += rejected(lambda: validate_census(altered)) + target = next(m for m, w in witnesses.items() if any(w)) + coefficients = list(witnesses[target]) + changed = next(i for i, a in enumerate(coefficients) if a) + coefficients[changed] = 0 + current = IDENTITY + for a, b in zip(coefficients, UPPER_WORD, strict=True): + current = multiply(paid(a, b), current) + count += rejected(lambda: check(current == target, "omitted nonidentity factor")) + check(count == 7, "incomplete rejection controls") + return count + + +def receipt(result): + package = Path(__file__).resolve().parent + source = json.loads((package / "SOURCES.json").read_text()) + check(len(source["files"]) <= 16, "source inventory exceeds fixed capacity") + files = {name: sha256((package / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + for row in source["files"]: + if row["usage"] == "input": + digest = sha256((package.parent.parent / row["path"]).read_bytes()).hexdigest() + check(digest == row["sha256"], "predecessor input changed") + files[row["path"]] = digest + return {"result": result, "files_sha256": files} + + +def main(): + argparse.ArgumentParser(description=__doc__).parse_args() + group, index, factors, transitions = matrix_model() + masks, histogram = matrix_census(index, transitions) + actions, factor_ids, table = action_model() + check(tuple(map(encode_action, actions)) == group, "independent group disagreement") + independent, evaluations = action_census(factor_ids, table) + check(independent == masks, "independent complete endpoint masks disagree") + witnesses = upper_witnesses(index) + dirty_checks = check_upper(actions, factor_ids, table, witnesses) + conjugations = free_maps_and_delta(group, factors) + control_count = controls(masks, witnesses) + payload = [[list(w), str(mask)] for w, mask in sorted(masks.items())] + result = {"group": len(group), "four_word_histogram": histogram, + "independent_parameter_tuples": evaluations, "upper_word": UPPER_WORD, + "upper_targets": len(witnesses), "arbitrary_input_checks": dirty_checks, + "free_conjugations": conjugations, "delta_cases": len(group), + "controls": control_count, + "census_sha256": sha256(json.dumps(payload).encode()).hexdigest(), + "witnesses_sha256": sha256(json.dumps(sorted(witnesses.items())).encode()).hexdigest()} + print(json.dumps(receipt(result), sort_keys=True)) + print("PASS_RIGHT_VECTOR_THREE_ROLE_PRODUCTS group=168 words4=2401 " + "max4=144 upper=5 delta=3 controls=7") + + +if __name__ == "__main__": + main()