From cba0d9a40f4815716594d235590b469cfeaa7da0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 12:12:28 +0000 Subject: [PATCH] feat(research): count width-two projector word symmetry orbits --- research/projector-word-symmetry/PROOF.md | 200 +++++++++++ research/projector-word-symmetry/README.md | 143 ++++++++ research/projector-word-symmetry/SOURCES.json | 30 ++ research/projector-word-symmetry/TASK.json | 78 ++++ research/projector-word-symmetry/VERIFY.json | 34 ++ research/projector-word-symmetry/verify.py | 335 ++++++++++++++++++ 6 files changed, 820 insertions(+) create mode 100644 research/projector-word-symmetry/PROOF.md create mode 100644 research/projector-word-symmetry/README.md create mode 100644 research/projector-word-symmetry/SOURCES.json create mode 100644 research/projector-word-symmetry/TASK.json create mode 100644 research/projector-word-symmetry/VERIFY.json create mode 100644 research/projector-word-symmetry/verify.py diff --git a/research/projector-word-symmetry/PROOF.md b/research/projector-word-symmetry/PROOF.md new file mode 100644 index 0000000000..c628dc4dd7 --- /dev/null +++ b/research/projector-word-symmetry/PROOF.md @@ -0,0 +1,200 @@ +# Exact symmetry quotients for odd projector words + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let K=F_q be any finite field. Let X be the rank-one idempotents of +M_2(K), and put n=q(q+1). For an odd positive integer k=2m+1, consider +ordered tuples (N_1,...,N_k) in X^k. The following transformations act on +these tuples: + +1. Simultaneous conjugation C_S by a monomial invertible two by two matrix + S, with scalar multiples identified. +2. R(N_1,...,N_k)=(N_k^T,...,N_1^T). + +Write epsilon=0 in characteristic two and epsilon=1 otherwise. The number +of orbits under the group generated by these transformations is exactly + +\[ + \boxed{\frac{n^{2m+1} + +2^{2m+1}\left(q-2+\epsilon\frac{q-1}{2}\right) + +(q-1)(q+\epsilon)n^m}{4(q-1)}}. \tag{1} +\] + +The term containing epsilon is zero in characteristic two. For k=5 the +orbit counts at q=2,3,4,5 are respectively 1,962; 31,256; 267,072; and +1,520,110. These counts are exact for this declared action. No maximal +symmetry group or minimal possible search domain is asserted. + +The action preserves the *universal diagonal-pair existence problem* in +JoyboyBrian's PR6097 and Josie Elliston's PR6137. One representative per +orbit therefore suffices when searching all groups and label sets for a +width-two word of this length with distinct diagonal targets, each of +label length at least three. It also preserves their coefficient-class +collision relaxation. This is a search reduction, not a proof that the +representatives refute, and not a new six-call lower bound over any field. + +## Why these are safe transformations + +For a group G and g in a label set L, write + +\[ + D_N(g)=(I-N)+[g]N\quad\hbox{in }M_2(K[G]). +\] + +The universal target family is diag([a],[b]), where a and b are distinct +and neither is a product of at most two labels in L. A monomial S either +fixes E_00,E_11 separately or exchanges them. Thus + +\[ + S D_N(g) S^{-1}=D_{SNS^{-1}}(g) +\] + +preserves the target family, exchanging a,b in the second case. All +coefficients of the endpoint identity transform, so arbitrary dirty input +coordinates remain covered. A general scalar change of basis need not +preserve this diagonal target pattern. This is why the quotient uses its +monomial normalizer rather than all of GL_2(K). + +There is an anti-isomorphism from M_2(K[G]) to M_2(K[G^op]) that transposes +the scalar matrices and keeps the named group elements. It reverses the +order of a product. Consequently an identity with projectors N_1,...,N_k +becomes an identity with N_k^T,...,N_1^T and labels g_k,...,g_1 over G^op. +The target is still diagonal. The set of group elements expressible by at +most two labels is unchanged: a length-two product in G^op is the reversed +product in G, and every ordered pair from L is allowed. Distinctness is +unchanged too. Applying the transformation twice returns the original +identity. Thus existence in this universal family is equivalent along R. + +This does not grant R as a symmetry of an arbitrary *fixed* oriented group, +label set and target specification without transporting that specification. +Equivalently one can identify G^op with G by inversion and transport L,a,b +to L^{-1},a^{-1},b^{-1}. A caller keeping them fixed needs extra closure. + +The collision relaxation is covariant for the same explicit reasons. +Monomial conjugation permutes the two diagonal equations and rescales or +exchanges the off-diagonal equations by nonzero scalars. It preserves their +zero class-sum constraints. Reversal sends a chronological subset +(i_1,...,i_j) to (k+1-i_j,...,k+1-i_1). It exchanges prefix and suffix +cancellation, preserves subset cardinalities, and transports target-marker +and nonidentity restrictions. Thus a feasible equality partition maps to +a feasible partition in both directions. This assertion concerns the +relaxation, not a particular branch order, node cap or proof format. + +## The finite action + +Represent the projective monomial group H by + +\[ + D_t=\begin{pmatrix}t&0\\0&1\end{pmatrix},\qquad + S_t=\begin{pmatrix}0&t\\1&0\end{pmatrix},\qquad t\in K^*. +\] + +It has order 2(q-1). Transposition gives + +\[ + R C_S R=C_{S^{-T}}. +\] + +Hence the abstract semidirect product generated by H and R has order +4(q-1), and every element is C_S or C_S R. Burnside's lemma applies to this +finite action, whether or not faithfulness is separately established. + +An idempotent in X is specified by its image line and its complementary +kernel line. There are q+1 choices for the image and q for the kernel, so +|X|=n. Equivalently it has the form + +\[ + N=\begin{pmatrix}a&b\\c&1-a\end{pmatrix},\qquad bc=a(1-a). \tag{2} +\] + +Trace one excludes both zero and the identity in every characteristic. + +## Fixed tuples without reversal + +The identity fixes all n projectors. For t!=1, a projector commuting with +D_t is diagonal, so exactly E_00,E_11 are fixed. A projector commuting +with S_t must satisfy a=1-a and b=t c. In characteristic two the first +condition is impossible. In odd characteristic, a=1/2 and (2c)^2=1/t. +There are two solutions when t is a square and none otherwise. Precisely +(q-1)/2 nonzero elements are squares in odd characteristic. + +It follows that the total number of fixed k-tuples, summed over H, is + +\[ + n^k+2^k\left(q-2+\epsilon\frac{q-1}{2}\right). \tag{3} +\] + +## Fixed tuples with reversal + +Put T_S(N)=S N^T S^{-1} and h(S)=|Fix(T_S)|. A tuple fixed by C_S R has +N_i=T_S(N_{k+1-i}), including a fixed middle projector. Also + +\[ + T_S^2(N)=(S S^{-T})N(S S^{-T})^{-1}. \tag{4} +\] + +For S=D_t, the matrix S is symmetric, so (4) is the identity. The m +paired projectors are arbitrary and the middle has h(D_t) choices. +The equation for the middle is b=t c in (2). It is the condition that the +projector is self-adjoint for the nondegenerate symmetric form with matrix +diag(1/t,1). Every nonisotropic image line has exactly one such projector, +whose kernel is its orthogonal line. Isotropic image lines have none. +The isotropic-line equation is x^2=-t y^2. In characteristic two it has +exactly one projective solution for every t, because squaring is bijective. +In odd characteristic it has two solutions for half the nonzero t and +none for the other half. Therefore + +\[ + \sum_{t\ne0}h(D_t)=q(q-1). \tag{5} +\] + +For S=S_t, direct calculation gives + +\[ + T_{S_t}(N)=\begin{pmatrix}1-a&t b\\c/t&a\end{pmatrix}. +\] + +Its fixed point condition includes 2a=1. There are no fixed projectors in +characteristic two. In odd characteristic, t!=1 forces b=c=0, which is +incompatible with bc=1/4. For t=1 there are q-1 choices, one for each +nonzero b with c=(4b)^{-1}. Since S_1 is symmetric, (4) is again the +identity. Every other S_t contributes zero, since it has no fixed middle. +Combining this with (5), the total fixed k-tuples over the reversal coset is + +\[ + n^m(q-1)(q+\epsilon). \tag{6} +\] + +Adding (3) and (6), then dividing by 4(q-1), proves (1) by Burnside's lemma. +This proves all finite fields and every odd positive k. Finite execution +below corroborates the proof; it does not replace its universal argument. + +## Canonical enumeration and its certificate + +Order X lexicographically in a declared field encoding. Encode a tuple as +the corresponding base-n integer. Its canonical representative is the +minimum of its 4(q-1) images. This minimum is unchanged along an orbit, +and two tuples have the same minimum exactly when they lie in the same +orbit. No coefficient, label or target marker may be dropped when a later +solver transports an instance to that representative. + +The standalone verifier constructs F_2,F_3,F_4,F_5,F_7,F_8,F_9 and checks +their field operations. It obtains X independently by all matrix entries +and by outer products u v^T with v^T u=1. It counts the fixed projectors +under every declared transformation and checks (1) at k=1,3,5. A separate +complete orbit enumeration covers every length-five tuple at q=2,3,4,5. +It marks each orbit in a bounded byte array, rejects intersections with +previous orbits, and requires every tuple to be covered. Its representative +digest and orbit-size histogram are generated from that enumeration. + +The verifier also expands new formal positional words coefficientwise to +check conjugation and opposite-group covariance. It rejects transpose +without reversal and a nonmonomial scalar adapter as incorrect substitutes. +These checks import no predecessor scientific code and make no decision +about whether a collision representative is feasible. + +The written theorem is a scoped algebraic proof. No independent human or +formal proof-kernel acceptance, new kappa, native implementation, complete +supplier invoice or discharge of the selected five assumptions is claimed. diff --git a/research/projector-word-symmetry/README.md b/research/projector-word-symmetry/README.md new file mode 100644 index 0000000000..20cee49c2c --- /dev/null +++ b/research/projector-word-symmetry/README.md @@ -0,0 +1,143 @@ +# Exact symmetry quotients for width-two projector words + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +This is a scoped algebraic proof with exact finite corroboration. It answers +the symmetry-reduction blocker in Open next question 1 of Josie Elliston's +[PR6137](https://github.com/CrocSwap/integer-mult-bounds/pull/6137), building on +JoyboyBrian's [PR6097](https://github.com/CrocSwap/integer-mult-bounds/pull/6097). +Their collision obstructions are cited premises, not audit or replay targets. +No predecessor scientific executable is imported or run. + +## Result + +Let X be the rank-one idempotents of M_2(F_q), n=q(q+1), k=2m+1 an odd +positive integer, and epsilon=0 for even q and 1 for odd q. Simultaneous +monomial conjugation and reversal with transpose preserve the universal +width-two diagonal-pair search family. Their action has exactly + +\[ + \frac{n^{2m+1}+2^{2m+1}\left(q-2+\epsilon\frac{q-1}{2}\right) + +(q-1)(q+\epsilon)n^m}{4(q-1)} +\] + +orbits on X^k. [PROOF.md](PROOF.md) proves the reduction, the finite-field +formula and the covariance of the coefficient-class collision relaxation. +The monomial group preserves the unordered pair of coordinate projectors. +Reversal with transpose transports the group to its opposite. A fixed +oriented group/label/target problem needs its specification transported too. + +For five calls the exact domain counts are: + +| Field | All projector tuples | Representatives under the declared action | +|---|---:|---:| +| F2 | 7,776 | 1,962 | +| F3 | 248,832 | 31,256 | +| F4 | 3,200,000 | 267,072 | +| F5 | 24,300,000 | 1,520,110 | + +The standalone verifier enumerates every tuple in this table, independently +of the fixed-point formula. It supplies a deterministic canonical-index +function, orbit-size histograms and hashes of the sorted representative +indices. Counts are search-domain cardinalities, not measured speedups. +No claim is made that this is the largest safe symmetry group. + +This removes one specific prerequisite for a smaller collision search. +It does not run that search, refute a new field, reproduce the predecessor's +F2/F3 results, or certify any group realization of a relaxed partition. +The investigation stops at this first verified reduction. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/projector-word-symmetry +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/projector-word-symmetry/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/projector-word-symmetry/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/projector-word-symmetry --check-source-history +``` + +Use an equivalent CPython 3.12 path on another machine. The direct marker is +`PASS_PROJECTOR_WORD_SYMMETRY`. Each direct run emits a generated JSON receipt +with counts, representative digests and SHA256 hashes of all six package +files. It writes no files and needs neither Git nor network access. No +hand-written receipt is used as evidence. Registered normal and optimized +commands both cover the complete table and use explicit checks that survive +Python optimization. + +The finite checks also construct the fields of orders 2,3,4,5,7,8,9, compare +two projector inventories, count every fixed projector, and check the formula +at lengths 1,3,5. New formal positional words test conjugation and +opposite-group covariance. Fifteen rejecting controls and two semantic +controls distinguish invalid replay inputs, transpose without reversal, and +a scalar adapter outside the target normalizer. These finite checks +corroborate the universal written proof, which is not a formal-kernel proof. + +## Scope and credit + +The base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision 8, selected PR6030. The selected binding orientation passed; +it was metadata orientation rather than a scientific replay. The +`bit-new-register-model` card changes explicitly to this formal search-domain +side result. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373332) +records the question. [SOURCES.json](SOURCES.json) pins historical provenance; +there are no live or executable predecessor dependencies. + +Josie Elliston / PR6137 supplies the explicit symmetry blocker and the F3 +context. JoyboyBrian / PR6097 supplies the diagonal-pair model, collision +relaxation and F2 context. Retain Josie Elliston / PR6048, Nick Petalas / +PR6038, Wentao Li / PR4089/4093, Cinna Davis / PR2246 and their credited +register-model lineage. Projector conjugacy, orthogonal projections over +finite fields and Burnside's lemma are classical. The contribution is the +explicit quotient, exact orbit formula and standalone canonical enumeration +for this search family; global literature priority is unclaimed. + +Before claiming, live handoffs and active Discussions, open PRs, this +account's recent work, local reservations, all-main README searches and +merged PR searches were checked for the object, formula and general form. +The overlap snapshot covered 555 open PRs and 6,593 Discussion records with +complete remote pagination. Its sparse local scan omitted 8,787 main note +paths; the separate Git searches covered all main READMEs for the named +terms. Arbitrary historical diffs and unpublished work remain limits. +Searches are not a novelty certificate. + +No new kappa, physical speedup, supplier admission, selected-frontier change, +complete multiplication theorem or discharge of any of the five selected +framework assumptions is claimed. Native conversion, scalar/frame/movement +costs, restoration, precision, compiler closure and a complete paid consumer +remain outside the result. No Lean, Docker or historical scientific suite ran. + +## Open next questions + +Can the F4 or F5 representatives settle the five-call existence question? +Start by transporting every coefficient equation and cancellation rule to +the canonical tuple, then emit an independently checkable refutation or an +actual group realization. No such solver or certificate is supplied here. +The quotient alone proves no new call minimum. + +Can a specified Frobenius action reduce this domain further? Prove covariance +and count its fixed tuples before omitting cases. The present group need not +be maximal. [TASK.json](TASK.json) records these questions, their relevance, +first steps and blockers. No follow-up is reserved. + +## Verifier bounds + +The verifier has no recursion, subprocess, network access, dynamic code +execution or mutable shared store. Field orders are restricted to the seven +listed values, tuple lengths to 1,3,5, and complete tuple enumeration to +24,300,000 entries per field. A census owns one byte array of that size; +its orbit set has at most sixteen indices. Fields checked without a complete +census have at most ninety projectors and thirty-two transformations. +Coefficient expansion has at most thirty-two words. All functions fit +within sixty physical lines. Invalid domains fail explicitly. + +Power of Ten rule 3 has a managed-runtime deviation in verify.py. Python +integers, tuples, dictionaries and arithmetic temporaries allocate during +replay; the platform cannot provide allocation-free interpreted execution. +The enforced finite domains above bound live storage. The byte array is +allocated once before each census and released on return. A larger census +must first change and justify the explicit capacity gate. Warning-strict +normal and optimized execution provide the supported interpreted diagnostics; +no external static analyzer or proof assistant is assumed installed. diff --git a/research/projector-word-symmetry/SOURCES.json b/research/projector-word-symmetry/SOURCES.json new file mode 100644 index 0000000000..1f131c2170 --- /dev/null +++ b/research/projector-word-symmetry/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/diagonal-pair-collision-audit/README.md", + "usage": "provenance", + "git_blob": "7b8d36d096438ee17b91de51d7e3e9dc32a9cf06", + "sha256": "5ab441cf115d5e188a01bc5c06b0299732b99d79e7c84f1aab4daa0aaf4c2b78" + }, + { + "path": "research/diagonal-pair-five-call-collisions/PROOF.md", + "usage": "provenance", + "git_blob": "75a4586f3ab6f3533ba4660a3178aaa226ca38c6", + "sha256": "3d607f594f34c5779508f70bd6afc76989107c5f74e0522021305e8cf9b538b0" + } + ] +} diff --git a/research/projector-word-symmetry/TASK.json b/research/projector-word-symmetry/TASK.json new file mode 100644 index 0000000000..c6ea4d4efd --- /dev/null +++ b/research/projector-word-symmetry/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": "Exact target-family-preserving monomial/reversal-transpose quotient and finite-field orbit formula for odd width-two rank-one-projector words.", + "scope_change_reason": "The nonabelian register-model card is used for a scoped search-domain theorem answering the explicit symmetry blocker in PR6137, rather than a new native supplier.", + "bottleneck_link": "This algebraic side result reduces the finite projector domain needed to investigate changed-field nonabelian diagonal-pair obstructions. It supplies no physical BIT saving.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved symmetry reduction and exact corroboration; do not run predecessor collision searches or extend the construction.", + "outcome": "completed", + "evidence": "PROOF.md proves the universal quotient and formula. verify.py independently enumerates all 27,756,608 length-five tuples over F2/F3/F4/F5 and checks literal fixed counts, finite field arithmetic, canonical representatives, formal coefficient covariance and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the reduced F4 or F5 representatives settle the five-call diagonal-pair existence question?", + "why_it_matters": "It would extend the existing F2/F3 field scope.", + "first_step": "Transport every coefficient equation and cancellation rule to one canonical representative, then emit a checkable refutation or an actual group realization.", + "blocked_by": "No representative collision solver or independently checkable refutation certificate is supplied here." + }, + { + "question": "Can field automorphisms safely reduce this domain further?", + "why_it_matters": "The present quotient need not be the largest safe action.", + "first_step": "Prove covariance under a specified Frobenius action and count its fixed tuples before changing the search domain.", + "blocked_by": "A larger-action proof and orbit count are not supplied; no follow-up is reserved." + } + ], + "claim_type": "scoped algebraic proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373332", + "environment": { + "python": "CPython 3.12.15", + "os": "macOS 27.0.1", + "machine": "arm64", + "dependencies": "standard library only" + } +} diff --git a/research/projector-word-symmetry/VERIFY.json b/research/projector-word-symmetry/VERIFY.json new file mode 100644 index 0000000000..e34e87ae95 --- /dev/null +++ b/research/projector-word-symmetry/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": 300, + "checks": "Exact finite-field fixed counts, complete F2/F3/F4/F5 length-five orbit enumeration, coefficient covariance and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same complete finite domain and controls with Python optimization enabled." + } + ] +} diff --git a/research/projector-word-symmetry/verify.py b/research/projector-word-symmetry/verify.py new file mode 100644 index 0000000000..da4b672d30 --- /dev/null +++ b/research/projector-word-symmetry/verify.py @@ -0,0 +1,335 @@ +"""Exact symmetry counts for a declared width-two universal search family. + +Produced by Nick Petalas. Apache-2.0. +No predecessor executable, external dependency, Git or network access is used. +""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys + +Matrix = tuple[int, int, int, int] +IDENTITY: Matrix = (1, 0, 0, 1) +ZERO: Matrix = (0, 0, 0, 0) +E00: Matrix = (1, 0, 0, 0) +E11: Matrix = (0, 0, 0, 1) +SPECS = {2: (2, (0, 1)), 3: (3, (0, 1)), 4: (2, (1, 1, 1)), + 5: (5, (0, 1)), 7: (7, (0, 1)), 8: (2, (1, 1, 0, 1)), + 9: (3, (1, 0, 1))} + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def raw_product(a: int, b: int, p: int, modulus: tuple[int, ...]) -> int: + degree = len(modulus) - 1 + aa = tuple((a // p**i) % p for i in range(degree)) + bb = tuple((b // p**i) % p for i in range(degree)) + coeff = [0] * (2 * degree - 1) + for i in range(degree): + for j in range(degree): + coeff[i + j] = (coeff[i + j] + aa[i] * bb[j]) % p + for i in range(2 * degree - 2, degree - 1, -1): + lead = coeff[i] + for j in range(degree + 1): + coeff[i - degree + j] = ( + coeff[i - degree + j] - lead * modulus[j]) % p + return sum(coeff[i] * p**i for i in range(degree)) + + +class Field: + __slots__ = ("q", "p", "add", "mul", "neg", "inverse") + + def __init__(self, q: int, p: int, add: tuple[tuple[int, ...], ...], + mul: tuple[tuple[int, ...], ...], neg: tuple[int, ...], + inverse: tuple[int, ...]) -> None: + self.q = q + self.p = p + self.add = add + self.mul = mul + self.neg = neg + self.inverse = inverse + + +def field(q: int) -> Field: + require(type(q) is int and q in SPECS, "unsupported finite replay field") + p, modulus = SPECS[q] + degree = len(modulus) - 1 + require(p**degree == q and modulus[-1] == 1, "field specification") + add = tuple(tuple(sum((((a // p**i) % p + (b // p**i) % p) % p) + * p**i for i in range(degree)) + for b in range(q)) for a in range(q)) + mul = tuple(tuple(raw_product(a, b, p, modulus) for b in range(q)) + for a in range(q)) + neg = tuple(next(b for b in range(q) if add[a][b] == 0) for a in range(q)) + inverses = [0] + for a in range(1, q): + candidates = tuple(b for b in range(1, q) if mul[a][b] == 1) + require(len(candidates) == 1, "nonfield modulus") + inverses.append(candidates[0]) + return Field(q, p, add, mul, neg, tuple(inverses)) + + +def mm(f: Field, a: Matrix, b: Matrix) -> Matrix: + s, t = f.add, f.mul + return (s[t[a[0]][b[0]]][t[a[1]][b[2]]], + s[t[a[0]][b[1]]][t[a[1]][b[3]]], + s[t[a[2]][b[0]]][t[a[3]][b[2]]], + s[t[a[2]][b[1]]][t[a[3]][b[3]]]) + + +def transpose(a: Matrix) -> Matrix: + return (a[0], a[2], a[1], a[3]) + + +def subtract(f: Field, a: Matrix, b: Matrix) -> Matrix: + return tuple(f.add[x][f.neg[y]] for x, y in zip(a, b, strict=True)) + + +def plus(f: Field, a: Matrix, b: Matrix) -> Matrix: + return tuple(f.add[x][y] for x, y in zip(a, b, strict=True)) + + +def invert(f: Field, a: Matrix) -> Matrix: + det = f.add[f.mul[a[0]][a[3]]][f.neg[f.mul[a[1]][a[2]]]] + require(det != 0, "singular scalar adapter") + d = f.inverse[det] + return tuple(f.mul[d][x] for x in (a[3], f.neg[a[1]], f.neg[a[2]], a[0])) + + +def conjugate(f: Field, s: Matrix, a: Matrix) -> Matrix: + return mm(f, mm(f, s, a), invert(f, s)) + + +def is_projector(f: Field, a: Matrix) -> bool: + return mm(f, a, a) == a and f.add[a[0]][a[3]] == 1 + + +def projectors(f: Field) -> tuple[Matrix, ...]: + direct = tuple(a for a in product(range(f.q), repeat=4) if is_projector(f, a)) + outer: set[Matrix] = set() + vectors = tuple(product(range(f.q), repeat=2)) + for u in vectors: + for v in vectors: + if f.add[f.mul[u[0]][v[0]]][f.mul[u[1]][v[1]]] == 1: + outer.add(tuple(f.mul[x][y] for x in u for y in v)) + require(set(direct) == outer, "independent projector inventory") + require(len(direct) == f.q * (f.q + 1), "projector cardinality") + return direct + + +def symmetries(f: Field) -> tuple[Matrix, ...]: + return (tuple((t, 0, 0, 1) for t in range(1, f.q)) + + tuple((0, t, 1, 0) for t in range(1, f.q))) + + +def permutations(f: Field, items: tuple[Matrix, ...]) -> tuple[tuple[int, ...], ...]: + indices = {a: i for i, a in enumerate(items)} + normal = tuple(tuple(indices[conjugate(f, s, a)] for a in items) + for s in symmetries(f)) + reverse_maps = tuple(tuple(indices[conjugate(f, s, transpose(a))] for a in items) + for s in symmetries(f)) + return normal + reverse_maps + + +def orbit_formula(f: Field, length: int) -> int: + require(type(length) is int and length in (1, 3, 5), "odd replay length") + q, n, odd = f.q, f.q * (f.q + 1), int(f.p != 2) + numerator = (n**length + 2**length * (q - 2 + odd * ((q - 1) // 2)) + + (q - 1) * (q + odd) * n**(length // 2)) + denominator = 4 * (q - 1) + require(numerator % denominator == 0, "nonintegral Burnside quotient") + return numerator // denominator + + +def field_checks(f: Field) -> int: + for a, b, c in product(range(f.q), repeat=3): + require(f.add[f.add[a][b]][c] == f.add[a][f.add[b][c]], "add associativity") + require(f.mul[f.mul[a][b]][c] == f.mul[a][f.mul[b][c]], "mul associativity") + require(f.mul[a][f.add[b][c]] == f.add[f.mul[a][b]][f.mul[a][c]], + "distributivity") + for a in range(f.q): + require(f.add[0][a] == a and f.mul[1][a] == a, "field identities") + require(f.mul[a][0] == 0, "field zero") + return f.q**3 + + +def fixed_counts(f: Field, items: tuple[Matrix, ...]) -> dict[str, object]: + n, half = len(items), 2 * (f.q - 1) + maps = permutations(f, items) + require(len(maps) == 2 * half and len(set(maps)) == 2 * half, "action order") + require(all(set(p) == set(range(n)) for p in maps), "action bijections") + rows = [] + for s, p, r in zip(symmetries(f), maps[:half], maps[half:], strict=True): + c = sum(p[i] == i for i in range(n)) + h = sum(r[i] == i for i in range(n)) + a = mm(f, s, transpose(invert(f, s))) + pair = sum(conjugate(f, a, x) == x for x in items) + require(h == 0 or pair == n, "middle fixed point forces paired freedom") + rows.append((c, h, pair)) + counts = {} + for length in (1, 3, 5): + fixed_sum = sum(c**length + h * pair**(length // 2) for c, h, pair in rows) + require(fixed_sum % (2 * half) == 0, "Burnside divisibility") + count = fixed_sum // (2 * half) + require(count == orbit_formula(f, length), "literal fixed-count formula") + counts[str(length)] = count + return {"field": f.q, "projectors": n, "fixed_rows": rows, "orbits": counts} + + +def image_index(digits: tuple[int, ...], perm: tuple[int, ...], + reverse: bool, n: int) -> int: + result = 0 + for i in range(len(digits)): + digit = digits[-1 - i] if reverse else digits[i] + result = result * n + perm[digit] + return result + + +def decode(index: int, n: int, length: int) -> tuple[int, ...]: + digits = [0] * length + for i in range(length - 1, -1, -1): + index, digits[i] = divmod(index, n) + require(index == 0, "tuple index range") + return tuple(digits) + + +def canonical(digits: tuple[int, ...], maps: tuple[tuple[int, ...], ...], n: int) -> int: + require(len(digits) in (1, 3, 5), "canonical length") + require(all(type(x) is int and 0 <= x < n for x in digits), "projector index") + require(len(maps) > 0 and len(maps) % 2 == 0, "canonical action size") + require(all(len(p) == n and set(p) == set(range(n)) for p in maps), + "canonical permutations") + return min(image_index(digits, p, j >= len(maps) // 2, n) + for j, p in enumerate(maps)) + + +def census(f: Field, length: int) -> dict[str, object]: + items = projectors(f) + maps, n = permutations(f, items), len(items) + total = n**length + require(length in (1, 3, 5) and total <= 24_300_000, "census capacity") + seen = bytearray(total) + histogram: dict[int, int] = {} + digest, count, covered = sha256(), 0, 0 + for index in range(total): + if seen[index]: + continue + digits = decode(index, n, length) + orbit = {image_index(digits, p, j >= len(maps) // 2, n) + for j, p in enumerate(maps)} + require(min(orbit) == index, "canonical enumeration") + require(all(not seen[i] for i in orbit), "overlapping orbits") + require(len(maps) % len(orbit) == 0, "orbit stabilizer divisor") + for i in orbit: + seen[i] = 1 + covered += len(orbit) + count += 1 + histogram[len(orbit)] = histogram.get(len(orbit), 0) + 1 + digest.update(index.to_bytes(8, "big")) + require(covered == total and all(seen), "complete tuple coverage") + require(count == orbit_formula(f, length), "enumerated orbit formula") + return {"field": f.q, "length": length, "tuples": total, "orbits": count, + "orbit_size_histogram": histogram, "representatives_sha256": digest.hexdigest()} + + +def expand(f: Field, word: tuple[Matrix, ...]) -> dict[tuple[int, ...], Matrix]: + result = {(): IDENTITY} + for label, projector in enumerate(word): + following: dict[tuple[int, ...], Matrix] = {} + for w, coefficient in result.items(): + for suffix, factor in (((), subtract(f, IDENTITY, projector)), + ((label,), projector)): + key = w + suffix + following[key] = plus(f, following.get(key, ZERO), mm(f, coefficient, factor)) + result = {w: a for w, a in following.items() if a != ZERO} + return result + + +def covariance_checks(f: Field, items: tuple[Matrix, ...]) -> int: + fixtures = 0 + for offset in range(min(10, len(items))): + word = tuple(items[(offset + i * i + 1) % len(items)] for i in range(5)) + original = expand(f, word) + for s in symmetries(f): + got = expand(f, tuple(conjugate(f, s, a) for a in word)) + expected = {w: conjugate(f, s, a) for w, a in original.items()} + require(got == expected, "formal conjugation covariance") + reverse_word = tuple(conjugate(f, s, transpose(a)) for a in reversed(word)) + got = expand(f, reverse_word) + expected = {tuple(4 - i for i in reversed(w)): + conjugate(f, s, transpose(a)) for w, a in original.items()} + require(got == expected, "reversal and opposite-group covariance") + require({conjugate(f, s, E00), conjugate(f, s, E11)} == {E00, E11}, + "target normalizer") + fixtures += 1 + return fixtures + + +def controls() -> int: + rejected = 0 + for q in (0, 1, 6, 10, True): + try: + field(q) + except ValueError: + rejected += 1 + f = field(3) + for length in (0, 2, 4, 7, True): + try: + orbit_formula(f, length) + except ValueError: + rejected += 1 + items = projectors(f) + maps = permutations(f, items) + for digits in ((-1,), (len(items),), (True,), (0, 1)): + try: + canonical(digits, maps, len(items)) + except ValueError: + rejected += 1 + try: + invert(f, ZERO) + except ValueError: + rejected += 1 + require(rejected == 15, "rejection controls") + require(not is_projector(f, ZERO) and not is_projector(f, IDENTITY), "rank condition") + word = (E00, (1, 1, 0, 0)) + wrong = expand(f, tuple(transpose(a) for a in word)) + intended = {tuple(1 - i for i in reversed(w)): transpose(a) + for w, a in expand(f, word).items()} + require(wrong != intended, "transpose without reversal is not the claimed operation") + require(conjugate(f, (1, 1, 0, 1), E11) not in (E00, E11), + "arbitrary scalar conjugation does not preserve the target pattern") + return rejected + + +def main() -> None: + require(len(sys.argv) == 1, "this bounded verifier accepts no arguments") + fixed, field_triples, covariance = [], 0, 0 + for q in SPECS: + f = field(q) + field_triples += field_checks(f) + items = projectors(f) + fixed.append(fixed_counts(f, items)) + covariance += covariance_checks(f, items) + maps = permutations(f, items) + for i in range(len(items)): + index = canonical((i,), maps, len(items)) + require(canonical(decode(index, len(items), 1), maps, len(items)) == index, + "canonical idempotence") + censuses = [census(field(q), 5) for q in (2, 3, 4, 5)] + rejection_count = 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_PROJECTOR_WORD_SYMMETRY", "fields": fixed, + "field_triples": field_triples, "formal_covariance_fixtures": covariance, + "censuses": censuses, "rejections": rejection_count, + "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()