From 2c69372760776c6f522ba31fef3357e2aa9d309d Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 12:18:51 +0000 Subject: [PATCH] feat(research): classify regular rank-one projector triples --- .../regular-projector-triple-orbits/PROOF.md | 153 +++++++++ .../regular-projector-triple-orbits/README.md | 133 ++++++++ .../SOURCES.json | 18 ++ .../regular-projector-triple-orbits/TASK.json | 97 ++++++ .../VERIFY.json | 34 ++ .../regular-projector-triple-orbits/verify.py | 302 ++++++++++++++++++ 6 files changed, 737 insertions(+) create mode 100644 research/regular-projector-triple-orbits/PROOF.md create mode 100644 research/regular-projector-triple-orbits/README.md create mode 100644 research/regular-projector-triple-orbits/SOURCES.json create mode 100644 research/regular-projector-triple-orbits/TASK.json create mode 100644 research/regular-projector-triple-orbits/VERIFY.json create mode 100644 research/regular-projector-triple-orbits/verify.py diff --git a/research/regular-projector-triple-orbits/PROOF.md b/research/regular-projector-triple-orbits/PROOF.md new file mode 100644 index 0000000000..b00b242fdf --- /dev/null +++ b/research/regular-projector-triple-orbits/PROOF.md @@ -0,0 +1,153 @@ +# Regular fully coupled rank-one triples + +This proof was produced by Nick Petalas. Apache-2.0. It is a scoped written +linear-algebra proof. Finite corroboration is separate from its universal +quantifiers. Independent human and formal proof-kernel review are unclaimed. + +## Contract and result + +Let F be any field, n>=3, and let P1,P2,P3 be an ordered triple of rank-one +idempotents on V=F^n. Put S=P1+P2+P3. Require + +1. rank(S)=rank(S^2)=3; +2. p=tr(P1 P2), q=tr(P1 P3), r=tr(P2 P3) are all nonzero. + +Two triples are equivalent exactly when one invertible linear map +simultaneously conjugates all three, preserving their order. No transpose, +projector permutation or field automorphism is included in this equivalence. +Set u=tr(P1 P2 P3). Then u is nonzero. The complete invariant is + + (F,n,p,q,r,u). + +The admissible quadruples are exactly p,q,r,u in F* such that + + Delta = 1-p-q-r+u+pqr/u != 0. (1) + +A unique representative on the three active coordinates is obtained from + + G = [ 1 1 1 ] + [ p 1 u/q] + [ q rq/u 1 ] (2) + +by setting Pi=e_i times row i of G, and adjoining n-3 zero coordinates. +Over a finite field of order Q, the exact number of these conjugacy classes +is + + N(Q)=Q^4-5Q^3+9Q^2-9Q+6. (3) + +This is one fixed algebraic state class, not a classification of arbitrary +triples or a bound on a complete physical register search. + +## Rank-one factorization and the active space + +Write Pi=x_i y_i with x_i nonzero and y_i a row covector. Idempotence says +y_i x_i=1. Put C=[x_1 x_2 x_3], D=[y_1;y_2;y_3] and G=DC. Then S=CD. +The first rank condition implies rank C=rank D=3. Thus C is injective and +D is surjective, so rank(S^2)=rank(C G D)=rank G. The second rank equality +therefore makes G invertible. + +Consequently W=im C and N=ker D have dimensions 3 and n-3 and intersect +only at zero. Thus V=W direct-sum N. All Pi preserve W and kill N. In the +basis x_1,x_2,x_3 of W, Pi has exactly row i of G in its ith row and zero +in the other rows. Conversely any invertible unit-diagonal G constructs +rank-one idempotents with rank(S)=rank(S^2)=3, including after adjoining zero +spectators. + +## Completeness of the four traces + +The factorization Pi=x_i y_i is unique up to x_i -> d_i x_i, +y_i -> d_i^(-1) y_i, with d_i in F*. Its Gram matrix therefore changes as + + G -> diag(d)^(-1) G diag(d). (4) + +Ambient simultaneous conjugation preserves G when the factors are carried +along. Conversely, equal G gives an intertwiner by mapping the three image +basis vectors to their counterparts and extending by any isomorphism between +the common kernels. Thus simultaneous conjugacy is exactly diagonal similarity +of these Grams, together with equal ambient n and field F. This argument is +direct and does not assume a predecessor's two-projector classification. + +Write g_ij=y_i x_j. Rank-one multiplication gives + + p=g_12 g_21, q=g_13 g_31, r=g_23 g_32, + u=g_12 g_23 g_31, + v=tr(P1 P3 P2)=g_13 g_32 g_21, + uv=pqr. (5) + +The nonzero pair traces imply that all six off-diagonal g_ij are nonzero, +and hence u is nonzero. Apply (4) with +d_1=1, d_2=1/g_12, d_3=1/g_13. The first row becomes (1,1,1). Equations +(5) then force exactly (2). Any further diagonal similarity preserving this +first row has d_1=d_2=d_3 and acts trivially. This proves uniqueness and +completeness over every field. Expanding the determinant of (2) gives (1), +which proves that there are no further realizability restrictions. + +The ambient centralizer of a representative is F* on W times GL(N). +Indeed a commuting map preserves each image line and each kernel, so it +preserves W and N. On W it is diagonal; the six nonzero couplings force +its three diagonal entries to agree. Conversely these maps commute. +Over a finite field each ambient class thus has size + + |GL_n(F)| / ((Q-1)|GL_(n-3)(F)|). (6) + +Use |GL_0|=1. Formula (6) counts actual ordered triples in one class, not +additional conjugacy classes. + +## Exact count over every finite field + +There are (Q-1)^4 candidate quadruples. Count those with Delta=0. For fixed +p,q,u, rewrite that equation as + + A+B r=0, A=1-p-q+u, B=pq/u-1. (7) + +If u!=pq, then B!=0, so exactly one r solves (7). This r is nonzero exactly +when A!=0. Before excluding A=0 there are (Q-1)^2(Q-2) choices of p,q,u. +For A=0 we must have u=p+q-1, nonzero and unequal to pq. The inequality +u!=pq is equivalent to (p-1)(q-1)!=0. There are (Q-2)^2 pairs with +p,q outside {0,1}, of which Q-2 have p+q=1. Therefore the number to remove +is (Q-2)(Q-3). This case contributes + + (Q-1)^2(Q-2) - (Q-2)(Q-3). + +If u=pq, then B=0 and A=(1-p)(1-q). Thus Delta=0 exactly when p=1 or +q=1, independently of the nonzero r. This contributes + + (2Q-3)(Q-1). + +Adding the two contributions gives Q^3-3Q^2+5Q-5. Subtracting this from +(Q-1)^4 proves (3). The argument uses only field arithmetic and applies to +every prime power, including characteristic two. At Q=2 the intermediate +products containing Q-2 are zero, so the same counting argument remains valid. + +## Why pair data alone is insufficient + +Over F5 take (p,q,r)=(1,1,1). The choices u=2 and u=3 give the invertible +Grams + + [1 1 1] [1 1 1] + [1 1 2] and [1 1 3]. + [1 3 1] [1 2 1] + +Both determinants equal 3. They have the same pair traces. Their oriented +triple traces differ, so they are not simultaneously conjugate. This also +shows why transposition or reversing a word cannot silently be included in +the stated equivalence. The witness is a distinction between states, not a +paid-call lower bound. + +## Finite evidence and scope + +The checker enumerates every unit-diagonal Gram with nonzero off-diagonal +entries over F2,F3,F4,F5,F7. Its diagonal orbits are compared as complete sets +with a second enumeration that starts from four trace parameters. A six-term +determinant and row reduction separately check invertibility. Actual matrix +multiplication checks idempotence and the projector traces. F4 uses +F2[t]/(t^2+t+1), rather than integers modulo four. + +For every canonical ternary class, another check enumerates every GL3(F3) +basis change, computes all three conjugated matrices and their traces, and +counts the distinct endpoints. Zero spectators of dimensions one and two, +ten invalid-domain cases and the pair-trace ambiguity witness exercise the +boundaries. These finite checks corroborate the proof; they do not replace +its all-field argument or establish a physical caller. Singular active +systems, missing pair couplings, unordered equivalence, native implementation, +dirty-helper programs and a complete recursive invoice are outside scope. diff --git a/research/regular-projector-triple-orbits/README.md b/research/regular-projector-triple-orbits/README.md new file mode 100644 index 0000000000..34f93e2c3f --- /dev/null +++ b/research/regular-projector-triple-orbits/README.md @@ -0,0 +1,133 @@ +# Exact orbits of regular fully coupled projector triples + +This contribution was produced by Nick Petalas. Apache-2.0. + +For an ordered rank-one idempotent triple P1,P2,P3 over any field, put +S=P1+P2+P3. Assume rank(S)=rank(S^2)=3 and all three pair traces are nonzero. +Then the ambient dimension and + + p=tr(P1P2), q=tr(P1P3), r=tr(P2P3), u=tr(P1P2P3) + +are a complete invariant under simultaneous GL conjugacy. The admissible +quadruples are exactly the nonzero p,q,r,u with + + 1-p-q-r+u+pqr/u != 0. + +Over every finite field of order Q there are exactly + + Q^4-5Q^3+9Q^2-9Q+6 + +such classes, in every fixed ambient dimension n>=3. [PROOF.md](PROOF.md) +gives the all-field proof, explicit representative and centralizer. Two +triples over F5 give different classes with identical +pair traces. Thus a descriptor retaining only the three pair traces loses +information even in this regular class. + +Claim type: scoped written algebraic proof with exact finite corroboration. +The new result is the triple normal form and closed class count. It does not +claim global literature priority for rank-one factorizations, diagonal +similarity or cycle products, which are classical methods. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/regular-projector-triple-orbits/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/regular-projector-triple-orbits/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/regular-projector-triple-orbits +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/regular-projector-triple-orbits --check-source-history +``` + +Another machine can substitute its CPython 3.12 executable. Direct replay +also works from a Git-free export of the six package files. The verifier +writes nothing. It prints a generated receipt with the six file hashes and +`PASS_REGULAR_PROJECTOR_TRIPLE_ORBITS`. + +The full six-entry Gram domains contain 1, 64, 729, 4,096 and 46,656 matrices +over F2,F3,F4,F5,F7. They give 0, 6, 50, 186 and 1,070 classes respectively. +Every accepted Gram is compared with its four-trace representative. A second +enumeration expands every representative's complete diagonal orbit, and the +two full sets must agree. Matrix multiplication checks the projector traces; +row reduction separately checks invertibility. F4 uses t^2+t+1. + +For every ternary representative, all 11,232 GL3(F3) basis changes are checked, +giving 67,392 conjugated triples and 33,696 distinct endpoints. This agrees +with the proved scalar centralizer. Spectator dimensions zero, one and two, +ten domain rejection controls and an explicit F5 pair-trace ambiguity fixture +also pass. The universal quantifiers come from the proof, rather than an +extrapolation of these finite domains. No predecessor scientific checker is +imported or run. + +## Scope, provenance and credit + +This is an original state-classification side question, with a changed +`bit-new-register-model` scope recorded in [TASK.json](TASK.json). It concerns +full simultaneous conjugacy on a three-dimensional active direct summand. +The separately claimed width-two monomial/reversal quotient concerns +target-preserving word symmetries and a different equivalence relation. + +Credit MatShep's [PR4762](https://github.com/CrocSwap/integer-mult-bounds/pull/4762), +head `3b4e0449262b0b1e07b80e009ef71cc0ca5bf816`, for the related two-idempotent +factor descriptor, and codyw912's +[PR4735](https://github.com/CrocSwap/integer-mult-bounds/pull/4735), head +`4afbea22e79e19d1d65702eb4090d454ee39d967`, for its inclusion/observation +framework. Those results are context, not proof premises or audit targets. +The proof here derives the three-factor reduction directly. Credit the +eumemic/woklerx scalar-projector register lineage and the retained native, +frame, helper, compiler and outer contributors for the application context. +No predecessor files or credit lines are changed. + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, +selected PR6030. [SOURCES.json](SOURCES.json) pins task provenance. There are +no external scientific runtime inputs. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373460) +records the scope. Live claims, local reservations, recent account work, +main README searches and all-state general/formula PR searches were checked. +The broader cache covered 556 open PRs and 6,605 Discussion records with +complete remote pagination; sparse local coverage was 137 of 8,917 notes. +Arbitrary historical diffs and unpublished work remain limits. + +Singular active systems and zero pair traces are excluded. Projector order, +field and ambient dimension are retained. Transpose, reversal, field +automorphisms and projector permutations are not part of this equivalence. +This is not a complete word-state invariant. A search must still restrict +conjugations to its target stabilizer and preserve all other state. Physical +basis changes, native maps, input access, arbitrary dirty restoration, +precision/tape/stock, compiler closure and a complete paid/target invoice +are unpriced. No supplier, paid-call saving, kappa or selected-frontier change +is claimed. All five selected framework assumptions remain. + +No selected scientific cold replay, Lean, Docker, independent human review +or formal proof-kernel verification is claimed. + +## Open next questions + +- Classify a singular or partially uncoupled triple. Begin with one fixed + singular Gram and retain its factor kernel and observation image. The + regular direct-sum reduction used here is unavailable there. +- Bind this descriptor to one target-preserving search and charge every + basis change. Begin with an explicit alphabet and target stabilizer. + A concrete caller and its full paid invoice are still missing. + +Structured first steps and blockers are in TASK.json. No construction +expansion follows from this algebraic count. + +## Verifier constraints + +All function bodies have fewer than 60 physical lines. There is no recursion, +network, subprocess, dynamic code execution or output-file creation. Public +matrix and field boundaries validate their finite domains. Internal calls +use those validated objects. Loop bounds are Q<=7, matrix dimension<=5, +six Gram entries, four trace parameters, and the 3^9 ternary basis candidates. +Mathematical guards are explicit exceptions and remain active under -O. + +Power-of-ten rule 3 deviation: CPython allocates managed integers, tuples, +sets and dictionaries during checking. At most 46,656 raw Gram candidates, +38,520 accepted Grams per set, 1,312 class keys and 33,696 distinct ternary +endpoints are retained in fixed bounded phases. File reads are limited to +one MiB plus one byte for each of six fixed files. The normal and optimized +registered commands exercise these bounds. A fixed-allocation embedded +implementation would require a different runtime. Warning-strict execution +and source compilation are the available diagnostics; no separate static +linter or repository-wide build configuration is introduced. diff --git a/research/regular-projector-triple-orbits/SOURCES.json b/research/regular-projector-triple-orbits/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/regular-projector-triple-orbits/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/regular-projector-triple-orbits/TASK.json b/research/regular-projector-triple-orbits/TASK.json new file mode 100644 index 0000000000..baec63e3fc --- /dev/null +++ b/research/regular-projector-triple-orbits/TASK.json @@ -0,0 +1,97 @@ +{ + "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 regular fully coupled ordered triples of rank-one idempotents under simultaneous GL conjugacy over every field, and count their classes over every finite field.", + "scope_change_reason": "A self-contained algebraic state-classification side result replaces native-word construction. The canonical form distinguishes states with identical pair traces; no native or supplier acceptance gate is claimed.", + "bottleneck_link": "Side result for coupled-register search state descriptions. Pair-only trace data loses continuation-relevant oriented products. A physical consumer, target-preserving quotient and complete paid bill remain missing.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved canonical form and closed class count with fixed-domain exact corroboration. Do not extend to degenerate tuples or optimize a supplier.", + "outcome": "completed", + "evidence": "PROOF.md gives an all-field proof and finite-field closed count. verify.py enumerates full Gram domains and all ternary conjugations, and emits a receipt bound to the six package files.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which additional invariants classify triples when rank(S^2)> 1)*b << 1) + if value & 4: + value ^= 7 + else: + value = a*b % order + row.append(value) + rows.append(tuple(row)) + self.mul = tuple(rows) + self.inv = (0,) + tuple(next(b for b in range(1, order) + if self.mul[a][b] == 1) + for a in range(1, order)) + + +def validate_matrix(a, f, maximum=5): + require(isinstance(a, tuple) and 1 <= len(a) <= maximum, "matrix size") + require(all(isinstance(row, tuple) and len(row) == len(a) for row in a), + "matrix shape") + require(all(type(x) is int and 0 <= x < f.q for row in a for x in row), + "field entry") + + +def product(a, b, f): + n = len(a) + out = [[0]*n for _ in range(n)] + for i in range(n): + for j in range(n): + for k in range(n): + out[i][j] = f.add[out[i][j]][f.mul[a[i][k]][b[k][j]]] + return tuple(tuple(row) for row in out) + + +def rank(a, f): + rows = [list(row) for row in a] + n, pivot = len(a), 0 + for col in range(n): + found = next((i for i in range(pivot, n) if rows[i][col]), None) + if found is None: + continue + rows[pivot], rows[found] = rows[found], rows[pivot] + scale = f.inv[rows[pivot][col]] + rows[pivot] = [f.mul[scale][x] for x in rows[pivot]] + for i in range(n): + if i != pivot: + factor = f.neg[rows[i][col]] + rows[i] = [f.add[x][f.mul[factor][y]] + for x, y in zip(rows[i], rows[pivot])] + pivot += 1 + return pivot + + +def inverse(a, f): + n = len(a) + rows = [list(a[i])+[int(i == j) for j in range(n)] for i in range(n)] + for col in range(n): + found = next((i for i in range(col, n) if rows[i][col]), None) + require(found is not None, "singular conjugator") + rows[col], rows[found] = rows[found], rows[col] + scale = f.inv[rows[col][col]] + rows[col] = [f.mul[scale][x] for x in rows[col]] + for i in range(n): + if i != col: + factor = f.neg[rows[i][col]] + rows[i] = [f.add[x][f.mul[factor][y]] + for x, y in zip(rows[i], rows[col])] + return tuple(tuple(row[n:]) for row in rows) + + +def determinant(a, f): + """Six Leibniz terms, separate from row reduction.""" + total = 0 + for perm in itertools.permutations(range(3)): + term = 1 + for i in range(3): + term = f.mul[term][a[i][perm[i]]] + inversions = sum(perm[i] > perm[j] for i in range(3) + for j in range(i+1, 3)) + total = f.add[total][f.neg[term] if inversions % 2 else term] + return total + + +def trace(a, f): + out = 0 + for i in range(len(a)): + out = f.add[out][a[i][i]] + return out + + +def gram_key(g, f): + validate_matrix(g, f, 3) + require(len(g) == 3 and all(g[i][i] == 1 for i in range(3)), + "unit diagonal") + require(all(g[i][j] != 0 for i in range(3) for j in range(3)), + "fully coupled") + require(determinant(g, f) != 0, "regular active summand") + p = f.mul[g[0][1]][g[1][0]] + q = f.mul[g[0][2]][g[2][0]] + r = f.mul[g[1][2]][g[2][1]] + u = f.mul[f.mul[g[0][1]][g[1][2]]][g[2][0]] + return p, q, r, u + + +def representative(key, f): + require(isinstance(key, tuple) and len(key) == 4, "four invariants") + require(all(type(x) is int and 0 < x < f.q for x in key), + "nonzero invariant") + p, q, r, u = key + g = ((1, 1, 1), (p, 1, f.mul[u][f.inv[q]]), + (q, f.mul[f.mul[r][q]][f.inv[u]], 1)) + require(gram_key(g, f) == key, "admissible invariant") + return g + + +def diagonal_conjugate(g, scales, f): + return tuple(tuple(f.mul[f.mul[f.inv[scales[i]]][g[i][j]]][scales[j]] + for j in range(3)) for i in range(3)) + + +def projectors(g, ambient=3): + require(3 <= ambient <= 5, "ambient dimension") + return tuple(tuple(tuple(g[i][j] if row == i and j < 3 else 0 + for j in range(ambient)) + for row in range(ambient)) for i in range(3)) + + +def triple_key(ps, f): + require(isinstance(ps, tuple) and len(ps) == 3, "three projectors") + for p in ps: + validate_matrix(p, f) + require(len(p) == len(ps[0]), "common ambient dimension") + require(rank(p, f) == 1 and product(p, p, f) == p, "rank-one idempotent") + n = len(ps[0]) + s = tuple(tuple(f.add[f.add[ps[0][i][j]][ps[1][i][j]]][ps[2][i][j]] + for j in range(n)) for i in range(n)) + require(rank(s, f) == rank(product(s, s, f), f) == 3, + "regular active summand") + pairs = tuple(trace(product(ps[i], ps[j], f), f) + for i, j in ((0, 1), (0, 2), (1, 2))) + u = trace(product(product(ps[0], ps[1], f), ps[2], f), f) + require(all(x != 0 for x in pairs), "fully coupled") + return pairs+(u,) + + +def census(f): + """All six-entry Grams, compared with separately expanded orbits.""" + raw, classes, singular = set(), {}, 0 + positions = ((0, 1), (0, 2), (1, 0), (1, 2), (2, 0), (2, 1)) + for values in itertools.product(range(1, f.q), repeat=6): + g = [[int(i == j) for j in range(3)] for i in range(3)] + for (i, j), value in zip(positions, values): + g[i][j] = value + g = tuple(tuple(row) for row in g) + if determinant(g, f) == 0: + singular += 1 + continue + key = gram_key(g, f) + normalized = diagonal_conjugate(g, (1, f.inv[g[0][1]], + f.inv[g[0][2]]), f) + require(normalized == representative(key, f), "normal form") + raw.add(g) + classes[key] = classes.get(key, 0)+1 + expanded, accepted = set(), 0 + for key in itertools.product(range(1, f.q), repeat=4): + p, q, r, u = key + v = f.mul[f.mul[f.mul[p][q]][r]][f.inv[u]] + delta = f.add[f.add[f.add[f.add[f.add[1][f.neg[p]]][f.neg[q]]] + [f.neg[r]]][u]][v] + if not delta: + continue + g = representative(key, f) + require(rank(g, f) == 3, "row-reduction invertibility") + require(triple_key(projectors(g), f) == key, "matrix trace invariant") + for a, b in itertools.product(range(1, f.q), repeat=2): + expanded.add(diagonal_conjugate(g, (1, a, b), f)) + accepted += 1 + expected = f.q**4-5*f.q**3+9*f.q**2-9*f.q+6 + require(raw == expanded, "complete diagonal-orbit partition") + require(len(classes) == accepted == expected, "closed orbit count") + require(all(count == (f.q-1)**2 for count in classes.values()), "free gauge orbit") + require(len(raw)+singular == (f.q-1)**6, "complete six-entry domain") + return {"field_order": f.q, "raw_grams": (f.q-1)**6, + "regular_grams": len(raw), "classes": accepted, + "singular_grams": singular} + + +def conjugacy_checks(): + """All GL3(F3) basis changes for the six canonical ternary triples.""" + f, seeds = Field(3), [] + for key in itertools.product(range(1, 3), repeat=4): + try: + seeds.append((key, projectors(representative(key, f)))) + except ValueError as exc: + require(str(exc) == "regular active summand", "known rejection") + require(len(seeds) == 6, "six ternary seeds") + endpoints, group = set(), 0 + for entries in itertools.product(range(3), repeat=9): + a = tuple(tuple(entries[3*i:3*i+3]) for i in range(3)) + if determinant(a, f) == 0: + continue + ai = inverse(a, f) + for key, ps in seeds: + changed = tuple(product(product(a, p, f), ai, f) for p in ps) + require(triple_key(changed, f) == key, "full GL trace invariance") + endpoints.add(changed) + group += 1 + require(group == (27-1)*(27-3)*(27-9), "full GL3 enumeration") + require(len(endpoints) == 6*group//2, "scalar centralizer") + return {"group_order": group, "distinct_ordered_triples": len(endpoints), + "conjugated_triples_checked": 6*group} + + +def controls(): + f = Field(5) + g, h = (representative((1, 1, 1, u), f) for u in (2, 3)) + require(gram_key(g, f)[:3] == gram_key(h, f)[:3], "same pair data") + require(gram_key(g, f) != gram_key(h, f), "oriented trace distinction") + for n in (3, 4, 5): + require(triple_key(projectors(g, n), f) == (1, 1, 1, 2), "zero spectators") + invalid = [((1, 1, 1), (1, 1, 1), (1, 1, 1)), + ((1, 0, 1), (1, 1, 1), (1, 1, 1)), + ((2, 1, 1), (1, 1, 1), (1, 1, 1)), + ((1, 1), (1, 1)), ((1, 1, 1), (1, 1, 1), (1, 1, 5))] + rejections = 0 + for bad in invalid: + try: + gram_key(bad, f) + except ValueError: + rejections += 1 + for key in ((0, 1, 1, 2), (1, 1, 1, 1), (1, 1, 2), (1, 1, 1, 5)): + try: + representative(key, f) + except ValueError: + rejections += 1 + require(rejections == len(invalid)+4, "all invalid Grams and keys rejected") + bad_ps = list(projectors(g)) + bad_ps[0] = tuple(tuple(0 for _ in range(3)) for _ in range(3)) + try: + triple_key(tuple(bad_ps), f) + except ValueError as exc: + require(str(exc) == "rank-one idempotent", "rank rejection") + rejections += 1 + require(rejections == 10, "all ten domain rejections") + require(Field(4).add[1][1] == 0 and Field(4).mul[2][2] == 3, + "extension field differs from modular four") + return {"domain_rejections": rejections, "pair_trace_ambiguity_field": 5, + "spectator_dimensions": [0, 1, 2]} + + +def source_hashes(): + package = Path(__file__).resolve().parent + out = {} + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py"): + with (package/name).open("rb") as handle: + data = handle.read(1024*1024+1) + require(len(data) <= 1024*1024, "package-file bound") + out[name] = hashlib.sha256(data).hexdigest() + return out + + +def main(): + report = {"claim_type": "scoped written proof with exact finite corroboration", + "censuses": [census(Field(q)) for q in (2, 3, 4, 5, 7)], + "full_conjugation": conjugacy_checks(), + "controls": controls(), "sha256": source_hashes()} + print(json.dumps(report, sort_keys=True, indent=2)) + print("PASS_REGULAR_PROJECTOR_TRIPLE_ORBITS") + + +if __name__ == "__main__": + main()