From f1c69a4e22b670dcc018707fb6a4198e5ecf8b2a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 19:34:03 +0000 Subject: [PATCH] feat(research): classify alternating four-call lattice descent --- .../bit-four-use-alternating-descent/PROOF.md | 154 ++++++++++ .../README.md | 131 +++++++++ .../SOURCES.json | 24 ++ .../TASK.json | 78 ++++++ .../VERIFY.json | 34 +++ .../verify.py | 262 ++++++++++++++++++ 6 files changed, 683 insertions(+) create mode 100644 research/bit-four-use-alternating-descent/PROOF.md create mode 100644 research/bit-four-use-alternating-descent/README.md create mode 100644 research/bit-four-use-alternating-descent/SOURCES.json create mode 100644 research/bit-four-use-alternating-descent/TASK.json create mode 100644 research/bit-four-use-alternating-descent/VERIFY.json create mode 100644 research/bit-four-use-alternating-descent/verify.py diff --git a/research/bit-four-use-alternating-descent/PROOF.md b/research/bit-four-use-alternating-descent/PROOF.md new file mode 100644 index 0000000000..641d23d076 --- /dev/null +++ b/research/bit-four-use-alternating-descent/PROOF.md @@ -0,0 +1,154 @@ +# Alternating four-call lattice descent + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Model and statement + +Let K be any field of characteristic two, let n be a positive integer, +and let P,Q in M_n(K) be rank-one idempotents. Work over the Laurent +polynomial ring K[z,z^-1], with z an indeterminate. Put + + E_z(P) = I + (z-1)P, + W(P,Q) = E_z(P) E_z(Q) E_z(P) E_z(Q), + tau = tr(PQ). + +Products act on columns with the rightmost factor acting first. A matrix +is even if every entry belongs to K[z^2,z^-2]. In address notation z=[s], +this is descent from Zs to its subgroup 2Zs. There are no intervening +address-dependent operations in the alternating word studied here. + +**Theorem.** W(P,Q) is even if and only if + + P=Q or tau=0. + +Every even W(P,Q) is a product of exactly two rank-one calls labelled z^2: + +1. If P=Q, then W(P,P) = E_(z^2)(P) E_(z^2)(P). +2. If P!=Q and tau=0, put + + P' = P+PQ, Q' = Q+QP. + + These are rank-one idempotents with P'Q'=Q'P'=0, and + + W(P,Q) = E_(z^2)(P') E_(z^2)(Q') + = I+(z^2-1)(P'+Q'). + +The sum P'+Q' is a rank-two projector. The two-call count is minimal +among words of rank-one z^2 calls and arbitrary constant invertible maps. +This is an algebraic call count. It makes no assertion that a coarse +label has the same native price as a fine label. + +## The odd coefficient determines descent + +Write P=u v and Q=x y, where u,x are nonzero columns, v,y are rows, +and vu=yx=1. These factorizations exist for rank-one idempotents. +With alpha=vx and beta=yu, elementary multiplication gives + + tau=alpha beta, + PQP=tau P, QPQ=tau Q, (PQ)^2=tau PQ. + +Set a=z+1, N=P+Q and B=PQ. Then + + E_z(P) E_z(Q) = I+aN+a^2 B, + N^2 = N+PQ+QP, + NB+BN = tau N. + +Squaring the first identity, keeping the matrix order, yields + + W(P,Q) = I + a^2(N+PQ+QP) + a^3 tau N + a^4 tau PQ. + +In characteristic two a^2=1+z^2, a^4=1+z^4 and +a^3=1+z+z^2+z^3. Hence the coefficients of both z and z^3 in W +are exactly tau(P+Q). There are no other odd degrees. Since K is a +field, that coefficient vanishes precisely when tau=0 or P=Q. This +proves the necessary-and-sufficient criterion, for every finite n. + +No reduction of a rational address label modulo the field characteristic +is used. The address exponent and the scalar coefficient field are +different objects. + +## Constructive descent + +If P=Q, idempotence gives E_z(P)^2=E_(z^2)(P), proving case 1. +Suppose tau=0. The displayed rank-one identities give + + (P+PQ)^2=P+PQ, (Q+QP)^2=Q+QP, + (P+PQ)(Q+QP)=0, (Q+QP)(P+PQ)=0. + +The image of P+PQ lies in the one-dimensional image of P. Also +(P+PQ)u=u, because PQP=0. Thus P' has rank one. The same argument +gives rank Q'=1. Orthogonality makes their images disjoint, so P'+Q' +is an idempotent of rank two. In particular tau=0 already implies P!=Q. + +The odd-coefficient expansion now reduces to + + W(P,Q)=I+(z^2+1)(P+Q+PQ+QP). + +Multiplying the two proposed coarse calls, their cross term vanishes by +P'Q'=0. Their product is this same matrix. This proves case 2 and its +complete action on arbitrary input columns, including all spectators. + +For minimality, a rank-one idempotent is similar over K to +diag(1,0,...,0). Consequently det E_z(P)=z and det W=z^4. +A word with L rank-one z^2 calls and constant invertible maps has +determinant c z^(2L), for a nonzero constant c. Equality with W forces +L=2 and c=1. The argument allows free constant maps anywhere in the word. + +## A smallest failure of adjacent-pair descent + +Over F2 take + + P = [[1,0], Q = [[0,1], + [0,0]], [0,1]]. + +Here QP=0 and PQ=[[0,1],[0,0]] is nonzero. In particular P and Q do +not commute. The theorem supplies + + P'=[[1,1],[0,0]], Q'=Q, P'+Q'=I, + W(P,Q)=z^2 I_2. + +No proper nonempty consecutive block of this four-call word is even. +Blocks of length one or three have determinant z or z^3, whereas the +determinant of an even matrix is even. Every length-two block is an +alternating pair of distinct projectors. Its coefficient of z is P+Q, +which is nonzero. These are all nine proper consecutive blocks. + +This is the smallest example relevant to iterating a two-use reduction. +An odd number of positive rank-one z calls cannot have an even endpoint +by determinant parity. A two-call word is even exactly when its two +projectors agree, by the same coefficient calculation, and then the +two-use contraction already applies. Four calls therefore give the first +even endpoint with no even adjacent pair. + +Embedding P,Q as zero on any additional coordinates gives this example at +every n>=2. W is diag(z^2,z^2,1,...,1), so the additional coordinates +are restored for arbitrary initial data. No zero-initialized scratch is +assumed. + +The example does not contradict the two-use theorem of CubeJerry's +[PR6148](https://github.com/CrocSwap/integer-mult-bounds/pull/6148). +That theorem assumes exactly two odd calls in the block being contracted. +The example has four. It rules out a proposed shortcut that would require +every even four-call endpoint to expose an even adjacent pair. The new +coarse projectors show how this particular alternating class descends +despite the absence of such a pair. + +## Scope and remaining obligations + +The universal statement is this written proof. The verifier independently +multiplies full polynomial matrices and applies the literal factors to +basis columns over finite fields. Those checks corroborate the proof in +their stated finite domains. They are not its all-width justification. + +The result assumes an infinite-order address generator, one repeated fine +label, constant rank-one projectors, characteristic two, and the alternating +four-factor order. Four unrelated projectors, arbitrary intervening even +operations, finite-order address collisions, and other characteristics are +outside its classification. It does not establish a universal four-use +descent rule or classify the surviving eight-call profiles of PR6111. + +No complete supplier bill, native conversion for 2s, restored physical +caller, target inventory, stock, compiler, precision/tape implementation, +new kappa or complete multiplication theorem is supplied. The current +selected record and its five framework assumptions are unchanged. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/bit-four-use-alternating-descent/README.md b/research/bit-four-use-alternating-descent/README.md new file mode 100644 index 0000000000..721b759f97 --- /dev/null +++ b/research/bit-four-use-alternating-descent/README.md @@ -0,0 +1,131 @@ +# Exact descent for four alternating BIT calls + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof with finite exact corroboration.** No new +kappa, native supplier or complete multiplication theorem is claimed. + +Let K be any characteristic-two field and let P,Q be rank-one idempotents +of any finite size. Write E_z(P)=I+(z-1)P, with z an infinite-order address +monomial. Then + + E_z(P) E_z(Q) E_z(P) E_z(Q) is even + if and only if P=Q or tr(PQ)=0. + +Here even means that every entry has only even powers of z. If P=Q, the +word equals E_(z^2)(P)^2. Otherwise, for tr(PQ)=0, its exact factorization is + + E_(z^2)(P+PQ) E_(z^2)(Q+QP). + +The new projectors are rank one and mutually orthogonal. Exactly two coarse +calls are necessary by determinant degree, even with arbitrary free constant +invertible maps. Their native cost is not established by this algebraic count. + +A noncommuting example has + + P=[[1,0],[0,0]], Q=[[0,1],[0,1]], word=z^2 I_2. + +All nine proper nonempty consecutive blocks are not even. Four is the +smallest call count that can have an even endpoint without exposing an even +adjacent pair. Thus iterating an adjacent-pair rule cannot exhaust even +four-use words. The explicit coarse factorization resolves this alternating +class without such a rule. The complete argument is in [PROOF.md](PROOF.md). + +## Evidence + +The verifier enumerates all ordered rank-one idempotent pairs in each row. +One engine multiplies polynomial matrices. A second engine applies literal +factors to every basis column without polynomial matrix multiplication. +Both compare the complete endpoint, including arbitrary dirty spectator +columns. Every even case also has its proposed coarse factors multiplied. + +| Field | Width | Ordered pairs | Equal | Orthogonal distinct | Noncommuting even | Not even | +|---|---:|---:|---:|---:|---:|---:| +| F2 | 1 | 1 | 1 | 0 | 0 | 0 | +| F2 | 2 | 36 | 6 | 6 | 12 | 12 | +| F2 | 3 | 784 | 28 | 168 | 336 | 252 | +| F2 | 4 | 14400 | 120 | 3360 | 6720 | 4200 | +| F4 | 1 | 1 | 1 | 0 | 0 | 0 | +| F4 | 2 | 400 | 20 | 20 | 120 | 240 | +| F8 | 1 | 1 | 1 | 0 | 0 | 0 | +| F8 | 2 | 5184 | 72 | 72 | 1008 | 4032 | + +There are 20807 pairs in total. Separate controls enumerate the nine proper +blocks, check five semantic predicates including missing cross-term and +changed-call mutations, and reject six invalid inputs with exact reasons. +The generated stdout receipt binds the package files by SHA256. No receipt +is handwritten and replay writes no files. + +## Reproduce + +From the repository root, using the Python 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/bit-four-use-alternating-descent/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/bit-four-use-alternating-descent/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bit-four-use-alternating-descent +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bit-four-use-alternating-descent --check-source-history +``` + +Other hosts may use any CPython 3.12 interpreter. The expected receipt status +is `PASS_BIT_FOUR_USE_ALTERNATING_DESCENT`. Each registered command has a +120-second timeout. Direct replay is also Git-free and needs only these six +package files. Source pins are historical provenance, not imported code or +runtime dependencies. The selected baseline binding command passed at +canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. + +## Credit and scope + +CubeJerry's [PR6148](https://github.com/CrocSwap/integer-mult-bounds/pull/6148) +poses the four-odd-call question and proves two-use descent. This result +answers its suggested first step for an alternating class; it does not +replay the predecessor or settle general four-use descent. Its README is +pinned as provenance in [SOURCES.json](SOURCES.json). + +Credit JosieElliston PR6111 and JoyboyBrian PR6104 for the two-frame questions, +apoursh PR6089 for the one-frame work, Nick Petalas PR2910 for the determinant +model, Cinna Davis PR2085/2112 for the endpoint/operation model, Philippe Van +Velzen for the earlier BIT call floor, and their retained lineage. Rank-one +factorization, determinant degree and characteristic-two expansion are +classical methods; no literature priority for them is claimed. + +The originating card is explicitly changed to this algebraic side result in +[TASK.json](TASK.json). No actual native doubled-frame tariff, target inventory, +physical caller, stock, compiler, precision/tape implementation or outer bill +is supplied. No general four-projector theorem, arbitrary intervening-even +operation theorem, finite-order address claim or other-characteristic claim +is made. The universal claim rests on the written proof. The finite census +has only its displayed coverage. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker, predecessor scientific suites and the +selected complete replay were not run. The selected frontier is unchanged. + +## Code constraints + +Scientific loops have fixed domains: width at most four, field size at most +eight, word length at most four and polynomial degree at most four. The +largest pair domain has 14400 entries and is streamed. Matrices have at most +16 entries, the largest projector list used has 120 entries, and no search, +subprocess, recursion or external import is used. Every function has fewer +than 60 physical lines. Checks use explicit exceptions and remain active +under optimized Python. Both registered commands make warnings errors. + +Power-of-ten rule 3 deviation: Python integers, tuples and standard-library +operations allocate dynamically. The fixed domains above bound live data; +only one pair's polynomial endpoint is retained at a time. There is no +real-time guarantee. Extending the finite domains requires revisiting those +bounds before enlarging the replay. The package's standalone verifier has +no public mutable state or cleanup ownership. Optional external analyzers +are not part of its environment; syntax is checked by in-memory compilation. + +## Open next questions + +1. Does an even word of four unrelated rank-one projectors always admit two + coarse calls? Start with full polynomial endpoints at width two and seek + a counterexample or a replacement invariant. The alternating-square + calculation does not cover that question. +2. Can an actual BIT profile use this factorization with a favorable native + invoice? First identify the exact four-call region, source/target contracts + and a priced doubled-frame implementation. No physical realization or + complete bill is supplied here. + +TASK.json records why these questions matter, their first steps and blockers. diff --git a/research/bit-four-use-alternating-descent/SOURCES.json b/research/bit-four-use-alternating-descent/SOURCES.json new file mode 100644 index 0000000000..bd46207a03 --- /dev/null +++ b/research/bit-four-use-alternating-descent/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-two-use-lattice-descent/README.md", + "usage": "provenance", + "git_blob": "0b29fc26fe73f5cdc44b121ed406b65bdce59e12", + "sha256": "d078d83e7f902b0cc68a43e33825ab0ae869acd6c97eda31990814e75d46b7a4" + } + ] +} diff --git a/research/bit-four-use-alternating-descent/TASK.json b/research/bit-four-use-alternating-descent/TASK.json new file mode 100644 index 0000000000..089cf8f0d3 --- /dev/null +++ b/research/bit-four-use-alternating-descent/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Classify even endpoints and construct coarse factorizations for four alternating rank-one calls over every characteristic-two field, with a smallest noncommuting example having no proper even consecutive block.", + "scope_change_reason": "The current picker suggested verification tooling. The explicit original-result assignment takes precedence; this takes Open next question 2 of CubeJerry PR6148 as an algebraic side result instead of repeating a census or auditing a predecessor.", + "bottleneck_link": "An exact descent rule can strengthen BIT profile pruning. The example prevents rejecting four-use words solely because no even adjacent pair is exposed; native coarse-label pricing and an actual supplier remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved and reproducible original improvement; do not extend from this alternating class to general four-call words.", + "outcome": "completed", + "evidence": "PROOF.md proves the all-field/all-width criterion and two-call factorization. verify.py checks 20807 ordered pairs over F2/F4/F8 with two literal polynomial engines, all nine proper blocks of the noncommuting example, five semantic checks and six invalid inputs.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does every even product of four arbitrary rank-one z calls admit a two-call z^2 factorization, when its projectors are not alternating?", + "why_it_matters": "This would decide whether the same exact coarse-label simplification extends beyond the proved family.", + "first_step": "Expand four independent projectors over F2 at width two and seek a counterexample or a separate factorization invariant; retain exact full polynomial endpoints.", + "blocked_by": "The single trace invariant proved here uses the alternating square and does not settle four independent projectors." + }, + { + "question": "Can a source-bound BIT profile use this descent at a favorable complete native cost?", + "why_it_matters": "Only native prices, restored inputs and independent productive targets could turn the algebraic simplification into a supplier improvement.", + "first_step": "Identify one exact four-call region, its complete boundary contract and the actual implementation/tariff of the doubled frame before any construction search.", + "blocked_by": "No doubled-frame native implementation, physical caller or complete paid/target invoice is supplied." + } + ], + "question_source": { + "pr": 6148, + "author": "CubeJerry", + "question": "Open next question 2: four calls in the odd coset", + "source_head": "d2cba5a85ff80532661f9370700abe6c3678aaf9" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358875", + "baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY at selected6030; source orientation only, no scientific replay." +} diff --git a/research/bit-four-use-alternating-descent/VERIFY.json b/research/bit-four-use-alternating-descent/VERIFY.json new file mode 100644 index 0000000000..0bf3188af5 --- /dev/null +++ b/research/bit-four-use-alternating-descent/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": 120, + "checks": "All 20807 ordered projector pairs, exact odd coefficients, full matrix/column agreement, coarse factors, noncommuting proper-block example and invalid inputs." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the full scientific domain and semantic rejections with Python assertions disabled." + } + ] +} diff --git a/research/bit-four-use-alternating-descent/verify.py b/research/bit-four-use-alternating-descent/verify.py new file mode 100644 index 0000000000..496a25fb66 --- /dev/null +++ b/research/bit-four-use-alternating-descent/verify.py @@ -0,0 +1,262 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of alternating four-call lattice descent.""" + +import hashlib +import itertools +import json +from pathlib import Path +import platform +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def field_table(q): + require(q in (2, 4, 8), "field must be F2, F4 or F8") + modulus = {2: 3, 4: 7, 8: 11}[q] + degree = q.bit_length() - 1 + rows = [] + for a in range(q): + row = [] + for b in range(q): + value, x = 0, a + for bit in range(degree): + if (b >> bit) & 1: + value ^= x + x <<= 1 + if x & q: + x ^= modulus + row.append(value) + rows.append(tuple(row)) + table = tuple(rows) + for a, b, c in itertools.product(range(q), repeat=3): + require(table[a][b] == table[b][a], "field commutativity") + require(table[a][table[b][c]] == table[table[a][b]][c], "associativity") + require(table[a][b ^ c] == table[a][b] ^ table[a][c], "distributivity") + for a in range(1, q): + require(table[a][1] == a and 1 in table[a], "field unit/inverse") + return table + + +def identity(n): + return tuple(int(i == j) for i in range(n) for j in range(n)) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b, strict=True)) + + +def scale(a, coefficient, table): + return tuple(table[coefficient][x] for x in a) + + +def multiply(a, b, n, table): + out = [0] * (n * n) + for i, j, k in itertools.product(range(n), repeat=3): + out[n * i + j] ^= table[a[n * i + k]][b[n * k + j]] + return tuple(out) + + +def trace(a, n): + value = 0 + for i in range(n): + value ^= a[n * i + i] + return value + + +def rank(a, n, table): + rows = [list(a[i * n:(i + 1) * n]) for i in range(n)] + pivot = 0 + for column in range(n): + candidates = [i for i in range(pivot, n) if rows[i][column]] + if not candidates: + continue + selected = candidates[0] + rows[pivot], rows[selected] = rows[selected], rows[pivot] + inverse = table[rows[pivot][column]].index(1) + rows[pivot] = [table[inverse][x] for x in rows[pivot]] + for i in range(n): + if i != pivot and rows[i][column]: + coefficient = rows[i][column] + rows[i] = [x ^ table[coefficient][y] + for x, y in zip(rows[i], rows[pivot], strict=True)] + pivot += 1 + return pivot + + +def validate_projector(p, n, table): + require(1 <= n <= 4 and len(p) == n * n, "projector shape") + require(all(isinstance(x, int) and 0 <= x < len(table) for x in p), + "projector field entries") + require(multiply(p, p, n, table) == p, "projector idempotence") + require(rank(p, n, table) == 1, "projector rank one") + + +def projectors(n, table): + q = len(table) + require(1 <= n <= 4 and q ** n <= 256, "projector enumeration capacity") + vectors = tuple(itertools.product(range(q), repeat=n)) + out = [] + for u in vectors: + nonzero = [x for x in u if x] + if not nonzero or nonzero[0] != 1: + continue + for v in vectors: + pairing = 0 + for x, y in zip(u, v, strict=True): + pairing ^= table[x][y] + if pairing == 1: + p = tuple(table[x][y] for x in u for y in v) + validate_projector(p, n, table) + out.append(p) + expected = (q ** n - 1) * q ** (n - 1) // (q - 1) + require(len(out) == len(set(out)) == expected, "complete projector list") + return tuple(out) + + +def polynomial_product(a, b, n, table): + require(len(a) + len(b) <= 6, "polynomial degree capacity") + zero = (0,) * (n * n) + out = [zero] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + out[i + j] = add(out[i + j], multiply(x, y, n, table)) + return tuple(out) + + +def word(ps, n, table): + require(len(ps) <= 4, "word length capacity") + result = (identity(n),) + for p in ps: + result = polynomial_product(result, (add(identity(n), p), p), n, table) + return result + + +def column_interpreter(ps, n, table): + """Act on basis columns without polynomial matrix multiplication.""" + require(len(ps) <= 4, "column interpreter length capacity") + matrices = [[0] * (n * n) for _ in range(len(ps) + 1)] + for column in range(n): + coefficients = [tuple(int(i == column) for i in range(n))] + for p in reversed(ps): + following = [[0] * n for _ in range(len(coefficients) + 1)] + for degree, vector in enumerate(coefficients): + projected = [0] * n + for i, j in itertools.product(range(n), repeat=2): + projected[i] ^= table[p[n * i + j]][vector[j]] + for i in range(n): + following[degree][i] ^= vector[i] ^ projected[i] + following[degree + 1][i] ^= projected[i] + coefficients = [tuple(v) for v in following] + for degree, vector in enumerate(coefficients): + for row, value in enumerate(vector): + matrices[degree][n * row + column] = value + return tuple(tuple(m) for m in matrices) + + +def check_pair(p, q, n, table): + endpoint = word((p, q, p, q), n, table) + require(endpoint == column_interpreter((p, q, p, q), n, table), + "independent literal polynomial endpoints") + pq = multiply(p, q, n, table) + qp = multiply(q, p, n, table) + tau = trace(pq, n) + expected_odd = scale(add(p, q), tau, table) + require(endpoint[1] == endpoint[3] == expected_odd, "odd coefficient formula") + even = not any(endpoint[1]) and not any(endpoint[3]) + require(even == (p == q or tau == 0), "exact even-subalgebra criterion") + if not even: + return "not_even", endpoint + first, second = (p, p) if p == q else (add(p, pq), add(q, qp)) + validate_projector(first, n, table) + validate_projector(second, n, table) + coarse = word((first, second), n, table) + zero = (0,) * (n * n) + require(endpoint == (coarse[0], zero, coarse[1], zero, coarse[2]), + "two coarse-label calls reproduce every coefficient") + if p == q: + return "equal", endpoint + require(not any(multiply(first, second, n, table)), "coarse orthogonality") + require(not any(multiply(second, first, n, table)), "reverse orthogonality") + require(rank(add(first, second), n, table) == 2, "coarse rank two") + return "orthogonal" if pq == qp else "noncommuting", endpoint + + +def rejected_projector(p, n, table, expected): + try: + validate_projector(p, n, table) + except ValueError as error: + require(str(error) == expected, "wrong projector rejection reason") + return + raise ValueError("invalid projector accepted") + + +def controls(): + table, n = field_table(2), 2 + p, q = (1, 0, 0, 0), (0, 1, 0, 1) + zero = (0,) * 4 + endpoint = word((p, q, p, q), n, table) + require(endpoint == (zero, zero, identity(n), zero, zero), + "noncommuting even witness") + require(multiply(p, q, n, table) != multiply(q, p, n, table), + "commuting-only mutation rejected") + require(p != q, "equal-projector-only mutation rejected") + proper = 0 + for length in (1, 2, 3): + for start in range(5 - length): + subword = (p, q, p, q)[start:start + length] + result = word(subword, n, table) + require(any(any(result[i]) for i in range(1, len(result), 2)), + "proper consecutive block must not be even") + proper += 1 + bare = word((p, q), n, table) + require(endpoint != (bare[0], zero, bare[1], zero, bare[2]), + "omitting cross-term correction rejected") + require(endpoint != word((p, q, p, p), n, table), "changed fourth call rejected") + rejected_projector((0, 1, 0, 0), n, table, "projector idempotence") + rejected_projector(identity(n), n, table, "projector rank one") + rejected_projector((0, 0, 0, 0), n, table, "projector rank one") + rejected_projector((1,), n, table, "projector shape") + rejected_projector((2, 0, 0, 0), n, table, "projector field entries") + try: + field_table(3) + except ValueError as error: + require(str(error) == "field must be F2, F4 or F8", "wrong field error") + else: + raise ValueError("odd characteristic accepted") + require(proper == 9, "proper subword inventory") + return {"proper_noneven_blocks": proper, "semantic_checks": 5, + "invalid_inputs": 6} + + +def main(): + require(len(sys.argv) == 1, "no command-line arguments are supported") + rows, digest = [], hashlib.sha256() + for field_size, n in ((2, 1), (2, 2), (2, 3), (2, 4), + (4, 1), (4, 2), (8, 1), (8, 2)): + table = field_table(field_size) + ps = projectors(n, table) + counts = dict.fromkeys(("equal", "orthogonal", "noncommuting", "not_even"), 0) + for p, q in itertools.product(ps, repeat=2): + category, endpoint = check_pair(p, q, n, table) + counts[category] += 1 + digest.update(bytes(x for matrix in endpoint for x in matrix)) + require(sum(counts.values()) == len(ps) ** 2, "pair enumeration accounting") + rows.append({"field": field_size, "width": n, "projectors": len(ps), + "pairs": len(ps) ** 2, **counts}) + folder = Path(__file__).resolve().parent + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(folder.iterdir()) if p.is_file()} + receipt = {"status": "PASS_BIT_FOUR_USE_ALTERNATING_DESCENT", "rows": rows, + "controls": controls(), "endpoint_sha256": digest.hexdigest(), + "package_sha256": hashes, "python": platform.python_version(), + "claim_type": "scoped written proof with finite corroboration", + "no_new_kappa": True} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()