diff --git a/research/all-field-permutation-rigidity/PROOF.md b/research/all-field-permutation-rigidity/PROOF.md new file mode 100644 index 0000000000..59891f76af --- /dev/null +++ b/research/all-field-permutation-rigidity/PROOF.md @@ -0,0 +1,171 @@ +# Every shortest single-permutation word has one scalar projector + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let K be any field, n>=2, and R>=1. Let w be a nonidentity element of S_n +and let E in M_R(K) satisfy E^2=E and rank E=1. Work in the full formal +group algebra M_R(K[S_n]), with products acting on columns, rightmost first. +The endpoint is + + T = I + ([w]-[e]) E. + +A normalized paid factor is + + D_s(N) = I + ([s]-[e]) N, + +where s is a simple adjacent transposition, N^2=N, and rank N=1. +Every register has arbitrary entrance data. Equality means equality of all +formal coefficients, including the return of all dirty spectators. Arbitrary +scalar GL_R(K) operations may occur between paid factors. + +**Theorem.** The minimum paid length is inv(w). In every normalized word of +this length, every paid coupling is exactly E and the label sequence is a +reduced expression for w. Conversely, every reduced expression for w, with +E at every call, attains the endpoint. + +This is a scoped algebraic proof, with finite corroboration. The theorem +does not price physical scalar mixing or construct a native supplier. + +## What is inherited + +Brian's PR4765 proves tight spectator elimination over F2 for the S4 +ordered-pair module. Its Grassmann equality argument is the proof method +used below. Ross Richardson's PR1989 supplies the ordered-pair cut for +symmetric groups and the binary inversion tariff, retaining Adam Gall's +cut-method credit. Nick Petalas's PR4851 already proves the length-three S3 +single-target rigidity theorem over every field, even with a larger scalar +coupling alphabet. That special case is inherited. + +The new statement is the all-field, all-S_n single-target equality +classification in the stated idempotent alphabet. We prove the finite +ordered-pair geometry directly, rather than replaying predecessor searches. +No literature-priority claim is made. + +## Normalize and choose the active line + +Move each scalar GL_R(K) map through its neighboring paid factor by +conjugation. This preserves projector rank and idempotence. Augmentation, +which sends every [g] to 1, sends the endpoint and every paid factor to I. +It therefore forces the residual free scalar map to be I. The normalized +word has only the displayed paid factors. + +Write A=im E and S=ker E, so K^R=A direct sum S. The endpoint acts by w +on A and by identity on S. This basis choice is only for the proof. The +conclusion in the original basis will be N=E. If R=1, S is zero and every +rank-one idempotent is already E=I; the argument also covers this case. + +## Ordered-pair geometry over K + +Let U have basis e_(a,b) for distinct a,b in {1,...,n}. The action of g sends +e_(a,b) to e_(g(a),g(b)); these are formal basis labels over K. Put + + U+ = span{e_(a,b): ab}, + V = K^R tensor U, H = K^R tensor U+. + +This is a representation of the group algebra over every field. No ordering +or positivity is imposed on K, and the geometric labels are not identified +in characteristic two. Representation equality is used only as a necessary +consequence of the full formal endpoint. + +For an invertible represented matrix P define + + phi(P) = rank(pi_(K^R tensor U-) P|_H) + = dim H - dim(H intersect P^(-1)H). + +The second equality is rank-nullity. Both subspaces in the intersection +have dimension dim H. For equal-dimensional subspaces X,Y set + + d(X,Y) = dim X - dim(X intersect Y). + +This is an invertible-map-invariant metric. If X,Y,Z all have dimension k +and d(X,Z)=d(X,Y)+d(Y,Z), then + + X intersect Z subset Y subset X+Z. (1) + +Indeed, set a=dim(X intersect Y), b=dim(Y intersect Z), +c=dim(X intersect Z), and t=dim(X intersect Y intersect Z). The inclusions +(X intersect Y)+(Y intersect Z) subset Y and the inequality t<=c give +a+b-t<=k and a+b<=k+c. This proves the triangle inequality. Equality forces +t=c and dim((X intersect Y)+(Y intersect Z))=k, proving both inclusions in +(1). This is the inherited Grassmann equality lemma over an arbitrary field. + +The crossing block of a permutation has one independent column for each +inversion. Consequently phi(T)=inv(w), since E has one-dimensional image. + +For a simple s=(i,i+1), put alpha=e_(i,i+1), beta=e_(i+1,i), and let +H_other be the span of the remaining positive ordered-pair basis vectors. +The simple transposition permutes those remaining positive vectors. +Write N=u v with v(u)=1. On ker v the paid factor is identity, and on +span u it acts by s. Thus G=D_s(N) is invertible, G^2=I, and + + GH = (K^R tensor H_other) + direct sum (ker v tensor span alpha) + direct sum (span u tensor span beta). (2) + +It follows that d(H,GH)=phi(G)=1. These statements use idempotence and hold +unchanged in every characteristic. + +## Tight peeling forces both scalar sides onto A + +Suppose an invertible represented P fixes S tensor U pointwise and preserves +A tensor U, and suppose a right peel satisfies phi(PG)=phi(P)-1. +Put X=H, Y=GH, and Z=P^(-1)H. Since G is an involution, + + phi(PG)=d(H,G P^(-1)H)=d(GH,P^(-1)H)=d(Y,Z). + +The hypothesis is equality in the triangle inequality, so (1) applies. +Since P is the identity on S tensor U, + + S tensor U+ subset X intersect Z, + X+Z subset (A tensor U) direct sum (S tensor U+). (3) + +By (2), u tensor beta lies in Y. The second inclusion in (1) and (3) forces +the spectator part of u to vanish. Thus u is in A. For every x in S, +x tensor alpha lies in X intersect Z and hence in Y. In (2) every alpha +coefficient lies in ker v. Therefore v(x)=0 for every x in S. + +Both sides matter: N has image in A and annihilates S. Because A is a +line and N is a nonzero idempotent, N acts as identity on A. Hence N=E. +This conclusion is about the full scalar coupling, not only its image in +the ordered-pair representation. Therefore the full formal factor fixes +every spectator exactly. + +## Every peel in a shortest word is tight + +For invertible represented P,Q, the triangle inequality and its invariance +give phi(PQ)<=phi(P)+phi(Q). Every paid factor has phi=1, so any m-factor +word with endpoint T satisfies m>=inv(w). + +If m=inv(w), let P be the product of any initial j written factors. +Subadditivity gives phi(P)<=j and phi(T)<=phi(P)+(m-j), forcing phi(P)=j. +Starting at T, removing the rightmost written factor therefore drops phi +by one. The tight-peeling argument forces that factor's coupling to be E. +Its removal leaves a full formal endpoint acting only on A and fixing S. +Apply the same argument to the next peel. Induction forces all couplings +to be E. There is no bound on R in this reasoning. + +With common projector E, the full formal product is + + I + ([s_1 ... s_m]-[e]) E. + +Distinct permutations are distinct group-algebra basis elements, so formal +equality with T implies s_1 ... s_m=w. Its length m=inv(w) makes the +expression reduced. Finally, adjacent sorting gives a reduced expression +of length inv(w), and using E at every factor gives the displayed endpoint. +This proves the lower bound, rigidity and converse. + +## Scope boundaries + +The theorem requires a single active line, adjacent labels, rank-one +idempotents, the exact full endpoint and minimum unweighted length. Inserting +a mixed factor and its inverse creates a longer valid word using spectators. +Allowing the whole target permutation as a paid label can realize T in one +call. The verifier checks these boundaries. Higher-rank targets, nonidempotent +couplings and arbitrary separate generator prices are not classified here. + +Finite checks corroborate the written proof and do not establish its universal +quantifiers by enumeration. Independent human and formal proof-kernel review +are unclaimed. Native hosting, precision, tape, recursive invoices, supplier +admission and the complete multiplication theorem remain outside scope. diff --git a/research/all-field-permutation-rigidity/README.md b/research/all-field-permutation-rigidity/README.md new file mode 100644 index 0000000000..6b72eeba96 --- /dev/null +++ b/research/all-field-permutation-rigidity/README.md @@ -0,0 +1,133 @@ +# Shortest single-permutation circuits are rigid over every field + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with exact finite corroboration; no new kappa.** For every +field K, every n>=2 and every finite register count R, consider the exact +formal endpoint + + I + ([w]-[e]) E in M_R(K[S_n]), + +where w is a nonidentity permutation and E is a rank-one idempotent. Paid +calls use simple adjacent transpositions and rank-one scalar idempotents. +Arbitrary scalar GL_R(K) mixing is free, all inputs are arbitrary, and every +dirty spectator must return exactly. + +The minimum is inv(w). More precisely, **every normalized minimum-length +word uses E at every paid call**, and its labels form a reduced expression +for w. Thus complex or odd-characteristic scalar mixing cannot move the +active line or use dirty spectators in a shortest word of this alphabet. + +[PROOF.md](PROOF.md) gives the written all-parameter argument. The new step +extends Brian's binary S4 tight-peeling geometry to all coefficient fields +and all symmetric groups, then derives the single-line equality +classification. Ross Richardson's binary inversion tariff and Nick Petalas's +all-field three-call S3 special case are credited predecessor results. +Neither is a new result of this package, and neither executable is replayed. + +## Evidence and reproduction + +The first working example is w=3412 in one-based notation, with four +inversions. A rational three-register projector is + + E = (1,2,1)^T (1,1,0) / 3. + +The same E at the four adjacent calls realizes the complete formal target. +Its two-dimensional kernel is arbitrary dirty workspace and is restored. +The faithful regular-action check includes every input column. + +The standard-library verifier enumerates 18,792 one-step S4 peeling cases +over F3. The two-register domain uses all 12 rank-one idempotents as both +endpoint and call projector. The three-register domain fixes endpoint E00 +and tests all 117 rank-one idempotent call projectors. Exactly 468 peels +lower the cut, and each uses the endpoint projector and a right descent. +It also checks 46 complete nonidentity S4 endpoints over Q and F3 on +2,760 regular-action basis columns, four call omissions, four changed +projectors and three boundary controls. These are finite corroboration of +the written proof, not enumeration of its universal quantifiers. + +From the repository root with CPython 3.12 and no dependencies: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/all-field-permutation-rigidity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/all-field-permutation-rigidity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/all-field-permutation-rigidity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/all-field-permutation-rigidity --check-source-history +``` + +Other installations can substitute their CPython 3.12 executable. Direct +runs are read-only and print a generated JSON receipt with the marker +`PASS_ALL_FIELD_PERMUTATION_RIGIDITY`, enumerated counts and SHA256 hashes +of all six package files. There is no handwritten receipt or expected +output file. The registered ordinary and optimized runs enable warnings +as errors. Sources are pinned as provenance, with no runtime imports. + +## Scope and credit + +The source is JoyboyBrian / Brian's +[PR4765](https://github.com/CrocSwap/integer-mult-bounds/pull/4765), whose +Grassmann equality and tight spectator elimination are the main predecessor +method. Credit RossRichardson / Ross Richardson's +[PR1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989) for the +ordered-pair cut and binary inversion tariff, retaining Adam Gall / PR1941 +and the cited cut lineage. Nick Petalas's +[PR4851](https://github.com/CrocSwap/integer-mult-bounds/pull/4851) already +settles the S3 length-three special case over every field, including a +larger nonidempotent coupling alphabet. The register-model lineage retains +eumemic / PR288, Ali Romman / PR468, Gareth Davidson / PR1333 and the +predecessor credits. No literature-priority claim is made. + +Scientific base is canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected +PR6030 with conditional kappa 0.003125804. The card's source-binding first +example passed and was not a scientific replay. This changes +`bit-new-register-model` to a formal equality obstruction with a changed +coefficient-field and symmetric-group scope. Its native-supplier acceptance +gate remains unmet. The +[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362405) +records that scope. Work stopped at the first verified result. + +The initial overlap check read current open PRs, this account's latest 200 +PRs, active Discussions and recent handoffs, merged theorem searches and +all main READMEs for the distinctive rigidity/field/permutation terms. +The cached card report covered 389 open PRs and 6,322 Discussion records; +only 120 of 8,917 local notes were searched by that helper. Main-tree +searches supplemented the sparse coverage. Arbitrary historical diffs and +unpublished work remain outside the check. No-match searches do not prove +novelty. [SOURCES.json](SOURCES.json) pins the credited proof sources. + +The theorem classifies minimum unweighted length with a single active +line and idempotent calls. It does not classify higher-rank targets, +nonidempotent couplings, unequal generator prices or non-simple labels. +Native implementation, paid scalar work, compiler/hosting, precision, tape, +stock, recursive invoices and supplier admission are outside scope. No +selected-frontier change, complete multiplication theorem, selected cold +replay, Lean or Docker run is claimed. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +For a rank-two endpoint projector over a nonbinary field, which normalized +minimum-length words are possible inside its active plane? Tight peeling +still motivates restricting attention to that plane, but the one-dimensional +idempotence conclusion used here is unavailable. A first step is one S4 +endpoint and an exact two-dimensional coefficient calculation. No equality +classification or physical price for that changed target is supplied here. + +## Verifier bounds + +The verifier has no recursion, subprocesses, network access or external +mutable state. Its call graph is acyclic. All enumerations use fixed finite +domains: S4, F3 vectors of length at most three, words of length at most +eight and matrices of order at most 18 for crossing ranks. Each function +fits within sixty physical lines. Explicit exception checks remain active +under optimized Python. + +Python allocates tuples, dictionaries and arbitrary-size rational integers +dynamically. This is a managed-runtime deviation from fixed allocation, +confined to the bounded finite verifier. A formal state has at most 24 +coefficient matrices of order at most three; a regular-action vector has +at most 72 coordinates. Exact arithmetic on this fixed fixture is bounded +by the finite operations; no arbitrary input or real-time memory guarantee +is claimed. Normal and optimized warning-strict replay are the available +diagnostics. No shared diagnostic configuration changes. diff --git a/research/all-field-permutation-rigidity/SOURCES.json b/research/all-field-permutation-rigidity/SOURCES.json new file mode 100644 index 0000000000..4b6d22ae50 --- /dev/null +++ b/research/all-field-permutation-rigidity/SOURCES.json @@ -0,0 +1,48 @@ +{ + "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/all-field-s3-shortest-rigidity/README.md", + "usage": "provenance", + "git_blob": "b486d63785f2e3e033ad6e00f4d31b5149e2ea5c", + "sha256": "633667ff74e2365e64fbd16826d828da29e3d205c9bb6785754cb01b8f5356a1" + }, + { + "path": "research/s4-tight-word-spectator-elimination/PROOF.md", + "usage": "provenance", + "git_blob": "4c3d129001e3976a64c5c58bd55bcd2a93a71781", + "sha256": "b2270221efb0f666225c28a8b5d16e0bc561672cf96af1263b57e32dcfe1e842" + }, + { + "path": "research/s4-tight-word-spectator-elimination/README.md", + "usage": "provenance", + "git_blob": "8db05b993afe33649afd549f779c613a141806dc", + "sha256": "74f218e5cb2a28986b5db53ede7da419df5d719cd7c3bca0c955a354a24d92c4" + }, + { + "path": "research/symmetric-adjacent-cut-bound/PROOF.md", + "usage": "provenance", + "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d", + "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50" + }, + { + "path": "research/symmetric-adjacent-cut-bound/README.md", + "usage": "provenance", + "git_blob": "cdb3f431acc07b4a75abdd3998093fd68d9a498f", + "sha256": "4fb453c83d7cd15a93fc7c65b82f2f67cb609a31285ac9ebd1f44b675777d154" + } + ] +} diff --git a/research/all-field-permutation-rigidity/TASK.json b/research/all-field-permutation-rigidity/TASK.json new file mode 100644 index 0000000000..9380dd5e06 --- /dev/null +++ b/research/all-field-permutation-rigidity/TASK.json @@ -0,0 +1,64 @@ +{ + "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": "All-field all-S_n equality classification for minimum adjacent-transposition words realizing I+([w]-1)E with rank-one idempotent E and arbitrary finite restored dirty workspace.", + "scope_change_reason": "Change the coefficient field and replace a native-supplier search by a single-active-line shortest-word obstruction. Binary S4 tight peeling and the all-field three-call S3 case are credited premises and comparisons, not replay deliverables.", + "bottleneck_link": "Side result for the BIT interface: scalar mixing over arbitrary fields cannot provide a changed helper trajectory in a minimum-length simple-permutation single-line word. Native realization and the complete recursive bill remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and exactly corroborated equality obstruction; do not extend the alphabet or target rank.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-parameter proof. verify.py enumerates 18,792 ternary peels with 468 decreasing cases and checks 46 formal/regular endpoints on 2,760 basis columns plus 11 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Classify rank-two endpoint minimum words over a nonbinary coefficient field.", + "why_it_matters": "The active-plane coupling need not equal the endpoint projector, so the present one-line obstruction does not apply.", + "first_step": "Fix one S4 endpoint and calculate its exact two-dimensional coefficient equations.", + "blocked_by": "No equality classification or native price for the rank-two contract is supplied." + } + ] +} diff --git a/research/all-field-permutation-rigidity/VERIFY.json b/research/all-field-permutation-rigidity/VERIFY.json new file mode 100644 index 0000000000..8bf9835977 --- /dev/null +++ b/research/all-field-permutation-rigidity/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Written-proof finite corroboration: all 18,792 F3 peels, rational/formal/regular endpoints and boundary controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same exact coverage with optimized Python; all exception checks remain active." + } + ] +} diff --git a/research/all-field-permutation-rigidity/verify.py b/research/all-field-permutation-rigidity/verify.py new file mode 100644 index 0000000000..520b0b31f9 --- /dev/null +++ b/research/all-field-permutation-rigidity/verify.py @@ -0,0 +1,273 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written all-field permutation theorem. + +Produced by Nick Petalas. Apache-2.0. No files are written. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def scalar(value, prime): + return value % prime if prime else Fraction(value) + + +def identity(size): + return tuple(tuple(int(i == j) for j in range(size)) for i in range(size)) + + +def plus(left, right, prime, sign=1): + return tuple(tuple(scalar(a + sign * b, prime) for a, b in zip(x, y, strict=True)) + for x, y in zip(left, right, strict=True)) + + +def times(left, right, prime): + size = len(left) + return tuple(tuple(scalar(sum(left[i][k] * right[k][j] for k in range(size)), prime) + for j in range(size)) for i in range(size)) + + +def compose(left, right): + return tuple(left[j] for j in right) + + +def inversions(word): + return sum(word[i] > word[j] for i in range(len(word)) for j in range(i + 1, len(word))) + + +def adjacent(size): + result = [] + for i in range(size - 1): + value = list(range(size)) + value[i], value[i + 1] = value[i + 1], value[i] + result.append(tuple(value)) + return tuple(result) + + +def rank(matrix, prime): + work = [list(row) for row in matrix] + height, width = len(work), len(work[0]) + pivot = 0 + for column in range(width): + selected = next((i for i in range(pivot, height) if work[i][column]), None) + if selected is None: + continue + work[pivot], work[selected] = work[selected], work[pivot] + value = work[pivot][column] + inverse = pow(value, -1, prime) if prime else 1 / Fraction(value) + work[pivot] = [scalar(x * inverse, prime) for x in work[pivot]] + for row in range(pivot + 1, height): + coefficient = work[row][column] + if coefficient: + work[row] = [scalar(x - coefficient * y, prime) + for x, y in zip(work[row], work[pivot], strict=True)] + pivot += 1 + if pivot == height: + break + return pivot + + +def projectors(size, prime): + need(size in (2, 3) and prime == 3, "unsupported exhaustive projector domain") + vectors = tuple(product(range(prime), repeat=size)) + result = set() + for u in vectors: + for v in vectors: + if sum(a * b for a, b in zip(u, v, strict=True)) % prime == 1: + result.add(tuple(tuple(a * b % prime for b in v) for a in u)) + for matrix in result: + need(times(matrix, matrix, prime) == matrix, "projector idempotence") + need(rank(matrix, prime) == 1, "projector rank") + return tuple(sorted(result)) + + +def accumulate(coefficients, label, matrix, prime): + size = len(matrix) + zero = tuple((0,) * size for _ in range(size)) + value = plus(coefficients.get(label, zero), matrix, prime) + if any(any(row) for row in value): + coefficients[label] = value + else: + coefficients.pop(label, None) + + +def formal_word(labels, couplings, prime): + need(1 <= len(labels) <= 8 and len(labels) == len(couplings), "word bounds") + size = len(couplings[0]) + unit = identity(size) + result = {tuple(range(len(labels[0]))): unit} + for label, coupling in zip(labels, couplings, strict=True): + updated = {} + complement = plus(unit, coupling, prime, -1) + for old, matrix in result.items(): + accumulate(updated, old, times(matrix, complement, prime), prime) + accumulate(updated, compose(old, label), times(matrix, coupling, prime), prime) + result = updated + return result + + +def target(word, projector, prime): + result = {} + accumulate(result, tuple(range(len(word))), plus(identity(len(projector)), projector, prime, -1), prime) + accumulate(result, word, projector, prime) + return result + + +def crossing(coefficients, size, prime): + first = next(iter(coefficients)) + positive = tuple((i, j) for i in range(len(first)) for j in range(i + 1, len(first))) + negative = tuple((j, i) for i, j in positive) + index = {pair: j for j, pair in enumerate(negative)} + width = len(positive) + result = [[0] * (size * width) for _ in range(size * width)] + for word, matrix in coefficients.items(): + for column, (a, b) in enumerate(positive): + row = index.get((word[a], word[b])) + if row is not None: + for i in range(size): + for j in range(size): + result[i * width + row][j * width + column] += matrix[i][j] + return rank(tuple(tuple(scalar(x, prime) for x in row) for row in result), prime) + + +def peel(word, endpoint, coupling, label, prime): + size = len(coupling) + unit = identity(size) + ec = plus(unit, endpoint, prime, -1) + nc = plus(unit, coupling, prime, -1) + result = {} + for group, matrix in ( + (tuple(range(len(word))), times(ec, nc, prime)), + (label, times(ec, coupling, prime)), + (word, times(endpoint, nc, prime)), + (compose(word, label), times(endpoint, coupling, prime)), + ): + accumulate(result, group, matrix, prime) + return crossing(result, size, prime) + + +def check_peels(): + counts = {"peels": 0, "decreasing_peels": 0} + words = tuple(permutations(range(4))) + for size in (2, 3): + pool = projectors(size, 3) + need(len(pool) == (12 if size == 2 else 117), "projector domain size") + endpoints = pool if size == 2 else (tuple(tuple(int(i == j == 0) for j in range(size)) + for i in range(size)),) + counts[f"projectors_F3_r{size}"] = len(pool) + for endpoint in endpoints: + for word in words: + length = inversions(word) + need(crossing(target(word, endpoint, 3), size, 3) == length, "target cut") + for coupling in pool: + for label in adjacent(4): + after = peel(word, endpoint, coupling, label, 3) + expected = coupling == endpoint and inversions(compose(word, label)) == length - 1 + need((after == length - 1) == expected, "one-step rigidity") + need(abs(after - length) <= 1, "one-step distance bound") + counts["peels"] += 1 + counts["decreasing_peels"] += int(after == length - 1) + return counts + + +def reduced_word(word): + value = word + peels = [] + for _ in range(inversions(word)): + label = next(label for label in adjacent(len(word)) + if inversions(compose(value, label)) == inversions(value) - 1) + peels.append(label) + value = compose(value, label) + need(value == tuple(range(len(word))), "sorting termination") + return tuple(reversed(peels)) + + +def regular_column(labels, couplings, prime, initial): + state = {initial: scalar(1, prime)} + for label, coupling in reversed(tuple(zip(labels, couplings, strict=True))): + updated = dict(state) + for (column, word), value in state.items(): + for row in range(len(coupling)): + delta = coupling[row][column] * value + same, shifted = (row, word), (row, compose(label, word)) + updated[same] = scalar(updated.get(same, 0) - delta, prime) + updated[shifted] = scalar(updated.get(shifted, 0) + delta, prime) + state = {key: value for key, value in updated.items() if value} + return state + + +def check_regular(labels, couplings, word, endpoint, prime): + columns = 0 + for group in permutations(range(len(word))): + for column in range(len(endpoint)): + expected = regular_column((word,), (endpoint,), prime, (column, group)) + observed = regular_column(labels, couplings, prime, (column, group)) + need(observed == expected, "faithful regular endpoint") + columns += 1 + return columns + + +def check_constructions(): + rational = tuple(tuple(Fraction(a * b, 3) for b in (1, 1, 0)) for a in (1, 2, 1)) + need(times(rational, rational, 0) == rational and rank(rational, 0) == 1, "rational projector") + columns, endpoints = 0, 0 + for prime, endpoint in ((0, rational), (3, projectors(2, 3)[4])): + for word in permutations(range(4)): + if not inversions(word): + continue + labels = reduced_word(word) + couplings = (endpoint,) * len(labels) + need(formal_word(labels, couplings, prime) == target(word, endpoint, prime), "formal endpoint") + columns += check_regular(labels, couplings, word, endpoint, prime) + endpoints += 1 + return {"complete_endpoints": endpoints, "regular_basis_columns": columns} + + +def check_controls(): + word = (2, 3, 0, 1) + endpoint = ((1, 0), (0, 0)) + other = ((0, 0), (0, 1)) + mixed = ((1, 1), (0, 0)) + labels = reduced_word(word) + need(len(labels) == 4, "first working example length") + wanted = target(word, endpoint, 3) + omissions = replacements = 0 + for i in range(len(labels)): + short = labels[:i] + labels[i + 1:] + need(formal_word(short, (endpoint,) * len(short), 3) != wanted, "omission control") + changed = tuple(other if j == i else endpoint for j in range(len(labels))) + need(formal_word(labels, changed, 3) != wanted, "wrong-projector control") + omissions += 1 + replacements += 1 + extended = (adjacent(4)[0],) * 2 + labels + couplings = (mixed, mixed) + (endpoint,) * len(labels) + need(formal_word(extended, couplings, 3) == wanted, "nonminimal mixed-word boundary") + need(mixed != endpoint, "nonminimal word really uses a spectator") + need(formal_word((word,), (endpoint,), 3) == wanted, "nonsimple-label boundary") + need(formal_word(labels, (other,) * len(labels), 3) != wanted, "full-endpoint boundary") + return {"omission_controls": omissions, "projector_replacements": replacements, + "boundary_controls": 3} + + +def main(): + counts = check_peels() + counts.update(check_constructions()) + counts.update(check_controls()) + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + print(json.dumps({"status": "PASS_ALL_FIELD_PERMUTATION_RIGIDITY", "counts": counts, + "claim_type": "scoped written proof with finite corroboration", + "source_sha256": hashes, "new_kappa": False}, sort_keys=True)) + + +if __name__ == "__main__": + main()