diff --git a/research/gl3-rational-two-column-kernel/PROOF.md b/research/gl3-rational-two-column-kernel/PROOF.md new file mode 100644 index 0000000000..09cda4315d --- /dev/null +++ b/research/gl3-rational-two-column-kernel/PROOF.md @@ -0,0 +1,133 @@ +# The exact two-column kernel over characteristic zero + +This is a scoped proof using the finite exact certificate in `verify.py`. +It concerns the address permutation algebra alone. No complete complex +unit or multiplication theorem is asserted. + +## Statement + +Let G=GL_3(F2), let V=Q^{F2^3}, and let P_g e_x=e_{gx}. +For f>=1 define the algebra homomorphism + + rho_f : Q[G] -> End_Q(V^{tensor f}), + rho_f([g]) = P_g^{tensor f}. + +Write C_j for the sum of all elements of order j in Q[G], and put + + E = 6[1] - 2 C_2 + 2 C_4 - C_7. + +Then + + E^2 = 56 E, + ker rho_2 = Q[G] E, + dim_Q ker rho_2 = 18, + dim_Q image rho_2 = 150. + +The same statements hold after extending scalars to C. The map rho_f is +injective for every f>=3. Thus width three is the smallest single positive +width that certifies every formal identity in this characteristic-zero +address algebra. A two-register restored shear realizes a nonidentity +formal map that is identity at both widths one and two. + +## The finite certificate + +The verifier constructs G in two ways. First it lists all three nonzero +binary columns and keeps the invertible matrices. Second it closes the six +elementary binary row additions, with a bound of 168 visited elements. +Both constructions give the same 168 address permutations. The multiplication +table is literal permutation composition, so no presentation or external +group data are assumed. + +Their order populations are + + order 1: 1, order 2: 21, order 3: 56, order 4: 42, order 7: 48. + +The verifier forms all coefficients of E^2 by integer convolution and checks +E^2=56E in all 168 coordinates. It checks centrality against all 168 group +elements. Centrality also follows because element order is conjugacy invariant. +It then sums all 168 permutation actions on all 64 point pairs and checks +that every one of the 4,096 entries of rho_2(E) is zero. These are finite +integer identities, with no numerical tolerance. + +Let A_g be the 64 by 64 matrix P_g^{tensor 2}, viewed as a column of 4,096 +integers. The Gram matrix of these 168 columns has entries + + H[g,h] = = #{x in F2^3 : gx=hx}^2. + +The equality holds because a common nonzero entry of two permutation matrices +is a point pair whose two coordinates have the same images under g and h. +The verifier constructs H from this formula. Gaussian elimination modulo +65537 selects 150 row indices and 150 column indices. A second determinant +calculation on that original integer minor gives a nonzero residue. Trial +division through 256 proves the modulus prime. The generated receipt records +the complete indices and determinant residue, so the minor is reproducible. +Consequently rank_Q H>=150, hence rank_Q rho_2>=150. No inference of a +rational upper rank from a modular upper rank is used. + +## Why this is the entire kernel + +Set e=E/56. The checked product identity says that e is an idempotent. +Left multiplication L_e on Q[G] is therefore an idempotent linear map. +Every diagonal entry of L_e is the identity coefficient of e, namely 6/56. +Its trace is + + 168 * 6/56 = 18. + +An idempotent over Q has eigenvalues zero and one, so its rank equals its +trace. Since e is central, its image is the two-sided ideal Q[G]e=Q[G]E. +The checked rho_2(E)=0 puts this 18-dimensional ideal inside ker rho_2. +It follows that rank_Q rho_2<=168-18=150. The minor proves the opposite +inequality. Thus the image rank is 150 and this ideal is exactly the kernel. +Ranks of rational matrices are unchanged by extension to C, which proves +the complex version as well. + +## Why the third column suffices + +The tuple (1,2,4) is the ordered standard basis of F2^3. Its images under +G are all distinct. For a=sum_g a_g[g], the coefficient at (g1,g2,g4) of + + rho_3(a) e_(1,2,4) + +is exactly a_g. Hence rho_3 is injective. For any f>3, append zero columns +to this tuple. All address maps fix zero, so the same regular orbit and +coefficient recovery apply. This is the standard regular-orbit argument +already used in the binary-stream predecessor. The new content here is the +characteristic-zero kernel below it. + +## A restored two-register witness + +Write E=sum_g c_g[g]. There are 112 nonzero c_g. Start with arbitrary +independent registers (x,y). For each such g, in lexicographic permutation +order, execute + + y <- P_g^{tensor f} y + x <- x + c_g y + y <- (P_g^{-1})^{tensor f} y. + +Every term restores the source y exactly. The final map is + + (x,y) -> (x + rho_f(E)y, y). + +It is invertible, with inverse obtained by changing every c_g to -c_g. +It uses no clean scratch, erasure or assumption that either input is zero. +These address maps and rational scalar additions are free in the stated +address-only part of the complex engine game. No physical movement or +precision price follows from that algebraic convention. + +At width two the map is identity by rho_2(E)=0. At width one the same +identity follows by restricting the width-two calculation to pairs (x,0). +The verifier also executes the chronological word on the complete dirty +input bases, 16 columns at width one and 128 at width two, and checks source +restoration after each term. At width three, take x=0 and y=e_(1,2,4). +The 112 nonzero coefficients of E occur on distinct output basis vectors, +so the word is not identity. The verifier executes that witness too. + +## Limits + +The arithmetic identities and nonzero minor are exhaustive finite evidence. +The linear-algebra deductions above are written proofs, with independent +human and formal proof-kernel review unclaimed. This package does not classify +the characteristic-two kernel, arbitrary address dimension, affine maps, +phase letters, paid C-calls or native precision and tape costs. In particular, +width three certifies only identities whose coefficients lie in Q[G] or C[G]. +It is not an all-width test for the full complex engine. diff --git a/research/gl3-rational-two-column-kernel/README.md b/research/gl3-rational-two-column-kernel/README.md new file mode 100644 index 0000000000..fe195b35dc --- /dev/null +++ b/research/gl3-rational-two-column-kernel/README.md @@ -0,0 +1,118 @@ +# The exact rational kernel of two-column GL3 tests + +For G=GL_3(F2) acting on rational or complex payloads, the action on two +point columns has image dimension **150** and kernel dimension **18**. +Its entire kernel is generated by the explicit central element + + E = 6[1] - 2 sum_(order g=2) [g] + + 2 sum_(order g=4) [g] - sum_(order g=7) [g]. + +The exact identities are E^2=56E and ker(rho_2)=Q[G]E, where +rho_f([g])=P_g^{tensor f}. A restored two-register word is formally +(x,y) -> (x+E y,y), yet is identity on every input at widths one and two. +At width three it has an explicit witness with 112 nonzero output entries. +The third-column regular orbit recovers every formal coefficient. + +This is a **scoped algebraic proof with an exhaustive finite certificate**, +not a complete complex unit, supplier admission or new kappa. The added +information is the complete characteristic-zero kernel and a literal +restored witness for the finite-testing interface. [PROOF.md](PROOF.md) +gives the argument without relying on a character table. + +## Why this question matters + +Small tensor-width tests can accept a formal endpoint with a hidden cross-role +coupling. ywz65's [#2599](https://github.com/CrocSwap/integer-mult-bounds/pull/2599) +proved the sharp stream boundary over F2. Its group norm cancels in +characteristic two. That norm has value 168 at the fixed zero pair over Q, +so it is not this characteristic-zero witness. This package determines +exactly what the two-column Q or C action loses, rather than repeating +the earlier binary-payload result. + +Jacob Alan Sussman's [#4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628) +provides the complex small-unit context and the warning that a fixed tensor +width alone need not certify a uniform program. Woklerx's +[#1440](https://github.com/CrocSwap/integer-mult-bounds/pull/1440) supplies a +different support-bound finite quotient criterion. Their results and executables +are cited, not audited or replayed here. Three-column faithfulness in this +note concerns only the address algebra, not words containing paid C-calls +or phase letters. + +## Evidence and reproduction + +From the repository root, use the available CPython 3.12 interpreter: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gl3-rational-two-column-kernel/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gl3-rational-two-column-kernel/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gl3-rational-two-column-kernel +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gl3-rational-two-column-kernel --check-source-history +``` + +The first line of direct verifier output is + +```text +PASS_GL3_RATIONAL_TWO_COLUMN_KERNEL group=168 image=150 kernel=18 E_squared=56E support=112 dirty_columns=144 no_new_kappa +``` + +The following JSON is a generated receipt binding the six package files by +SHA256. It records the complete modular minor, exact counts and controls. +An optional `--receipt /new/path.json` creates that receipt exclusively. +The verifier otherwise writes nothing and needs only the standard library. + +It constructs the group independently from binary columns and elementary +row additions, checks all 168 convolution coordinates and all 4,096 entries +of the two-column annihilator, and recomputes a nonzero 150 by 150 minor +modulo the checked prime 65537. The idempotent trace supplies the matching +18-dimensional kernel. The chronological shear is replayed on all 144 +dirty input columns at widths one and two and on its width-three witness. +Omitting each of the four nonzero order classes is rejected. The group norm +is checked to be visible over Q. The proof does not use a modular upper rank +as an upper rank over Q. + +The base is canonical main `624de9dc66858af0945e5f8a0942488d62280d43`, priority +revision 7. The card `complex-rank-shape-decoder` changes to this interface +side result. [TASK.json](TASK.json) records the reason, overlap coverage and +remaining questions. The catalogue and selected record are historical +provenance in [SOURCES.json](SOURCES.json), with no external live replay inputs. + +## Limitations + +No paid-call optimum, phase-letter identity, complete engine test, physical +movement, precision, restoration price, compiler, stock or outer bound is +provided. The algebraic word restores arbitrary dirt, but its physical invoice +is unknown. No Lean build or full selected construction replay was run. +The selected source-binding orientation command was attempted and stopped +because the sparse checkout omits `research/fresh-helper-thinned/PROOF.md`. +That is not a failed scientific check of this package or of its predecessor. +Independent human and formal proof-kernel review are unclaimed. + +The bounded verifier deliberately uses managed Python allocations. All +collection sizes follow from the fixed 168-element group, matrices of order +at most 168, and payload replays with at most 512 address rows and 128 input +columns per register. It has +no recursion, network access or unbounded search. Invariant failures use +explicit exceptions and remain enabled under optimization. + +## Open next questions + +1. Determine the characteristic-zero kernel for three-dimensional affine + address maps at their last unfaithful width. This would identify another + precise finite-test blind spot. Start with orbit-stabilizer data and an + exact permutation Gram minor. The group size and certificate cost grow. +2. For a fixed small-unit candidate containing paid calls or phases, identify + a sufficient tensor width or a formal algebra certificate. Start by pinning + the actual generated operator algebra. The GL3 address-only proof does not + cover those extra operators. + +## Credit + +This contribution was produced by Nick Petalas. Credit ywz65 for the binary +stream faithfulness question and regular-orbit argument, Josie Elliston and +Hanson Sun for the related GL3 register census context, Gareth Davidson for +the earlier binary norm alias, woklerx for finite-address certification, +and Jacob Alan Sussman for the complex small-unit model and width warning. +Eumemic and Swapnil Jain retain credit for the underlying obstruction +program cited by Sussman. Regular orbits, idempotent trace and modular-minor +rank arguments are standard linear algebra. No literature-priority claim +is made for those methods. New work is Apache-2.0. diff --git a/research/gl3-rational-two-column-kernel/SOURCES.json b/research/gl3-rational-two-column-kernel/SOURCES.json new file mode 100644 index 0000000000..cb9595ae30 --- /dev/null +++ b/research/gl3-rational-two-column-kernel/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/binary-stream-faithfulness/README.md", + "usage": "provenance", + "git_blob": "a471c1ee89c64c8d2eae5fa0f7bfccd8d3d726bb", + "sha256": "0b5f45d882980038ced16e66cdd4e7d8869c5ca2032e988a5df636df05cb6b12" + }, + { + "path": "research/bit-faithful-finite-address/README.md", + "usage": "provenance", + "git_blob": "0f3c0ded3e2ec8af5e50d9919784cde88ab29bb4", + "sha256": "b4e345bc8e86d069979a57ade7cb381812474ffbb0d7033d5a1283fc99eb16cb" + } + ] +} diff --git a/research/gl3-rational-two-column-kernel/TASK.json b/research/gl3-rational-two-column-kernel/TASK.json new file mode 100644 index 0000000000..2f12a3e66a --- /dev/null +++ b/research/gl3-rational-two-column-kernel/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the full characteristic-zero kernel of the two-column GL3(F2) address action, with an explicit restored shear witness.", + "scope_change_reason": "The card asks for improved decoder child ranks. This is a self-contained interface obstruction for finite tests of complex small units, before a complete decoder or paid profile exists.", + "bottleneck_link": "A two-column address test can miss an 18-dimensional formal coupling. The exact kernel distinguishes finite endpoint evidence from a uniform address-algebra identity; it provides no improved paid invoice.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact kernel formula, matching finite rank certificate and restored witness.", + "outcome": "completed", + "evidence": "Integer convolution E^2=56E; all 4096 two-column action entries vanish; a nonzero order-150 Gram minor modulo 65537; idempotent trace 18; full dirty-input word replay at widths one and two and a regular-orbit witness at width three.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the characteristic-zero kernel of the AGL3(F2) action at its last unfaithful width?", + "why_it_matters": "It would give an exact finite-test obstruction for shared affine offsets.", + "first_step": "Enumerate orbit-stabilizer data and construct an exact permutation Gram certificate.", + "blocked_by": "Larger group and rank-certificate cost." + }, + { + "question": "What finite tensor width suffices for one pinned complex unit including phases and paid calls?", + "why_it_matters": "The address-only threshold does not certify the full engine.", + "first_step": "Pin the generated operator algebra and identify a faithful tensor representation.", + "blocked_by": "Additional operators and central phases require a different proof." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132821", + "overlap": { + "open_pr_snapshot": "2026-10-22T21:14:30Z", + "open_pr_records": 348, + "discussion_snapshot": "2026-10-22T21:15:16Z", + "discussion_records": 3788, + "local_notes_searched": 65, + "local_head_note_paths": 6319, + "limitations": "Sparse local search; no arbitrary diffs or unpublished work. Distinctive tracked main README and merged PR searches were also used." + }, + "predecessors": [ + { + "pr": 2599, + "author": "ywz65", + "head": "cfafdd633cf4e2e534704ec3ddd684cb0c32734f", + "use": "binary-payload boundary and standard regular-orbit argument, not replayed" + }, + { + "pr": 1440, + "author": "woklerx", + "use": "different finite-address certification criterion, not replayed" + }, + { + "pr": 4628, + "author": "Jacob Alan Sussman", + "head": "ee4fd87f064017c23e5a86fc1dcfe0a5237caed3", + "use": "complex small-unit context and tensor-width warning, not replayed" + } + ], + "claim_type": "scoped proof with exhaustive finite certificate" +} diff --git a/research/gl3-rational-two-column-kernel/VERIFY.json b/research/gl3-rational-two-column-kernel/VERIFY.json new file mode 100644 index 0000000000..ac7ad0e7ea --- /dev/null +++ b/research/gl3-rational-two-column-kernel/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": 120, + "checks": "Exact group algebra identity, complete two-column annihilator, nonzero rank minor, full dirty word replay and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact certificate and controls with Python assertions disabled." + } + ] +} diff --git a/research/gl3-rational-two-column-kernel/verify.py b/research/gl3-rational-two-column-kernel/verify.py new file mode 100644 index 0000000000..fc4770490b --- /dev/null +++ b/research/gl3-rational-two-column-kernel/verify.py @@ -0,0 +1,257 @@ +#!/usr/bin/env python3 +"""Exact characteristic-zero GL3 two-column kernel. Apache-2.0.""" +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +N = 8 +SIZE = 168 +PRIME = 65537 +IDENTITY = tuple(range(N)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def compose(a, b): + return tuple(a[b[x]] for x in range(N)) + + +def from_columns(columns): + return tuple(columns[0] * (x & 1) ^ columns[1] * ((x >> 1) & 1) + ^ columns[2] * ((x >> 2) & 1) for x in range(N)) + + +def construct_group(): + candidates = (from_columns(c) for c in product(range(1, N), repeat=3)) + group = sorted(g for g in candidates if len(set(g)) == N) + require(len(group) == SIZE and len(set(group)) == SIZE, "GL3 order") + # A second construction starts from elementary binary row additions. + generators = [tuple(x ^ (((x >> j) & 1) << i) for x in range(N)) + for i in range(3) for j in range(3) if i != j] + reached, queue = {IDENTITY}, [IDENTITY] + for index in range(SIZE): + require(index < len(queue), "premature generator closure") + for generator in generators: + value = compose(generator, queue[index]) + if value not in reached: + reached.add(value) + queue.append(value) + require(len(queue) <= SIZE, "generator closure exceeded GL3") + require(reached == set(group), "independent group constructions disagree") + labels = {g: i for i, g in enumerate(group)} + table = [[labels[compose(a, b)] for b in group] for a in group] + return group, table, labels[IDENTITY] + + +def element_orders(table, one): + orders = [] + for g in range(SIZE): + current = one + for exponent in range(1, SIZE + 1): + current = table[current][g] + if current == one: + orders.append(exponent) + break + else: + raise ValueError("element order exceeds group order") + require(Counter(orders) == {1: 1, 2: 21, 3: 56, 4: 42, 7: 48}, + "unexpected order populations") + return orders + + +def convolution(a, b, table): + require(len(a) == len(b) == SIZE, "group algebra vector size") + result = [0] * SIZE + for i in range(SIZE): + for j in range(SIZE): + result[table[i][j]] += a[i] * b[j] + return result + + +def action(coefficients, group, width): + require(width in (1, 2), "full action is bounded to widths one and two") + points = tuple(product(range(N), repeat=width)) + labels = {point: i for i, point in enumerate(points)} + matrix = [[0] * len(points) for _ in points] + for g, coefficient in zip(group, coefficients, strict=True): + for column, point in enumerate(points): + row = labels[tuple(g[x] for x in point)] + matrix[row][column] += coefficient + return matrix + + +def is_zero(matrix): + return not any(any(row) for row in matrix) + + +def certify_element(coefficients, group, table): + require(convolution(coefficients, coefficients, table) + == [56 * c for c in coefficients], "E squared differs from 56 E") + require(is_zero(action(coefficients, group, 2)), "nonzero two-column action") + # Check centrality directly, independently of the order-class argument. + for g in range(SIZE): + left, right = [0] * SIZE, [0] * SIZE + for h in range(SIZE): + left[table[g][h]] += coefficients[h] + right[table[h][g]] += coefficients[h] + require(left == right, "E is not central") + + +def modular_pivots(matrix): + require(len(matrix) == SIZE and all(len(row) == SIZE for row in matrix), + "Gram matrix shape") + require(all(PRIME % divisor for divisor in range(2, 257)), "modulus not prime") + work = [[x % PRIME for x in row] for row in matrix] + labels = list(range(SIZE)) + pivot_rows, pivot_columns = [], [] + for column in range(SIZE): + rank = len(pivot_columns) + pivot = next((i for i in range(rank, SIZE) if work[i][column]), None) + if pivot is None: + continue + work[rank], work[pivot] = work[pivot], work[rank] + labels[rank], labels[pivot] = labels[pivot], labels[rank] + pivot_rows.append(labels[rank]) + pivot_columns.append(column) + scale = pow(work[rank][column], -1, PRIME) + work[rank] = [(x * scale) % PRIME for x in work[rank]] + for i in range(rank + 1, SIZE): + factor = work[i][column] + if factor: + work[i] = [(a - factor * b) % PRIME + for a, b in zip(work[i], work[rank], strict=True)] + return pivot_rows, pivot_columns + + +def minor_determinant(matrix, rows, columns): + require(len(rows) == len(columns) == 150, "rank certificate must have order 150") + work = [[matrix[i][j] % PRIME for j in columns] for i in rows] + determinant = 1 + for j in range(150): + pivot = next((i for i in range(j, 150) if work[i][j]), None) + require(pivot is not None, "zero rank-certificate determinant") + if pivot != j: + work[j], work[pivot] = work[pivot], work[j] + determinant = -determinant + diagonal = work[j][j] + determinant = determinant * diagonal % PRIME + inverse = pow(diagonal, -1, PRIME) + for i in range(j + 1, 150): + factor = work[i][j] * inverse % PRIME + work[i] = [(a - factor * b) % PRIME + for a, b in zip(work[i], work[j], strict=True)] + require(determinant != 0, "zero minor") + return determinant + + +def replay_shear(group, coefficients, width, full_basis): + require(width in (1, 2, 3) and (not full_basis or width <= 2), "replay bound") + points = tuple(product(range(N), repeat=width)) + labels = {point: i for i, point in enumerate(points)} + size = len(points) + if full_basis: + target = [[int(i == j) for j in range(2 * size)] for i in range(size)] + source = [[int(size + i == j) for j in range(2 * size)] for i in range(size)] + else: + target = [[0] for _ in points] + source = [[int(point == (1, 2, 4))] for point in points] + initial_source = [row[:] for row in source] + for g, coefficient in zip(group, coefficients, strict=True): + if coefficient == 0: + continue + permutation = [labels[tuple(g[x] for x in point)] for point in points] + moved = [None] * size + for old, new in enumerate(permutation): + moved[new] = source[old] + require(all(row is not None for row in moved), "source permutation") + for i in range(size): + target[i] = [a + coefficient * b + for a, b in zip(target[i], moved[i], strict=True)] + # Undo the address map on the source after every addition. + source = [moved[new] for new in permutation] + require(source == initial_source, "dirty source not restored") + if full_basis: + expected = [[int(i == j) for j in range(2 * size)] for i in range(size)] + require(target == expected, "shear is visible below width three") + else: + expected = [0] * size + for g, coefficient in zip(group, coefficients, strict=True): + expected[labels[(g[1], g[2], g[4])]] += coefficient + require([row[0] for row in target] == expected, "width-three shear witness") + require(sum(value != 0 for value in expected) == 112, "witness support") + return 2 * size if full_basis else 1 + + +def failure_controls(coefficients, orders, group, table): + rejected = 0 + for order in (1, 2, 4, 7): + changed = [0 if n == order else c + for c, n in zip(coefficients, orders, strict=True)] + try: + certify_element(changed, group, table) + except ValueError: + rejected += 1 + else: + raise ValueError("omitted class was accepted") + norm = action([1] * SIZE, group, 2) + require(norm[0][0] == SIZE and not is_zero(norm), "characteristic-zero norm control") + return {"omitted_classes_rejected": rejected, "group_norm_at_fixed_pair": norm[0][0]} + + +def verify(): + group, table, one = construct_group() + orders = element_orders(table, one) + coefficients = [{1: 6, 2: -2, 3: 0, 4: 2, 7: -1}[n] for n in orders] + certify_element(coefficients, group, table) + require(is_zero(action(coefficients, group, 1)), "width-one action") + regular_orbit = {(g[1], g[2], g[4]) for g in group} + require(len(regular_orbit) == SIZE, "width three lacks a regular orbit") + gram = [[sum(a[x] == b[x] for x in range(N)) ** 2 for b in group] + for a in group] + rows, columns = modular_pivots(gram) + require(len(rows) == len(columns) == 150, "two-column Gram rank") + determinant = minor_determinant(gram, rows, columns) + ideal_dimension, remainder = divmod(SIZE * coefficients[one], 56) + require(remainder == 0 and ideal_dimension == 18, "idempotent trace") + require(150 + ideal_dimension == SIZE, "kernel/image dimensions") + replay_columns = [replay_shear(group, coefficients, f, True) for f in (1, 2)] + replay_shear(group, coefficients, 3, False) + return { + "group_order": SIZE, "order_populations": dict(sorted(Counter(orders).items())), + "annihilator_class_coefficients": {"1": 6, "2": -2, "3": 0, "4": 2, "7": -1}, + "scale": 56, "kernel_dimension": ideal_dimension, "action_rank": 150, + "annihilator_support": sum(c != 0 for c in coefficients), + "minor_prime": PRIME, "minor_rows": rows, "minor_columns": columns, + "minor_determinant_mod_prime": determinant, + "complete_dirty_replay_columns": replay_columns, + "width_three_witness_support": 112, + "controls": failure_controls(coefficients, orders, group, table), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="exclusively create a hash-bound receipt") + args = parser.parse_args() + result = verify() + 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} + receipt = {"schema": "gl3-rational-two-column-kernel/v1", "result": result, + "source_sha256": hashes} + if args.receipt: + with args.receipt.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(receipt, indent=2, sort_keys=True) + "\n") + print("PASS_GL3_RATIONAL_TWO_COLUMN_KERNEL group=168 image=150 kernel=18 " + "E_squared=56E support=112 dirty_columns=144 no_new_kappa") + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()