From d0158a552352c09608295a7ec47dd31327b360ae Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:22:40 +0100 Subject: [PATCH] feat(research): prove unbounded polynomial right-vector cost --- .../right-vector-polynomial-cost/PROOF.md | 132 ++++++++++++ .../right-vector-polynomial-cost/README.md | 108 ++++++++++ .../right-vector-polynomial-cost/SOURCES.json | 24 +++ .../right-vector-polynomial-cost/TASK.json | 74 +++++++ .../right-vector-polynomial-cost/VERIFY.json | 34 +++ .../right-vector-polynomial-cost/verify.py | 199 ++++++++++++++++++ 6 files changed, 571 insertions(+) create mode 100644 research/right-vector-polynomial-cost/PROOF.md create mode 100644 research/right-vector-polynomial-cost/README.md create mode 100644 research/right-vector-polynomial-cost/SOURCES.json create mode 100644 research/right-vector-polynomial-cost/TASK.json create mode 100644 research/right-vector-polynomial-cost/VERIFY.json create mode 100644 research/right-vector-polynomial-cost/verify.py diff --git a/research/right-vector-polynomial-cost/PROOF.md b/research/right-vector-polynomial-cost/PROOF.md new file mode 100644 index 0000000000..bcdbbef8b1 --- /dev/null +++ b/research/right-vector-polynomial-cost/PROOF.md @@ -0,0 +1,132 @@ +# Exact polynomial right-vector cost + +Work over K=F2, R=F2[t], with two data roles and no scratch roles. +A paid factor is P(u,y)=I+u y^T, u in R^2 and y in K^2. +Every GL2(K) map is free anywhere. Cost counts paid factors. +All words below are written in algebraic product order. + +## Statement + +For each nonzero binary row y=(a,b), put v_y=(b,a)^T and +N_y=v_y y. For f in t F2[t], write T_y(f)=I+f N_y. +Every invertible target has a unique expression + + T_(y1)(f1) ... T_(yr)(fr) S, + +where S is in GL2(F2), every f_i is nonzero with zero constant term, +and consecutive directions y_i differ. Its exact paid cost is r. +In particular, with U=T_(0,1)(t), L=T_(1,0)(t), + + M = U L U L = [[1+t^2+t^4, t^3], [t^3, 1+t^2]] + +has cost 4. More generally (UL)^k has cost 2k for every k>=1. +Thus there is no uniform finite cost bound over all K-algebras, even +for two-role invertible targets over a commutative integral domain. +For k>=1, delta((UL)^k)=2, so the gap from the column lower bound +is unbounded too. + +This is the right-vector cost consequence of classical polynomial-matrix +normal forms, not a claim to a new group-theoretic normal-form theorem. +Nagao, *On GL(2,K[x])* (1959), Theorem 2 and its degree argument, +provides the classical structural context: +https://www.i-repository.net/contents/osakacu/sugaku/DB-M-010-02-04.pdf . +The proof below is self-contained for this binary cost statement. + +## 1. An invertible word only uses invertible paid factors + +Since R is commutative, det of a product is the product of determinants. +The only unit of F2[t] is 1. If a word has invertible endpoint, each +factor has determinant 1. For P(u,y), det P=1+y^T u. If y is nonzero, +invertibility therefore forces y^T u=0. The solution space of that +equation is u=f v_y for a unique polynomial f, including f=0. +Hence every usable paid factor is T_y(f). The case y=0 is identity. +Singular factors cannot evade this reduction. + +We have N_y^2=0 and T_y(f)T_y(g)=T_y(f+g). Split +f=f(0)+(f+f(0)); the constant part T_y(f(0)) is free. For any free S, +conjugation S T_y(f) S^-1 is T_z(f) for another nonzero binary row z. +Indeed the conjugated nonzero nilpotent has image equal to kernel, +and over F2 there is exactly one nonzero rank-one nilpotent with each +of the three kernel lines. This also follows directly from z=y S^-1 +and S v_y=v_z, since every invertible binary 2x2 determinant is 1. + +Move all free factors to the right, split off all constant parts, +and merge adjacent equal directions, deleting zero coefficients. +Every finite invertible word thus has the stated form with at most +as many nonconstant factors as its original paid count. Evaluation at +t=0 shows the final free matrix is necessarily S=M(0). + +## 2. A reduced nonempty word cannot be constant + +For distinct nonzero binary rows y,z, + + y v_z = a d + b c = 1 + +when y=(a,b), z=(c,d). Consequently + + N_(y1) ... N_(yr) = v_(y1) y_r != 0 + +whenever adjacent directions differ. Let d_i=deg f_i>=1. In the +expansion of a reduced product, the term choosing f_i N_(yi) from +every factor has degree D=sum d_i and nonzero leading coefficient +v_(y1) y_r. Every term omitting at least one factor has smaller degree. +Thus the degree of the matrix product, defined as the maximum entry +degree, is exactly D>0. Multiplication by an invertible constant S +preserves this degree because its leading matrix remains nonzero. + +This proves the degree test for arbitrary polynomial coefficients, +without any degree cap or finite search assumption. + +## 3. Uniqueness and exact cost + +Suppose two reduced products are equal. Their free endpoints agree by +evaluation at zero, so cancel them. Multiply the inverse of one product +by the other. Since each T_y(f) is its own inverse, cancel the common +initial factors at the middle of this concatenation. At the first +mismatch, either the directions differ, or their nonzero coefficients +sum to a nonzero polynomial in tF2[t]. In the latter case merge that +pair. The remaining concatenation is reduced and nonempty unless the +original products agreed factor by factor. A nonempty reduced product +has positive degree by Section 2, so cannot be identity. This proves +uniqueness. + +Now a target with reduced length r has a literal r-paid-factor word. +Any other word with q paid factors reduces to the same unique expression +and the reduction does not increase the number of paid factors. Hence +q>=r, proving cost=r. + +For completeness every GL2(F2[t]) target is reachable. Euclidean row +reduction on its first column uses row swaps and shears adding a +polynomial multiple of one row to the other. The swaps are free and +the shears are paid factors. The first-column gcd is 1 because the +determinant is 1. After it is changed to (1,0)^T, the remaining matrix +is [[1,b],[0,1]], also a paid factor. The usual polynomial division +strictly decreases the nonzero remainder degree, so this process +terminates. Reversing these invertible operations gives a finite word. +This existence argument is not needed for the four-factor lower bound. + +## 4. The first counterexample and its corollary + +U,L have different directions and coefficient t. Their alternating +word of length 2k is already reduced, so costs exactly 2k. Direct +multiplication at k=2 gives the displayed M. In particular a third +factor never suffices for M. This answers Open next question 1 of +Nick Petalas's #4276 negatively. The proof covers arbitrary polynomial +left coefficients and all insertions of free binary maps, rather than +only words in U and L. + +By the column lower bound and one-factor criterion of #4243/#4276, +delta<=1 would imply cost<=1. Delta is at most two for two roles, +so every (UL)^k with k>=1 has delta=2. This is predecessor use, not +an independent re-verification of that criterion. + +## Scope + +This is a scoped algebraic proof, with a finite corroborating census. +The algebra F2[t] is not semilocal: its distinct irreducible polynomials +give infinitely many maximal ideals. It lies outside #4749's hypothesis. +No contradiction with the semilocal three-factor theorem follows. +The polynomial t here is an algebra coefficient, not a free change of +basis. Allowing GL2(F2[t]) for free would change the question. +No native preparation, conversion, precision, routing, restoration, +stock, supplier admission or multiplication theorem is proved. diff --git a/research/right-vector-polynomial-cost/README.md b/research/right-vector-polynomial-cost/README.md new file mode 100644 index 0000000000..8e02119fab --- /dev/null +++ b/research/right-vector-polynomial-cost/README.md @@ -0,0 +1,108 @@ +# Two-role polynomial targets have unbounded right-vector cost + +Claim type: scoped proof, with a finite exact certificate. No new kappa. + +In the alphabet `I+u y^T`, with `u in F2[t]^2`, binary `y`, and free +`GL2(F2)` maps anywhere, put + +```text +U = [[1,t],[0,1]], L = [[1,0],[t,1]]. +M = (UL)^2 = [[1+t^2+t^4, t^3], [t^3, 1+t^2]]. +cost(M) = 4; cost((UL)^k) = 2k for every k >= 1. +``` + +This answers Open next question 1 of +[Nick Petalas's #4276](https://github.com/CrocSwap/integer-mult-bounds/pull/4276) +negatively: reachable two-role targets need not have three-factor words over +every coefficient algebra. The gap from `delta`, which equals two on this +family, is unbounded. The algebra is commutative but not semilocal, so this +lies outside the three-factor theorem of +[#4749](https://github.com/CrocSwap/integer-mult-bounds/pull/4749), pinned at +`29e4d3a25225a219f97c3a2815ed3a5a8fd9b891`. + +[PROOF.md](PROOF.md) reduces every invertible paid factor to a transvection, +removes its constant part using the free group, and proves uniqueness of the +resulting reduced word by polynomial degree. Its reduced length is the exact +paid cost. The normal-form structure is classical polynomial-matrix theory; +the contribution is its explicit cost consequence for the repository's +restricted alphabet and its open three-factor question. + +## Evidence and reproduction + +The verifier uses literal binary polynomial arithmetic and no predecessor +code. It enumerates every invertible 2x2 polynomial matrix whose maximum +entry degree is at most four. The 1,536 distinct targets have exact cost +histogram `[6,270,612,504,144]` for costs zero through four. The written degree +proof establishes why arbitrary larger coefficients cannot produce additional +shorter words in this domain. All 1,008 reduced expressions of degree four +and length at most three, including every free endpoint, miss M. + +A separate literal alphabet check enumerates all three nonzero binary right +vectors and all `32^2` polynomial left vectors of degree at most four. +Exactly 96 parameter tuples are invertible, including repeated identities. +Every tuple passes the constant split and all six free conjugations. +Seven controls distinguish equal-direction cancellation, constant polynomial +relations, specialization at zero, a dropped factor, reversed order, a +singular factor and a changed target entry. Every comparison remains active +under optimized Python. No generated output is written to the checkout. + +From the repository root, using the Python 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-polynomial-cost/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-polynomial-cost/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-polynomial-cost +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-polynomial-cost --check-source-history +``` + +Expected marker: `PASS_RIGHT_VECTOR_POLYNOMIAL_COST targets=1536 cost4=144 +target_cost=4 shorter_exclusions=1008 controls=7 no_new_kappa`. +The receipt is freshly generated from actual checks and hashes every package +file. It is not a handwritten verification receipt. + +## Limitations + +The universal argument is a written scoped proof. Its finite certificate +corroborates the degree-four domain; it does not prove the infinite statement +by enumeration. The base field is binary, the coefficient algebra is F2[t], +and there are two data roles with no scratch. Singular targets, other base +fields and multivariate algebras are not classified. Free maps must be binary. +Native preparation, conversion, routing, control, precision, restoration and +stock costs are unknown. No supplier, selected-frontier change or complete +multiplication theorem is claimed. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and the selected operator replay were not +run and are outside this result's obligations. + +The verifier uses managed Python allocation with an explicit finite domain. +The census stores 256 normal words and 1,536 targets. Enumeration has at most +four factor rounds, three directions, 15 nonconstant coefficients and six free +maps; the literal control examines 3,072 tuples. Polynomial multiplication +accepts at most 32 bits per operand and iterates over at most 32 bits. +Functions are below 60 lines, recursion and dynamic code are absent, and both +registered commands make warnings errors. Python allocation is a documented +allocation deviation with these fixed bounds; no real-time claim is made. + +## Open next questions + +1. Classify exact costs over `F2[s,t]`. Start with a named reachable word and + distinguish its cost from general reachability. The present one-variable + normal-form and Euclidean arguments do not settle that algebra. +2. Identify one coefficient algebra in a literal native producer/consumer, + then price left-coefficient preparation and the complete physical bill. + All native costs listed above remain blockers to a supplier construction. + +## Credit + +This contribution was produced by Nick Petalas. The right-vector alphabet and +column lower bound are Wentao Li's #4099, building on #2513. Nick Petalas's +#4243 supplies the free-map normal form, and #4276 supplies the one-factor +criterion and asks the all-algebra three-factor question answered here. +ToikY's #4334 and Nick Petalas's #4601/#4749 supply the field-product, +local-product and semilocal predecessor boundaries. Their proofs and +certificates are cited, not re-audited. + +The polynomial-matrix group structure and degree method retain Hirosi +Nagao's credit, *On GL(2,K[x])*, 1959, Theorem 2 and its proof +([original paper](https://www.i-repository.net/contents/osakacu/sugaku/DB-M-010-02-04.pdf)). +The restricted-alphabet cost consequence is proved here without relying on +a machine implementation of that theorem. Apache-2.0. diff --git a/research/right-vector-polynomial-cost/SOURCES.json b/research/right-vector-polynomial-cost/SOURCES.json new file mode 100644 index 0000000000..1bbbafcf20 --- /dev/null +++ b/research/right-vector-polynomial-cost/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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-two-factor-criterion/PROOF.md", + "usage": "input", + "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c", + "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895" + } + ] +} diff --git a/research/right-vector-polynomial-cost/TASK.json b/research/right-vector-polynomial-cost/TASK.json new file mode 100644 index 0000000000..9b188e5e8b --- /dev/null +++ b/research/right-vector-polynomial-cost/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "Exact right-vector paid cost for invertible two-role targets over F2[t]; cost four for (UL)^2 and unbounded cost 2k for (UL)^k.", + "scope_change_reason": "The connector card is changed to the all-algebra three-factor question explicitly left open by #4276. The non-semilocal polynomial coefficient algebra changes the semilocal premise of #4749. This is a formal-alphabet side result, not an extension of the source-toggle census.", + "bottleneck_link": "A scoped obstruction to a universal three-factor abstraction. The result gives no native implementation or multiplication saving.", + "budget_minutes": 60, + "stop_rule": "Package the first exact cost-four target, its reduced-word lower bound and direct corollary; do not search larger examples.", + "outcome": "completed", + "evidence": "PROOF.md gives a self-contained quantified degree proof. verify.py enumerates all 1536 invertible polynomial matrices of maximum entry degree at most four, with cost histogram [6,270,612,504,144], checks 96 literal invertible paid parameter tuples and seven negative controls, and emits a generated file-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact right-vector cost over a multivariate polynomial algebra such as F2[s,t]?", + "why_it_matters": "The one-variable degree normal form and Euclidean reachability do not supply a classification there.", + "first_step": "Specify one reachable word whose two variable directions cannot be collapsed by the single-variable argument; separate reachability from lower bounds.", + "blocked_by": "No multivariate normal-form or reachability theorem is supplied here." + }, + { + "question": "Which finitely generated coefficient algebras occurring in a literal native interface preserve a bounded two-role cost?", + "why_it_matters": "The abstract alphabet can have unbounded cost, while the semilocal theorem gives a three-factor bound.", + "first_step": "Identify one actual coefficient algebra and price polynomial left-coefficient preparation, conversion and the complete consumer.", + "blocked_by": "Native preparation, conversion, routing, precision, restoration and stock costs are unknown." + } + ], + "upstream_check": { + "commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b", + "checked_at": "2026-10-22T19:22:25.168050+00:00", + "priority_revision": 7, + "result": "Relevant guidance, selected record, catalogue and pinned proof input unchanged from the frozen scientific baseline. New main research README searches found no polynomial-cost duplicate." + } +} diff --git a/research/right-vector-polynomial-cost/VERIFY.json b/research/right-vector-polynomial-cost/VERIFY.json new file mode 100644 index 0000000000..1193429452 --- /dev/null +++ b/research/right-vector-polynomial-cost/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/right-vector-two-factor-criterion/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal polynomial-matrix census of all 1536 degree-at-most-four invertible targets, reduced-word degree identities, cost-four witness, 1008 shorter degree-four exclusions, 96 literal invertible paid parameter tuples, free conjugation and seven negative controls. Generated receipt binds all six package files. Checks remain active under optimization." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal polynomial-matrix census of all 1536 degree-at-most-four invertible targets, reduced-word degree identities, cost-four witness, 1008 shorter degree-four exclusions, 96 literal invertible paid parameter tuples, free conjugation and seven negative controls. Generated receipt binds all six package files. Checks remain active under optimization." + } + ] +} diff --git a/research/right-vector-polynomial-cost/verify.py b/research/right-vector-polynomial-cost/verify.py new file mode 100644 index 0000000000..c7ed9558d0 --- /dev/null +++ b/research/right-vector-polynomial-cost/verify.py @@ -0,0 +1,199 @@ +#!/usr/bin/env python3 +"""Exact F2[t] matrices corroborating the scoped reduced-word cost proof.""" +import hashlib +import itertools +import json +from pathlib import Path + +IDENTITY = (1, 0, 0, 1) +DIRECTIONS = (1, 2, 3) +MAX_DEGREE = 4 +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py" +) + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def multiply_polynomial(a, b): + require(0 <= a < 2**32 and 0 <= b < 2**32, "polynomial capacity") + result = 0 + for bit in range(b.bit_length()): + if (b >> bit) & 1: + result ^= a << bit + return result + + +def multiply(a, b): + return tuple( + multiply_polynomial(a[2*i], b[j]) + ^ multiply_polynomial(a[2*i+1], b[2+j]) + for i in range(2) for j in range(2) + ) + + +def transvection(direction, coefficient): + require(direction in DIRECTIONS, "invalid direction") + a, b = direction & 1, direction >> 1 + return ( + 1 ^ (coefficient if a*b else 0), coefficient if b else 0, + coefficient if a else 0, 1 ^ (coefficient if a*b else 0) + ) + + +def degree(matrix): + return max(value.bit_length() - 1 for value in matrix) + + +def determinant(matrix): + a, b, c, d = matrix + return multiply_polynomial(a, d) ^ multiply_polynomial(b, c) + + +def evaluate_word(word): + result = IDENTITY + for direction, coefficient in word: + result = multiply(result, transvection(direction, coefficient)) + return result + + +def free_matrices(): + return tuple(a for a in itertools.product(range(2), repeat=4) + if determinant(a) == 1) + + +def delta(matrix, free): + values = [] + for endpoint in free: + product = multiply(matrix, endpoint) + columns = ((product[0] ^ 1, product[2]), + (product[1], product[3] ^ 1)) + nonzero = set(columns) - {(0, 0)} + values.append(min(2, len(nonzero))) + return min(values) + + +def reduced_words(): + # At most four factors, three directions and 15 allowed coefficients. + states = [((), IDENTITY, 0)] + frontier = states + for _length in range(MAX_DEGREE): + next_frontier = [] + for word, matrix, total in frontier: + for direction in DIRECTIONS: + if word and word[-1][0] == direction: + continue + for coefficient in range(2, 2**(MAX_DEGREE+1), 2): + new_total = total + coefficient.bit_length() - 1 + if new_total <= MAX_DEGREE: + next_word = word + ((direction, coefficient),) + product = multiply(matrix, transvection(direction, coefficient)) + require(degree(product) == new_total, "degree sum failed") + require(determinant(product) == 1, "word not invertible") + next_frontier.append((next_word, product, new_total)) + states.extend(next_frontier) + frontier = next_frontier + require(len(states) == 256, "normalized-word census") + return states + + +def census(states, free): + seen = {} + histogram = [0] * 5 + for word, matrix, total in states: + require(evaluate_word(word) == matrix, "chronological product mismatch") + for endpoint in free: + target = multiply(matrix, endpoint) + require(target not in seen, "normal form collision") + require(degree(target) == total, "free endpoint changed degree") + cost = len(word) + require(delta(target, free) == min(2, cost), "column comparison") + seen[target] = word, endpoint + histogram[cost] += 1 + require(histogram == [6, 270, 612, 504, 144], "cost histogram") + return seen, histogram + + +def literal_paid_control(free): + count = 0 + # Enumerate all three nonzero y and all 32^2 possible polynomial left vectors. + for direction in DIRECTIONS: + a, b = direction & 1, direction >> 1 + for u0, u1 in itertools.product(range(32), repeat=2): + matrix = (1 ^ (u0 if a else 0), u0 if b else 0, + u1 if a else 0, 1 ^ (u1 if b else 0)) + if determinant(matrix) != 1: + continue + coefficient = u0 if b else u1 + require(matrix == transvection(direction, coefficient), "paid reduction") + constant = transvection(direction, coefficient & 1) + require(constant in free, "constant factor not free") + split = transvection(direction, coefficient ^ (coefficient & 1)) + require(multiply(split, constant) == matrix, "constant split") + for endpoint in free: + # Binary inverse is found in the complete six-element free group. + inverses = [s for s in free if multiply(endpoint, s) == IDENTITY] + require(len(inverses) == 1, "free inverse") + conjugate = multiply(multiply(endpoint, split), inverses[0]) + require(conjugate in [transvection(y, coefficient & ~1) + for y in DIRECTIONS], "conjugation closure") + count += 1 + require(count == 96, "literal invertible paid parameter count") + return count + + +def target_and_controls(seen): + word = ((2, 2), (1, 2), (2, 2), (1, 2)) + target = evaluate_word(word) + require(target == (21, 8, 8, 5), "four-factor target polynomial") + require(len(seen[target][0]) == 4, "target cost") + exclusions = sum(1 for candidate, endpoint in seen.values() + if len(candidate) <= 3 and degree(evaluate_word(candidate)) == 4) + require(exclusions == 1008, "degree-four shorter-word exclusions") + require(multiply(transvection(1, 2), transvection(1, 2)) == IDENTITY, + "equal-direction cancellation control") + constant = multiply(transvection(2, 1), transvection(1, 1)) + require(multiply(multiply(constant, constant), constant) == IDENTITY, + "constant-coefficient relation control") + require(tuple(p & 1 for p in target) == IDENTITY, "specialization control") + require(evaluate_word(word[:-1]) != target, "dropped factor control") + require(evaluate_word(tuple(reversed(word))) != target, "word-order control") + require(determinant((0, 0, 0, 1)) == 0, "singular-factor control") + require((target[0] ^ 1, *target[1:]) not in seen, "changed entry control") + return target, exclusions + + +def receipt(root, histogram, target, exclusions, paid_count): + sources = json.loads((root / "SOURCES.json").read_text()) + repository = root.parent.parent + for row in sources["files"]: + if row["usage"] == "input": + payload = (repository / row["path"]).read_bytes() + require(hashlib.sha256(payload).hexdigest() == row["sha256"], "source hash") + hashes = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + result = {"schema": "right-vector-polynomial-cost/v1", "files_sha256": hashes, + "targets": sum(histogram), "cost_histogram": histogram, + "target_polynomial_bits": target, "target_cost": 4, + "shorter_degree_four_exclusions": exclusions, + "literal_paid_parameters": paid_count, "negative_controls": 7} + print(json.dumps(result, sort_keys=True)) + print("PASS_RIGHT_VECTOR_POLYNOMIAL_COST targets=1536 cost4=144 target_cost=4 " + "shorter_exclusions=1008 controls=7 no_new_kappa") + + +def main(): + free = free_matrices() + require(len(free) == 6, "free group cardinality") + states = reduced_words() + seen, histogram = census(states, free) + paid_count = literal_paid_control(free) + target, exclusions = target_and_controls(seen) + receipt(Path(__file__).resolve().parent, histogram, target, exclusions, paid_count) + + +if __name__ == "__main__": + main()