diff --git a/research/all-group-diagonal-rank/PROOF.md b/research/all-group-diagonal-rank/PROOF.md new file mode 100644 index 0000000000..62714b57d1 --- /dev/null +++ b/research/all-group-diagonal-rank/PROOF.md @@ -0,0 +1,144 @@ +# Diagonal group targets have exact scalar-rank cost + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped written algebraic proof with exact finite corroboration. + +## Model and statement + +Let K be any field and G any group, finite or infinite, with identity e. +Work coefficientwise in the full formal group algebra K[G]. Every matrix +has finite support. A free operation is a fixed scalar K-linear map, with +address action [e]. Free maps may be rectangular or singular and may copy, +reset or discard scalar registers. The schedule is finite and fixed. + +A paid gate on r registers is + +```text +D(N,g) = I_r[e] + N([g]-[e]), N in M_r(K), N^2=N. +``` + +Its scalar-rank charge is rank_K N. Rank-one call count is the same charge +when every paid projector has rank one. Initial scalar embeddings of data +and clean helpers, and final selections of retained outputs, are free maps. +Arbitrary dirty inputs may also be supplied. Retained data outputs must be +correct for every such input. Restoration of additional outputs is optional +for the lower bound; the attaining construction restores them. + +**Theorem.** Suppose the retained independent data outputs implement +diag([t_1],...,[t_m]) on their m independent data inputs. Let +d = |{i : t_i != e}|, counting repetitions by position. Then every such +circuit has total paid scalar rank at least d. If every nonidentity target +label t_i is in the paid alphabet, its exact minimum scalar-rank charge +and exact minimum rank-one call count are both d. + +The lower bound holds for an arbitrary paid alphabet and does not use +idempotence. The equality statement requires the target-label availability +just specified. It is not a word-length theorem for a restricted generating +alphabet. + +This answers the four-or-more-target question in Ali Romman's +[#5394](https://github.com/CrocSwap/integer-mult-bounds/pull/5394) for every +group and field in its formal model. That package's arbitrary-rank, +unit-price invocation optimum remains its ordered-subproduct cover number. +Consequently rank-one count exceeds that invocation optimum exactly when +the cover number is less than d. We cite the cover theorem; we do not +re-prove or replay it. + +## One common scalar image space + +For a rectangular formal matrix M = sum_g M_g[g], define + +```text +U(M) = sum_{g != e} col_K(M_g), +c(M) = dim_K U(M). +``` + +All coefficient images are subspaces of the same scalar output space. +This is a sum of subspaces, rather than a sum of the individual ranks. +Its dimension counts repeated output directions correctly even when many +targets have the same group label. + +Write epsilon(M) = sum_g M_g for augmentation. The coefficient images of +M-epsilon(M)[e] span exactly U(M): its nonidentity coefficients are M_g, +and its identity coefficient is -sum_{g != e} M_g. + +**Lemma.** For compatible rectangular formal matrices A and B, + +```text +U(AB) is contained in U(A) + epsilon(A) U(B), +c(AB) <= c(A) + c(B). +``` + +**Proof.** Augmentation is multiplicative, since summing every ordered +coefficient product gives epsilon(A) epsilon(B). Thus + +```text +AB-epsilon(A)epsilon(B)[e] + = (A-epsilon(A)[e]) B + + epsilon(A)[e] (B-epsilon(B)[e]). +``` + +Every coefficient of the first summand is a sum of scalar matrix products +A'_g B_h, with col(A'_g) contained in U(A). Its columns therefore lie in +U(A). Every coefficient of the second summand has columns in +epsilon(A) U(B). Taking the sum of coefficient images proves containment. +The image of a linear map cannot increase dimension, proving the rank +inequality. No commutation of group labels, inverse of a free map or +restriction on the group order was used. QED. + +A free scalar map has c=0. For g != e, the gate coefficients at e and g +are I-N and N. After subtracting augmentation I, they are -N and N, so +c(D(N,g))=rank N. For g=e the gate is identity and has c=0, which is at +most its declared rank charge. Iterating the lemma through the entire +rectangular circuit gives c(M) <= sum_j rank N_j. + +Equivalently, in matrix order write the retained data block as +C_0 D_1 C_1 ... D_k C_k. Expand by the leftmost paid perturbation. +The scalar image of each resulting term lies in +col(C_0 C_1 ... C_(j-1) N_j). The sum of these k scalar spaces has dimension +at most sum_j rank N_j and contains every nonidentity output coefficient. +This equivalent expansion explains the transported-image test in verify.py. + +## Apply the bound and attain it + +Select the retained data-output rows and the independent data-input columns +of the circuit. The endpoint maps in that selection are scalar, so the +same bound applies to the resulting m-by-m matrix T. This argument allows +arbitrary dirty workspace and arbitrary discarded garbage without assigning +them zero cost or assuming their input values vanish. + +For each g != e, the coefficient T_g is diagonal, with a one in position i +exactly when t_i=g. Its column space is the span of the corresponding +coordinate axes. Summing over g != e gives precisely the d active axes. +Thus c(T)=d, proving the lower bound. + +For the upper bound, apply one gate D(E_ii,t_i) to each active position i. +The projectors have rank one and commute because they act on separate +scalar registers. Their product is the required diagonal target. They +touch no helper and restore all dirty spectators. There are exactly d +gates and d total rank units. This also covers d=0 by the empty word. QED. + +## Scope and predecessor credit + +Ali Romman's #5394 supplies the model, cover theorem, three-label result +and open question. The scalar coefficient-image method has precedent in +Arham Tahir's #1919 and in the image-span reduction retained in +research/bit-clean-workspace-compression. We claim the arbitrary-group +application, the rectangular common-image proof and the complete answer +to #5394's rank-one question, not invention of coefficient-span methods. + +Nick Petalas's older #6008 gives a representation-rank cut and proves the +same d value for prime-exponent groups, with a coprime cyclic-character +remark. Krzysztof Wojt's #5242 gives the mixed-target binary semilinear +case. Those restricted consequences are prior work. No predecessor +scientific verifier is run here. SOURCES.json pins the retained sources +used for the argument and context. + +Formal coefficientwise equality is essential. A representation faithful on +group elements can still kill nonzero linear combinations. Free +address-dependent maps and data-dependent control are outside this model. +The theorem prices scalar projector rank, not physical address action, +native realization, frame conversion, precision, tape movement, hosting, +restoration overhead or a complete supplier invoice. No new kappa or +selected-frontier change follows. Independent human and formal proof-kernel +review are unclaimed. diff --git a/research/all-group-diagonal-rank/README.md b/research/all-group-diagonal-rank/README.md new file mode 100644 index 0000000000..63b78db0b9 --- /dev/null +++ b/research/all-group-diagonal-rank/README.md @@ -0,0 +1,141 @@ +# Every group diagonal has exact scalar-rank cost d + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped written algebraic proof with exact finite corroboration. + +In Ali Romman's [#5394](https://github.com/CrocSwap/integer-mult-bounds/pull/5394) +formal group-gate model, let d count the nonidentity entries of a diagonal +target, with repetitions counted by position. For every field and every +group, finite or infinite, + +```text +minimum total projector rank = minimum rank-one call count = d. +``` + +Equality assumes each target label is an allowed paid label. The lower +bound needs no such assumption. Arbitrary finite scalar workspace, +rectangular or singular free scalar maps, copying, reset and discarded +garbage do not lower the bound. Dirty inputs may be arbitrary; the attaining +coordinate construction restores them. + +[PROOF.md](PROOF.md) proves that all nonidentity coefficient images of a +circuit lie in one scalar space of dimension at most the total paid rank. +The diagonal target needs exactly d scalar directions. No finite group +representation, characteristic assumption or inverse free map enters the +proof. The lower bound even permits nonidempotent paid couplings. + +This closes #5394's four-or-more-target rank-one question. Its unit-price, +arbitrary-rank invocation optimum remains the credited subproduct-cover +number. Rank-one count exceeds that optimum exactly when the cover number +is below d. The prime-exponent and coprime cyclic cases of Nick Petalas's +older #6008, and the binary semilinear case of Krzysztof Wojt's #5242, +retain their prior credit. We do not replay those results. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/all-group-diagonal-rank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -X dev -B research/all-group-diagonal-rank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/all-group-diagonal-rank +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/all-group-diagonal-rank --check-source-history +``` + +Another CPython 3.12 path can replace the absolute local path. The direct +command prints `PASS_ALL_GROUP_DIAGONAL_RANK` inside a generated JSON +receipt bound to all six package-file hashes. Both registered commands run +the full finite corroboration. The publication check requires the committed +package and full history. No receipt is handwritten or stored as an input. + +The checker constructs new circuits over C4, C6 and S3, over F2, F3 and F5. +It checks the transported common image, the rank charge and the complete +regular-action matrix against separate ordinary matrix multiplication. +A literal enumeration of all row combinations independently checks every +circuit's coefficient rank. Direct diagonal words include repeated labels, +identity targets, the three-copy order-two target in C4, and two arbitrary +restored dirty roles. Normal and optimized execution use explicit exceptions. +The receipt reports the executed counts. These finite checks corroborate +the written proof; they do not establish its universal quantifiers alone. + +Local CPython 3.12.15 runs pass 216 new circuits with 540 paid gates, +561 rectangular free maps and 79 singular square free maps. All 57,024 +regular-matrix entries agree, and 133 circuits have positive coefficient +rank. The 54 direct endpoint fixtures cover 1,512 regular basis columns, +including 36 fixtures with repeated labels. These counts include fixture +occurrences rather than distinct maps across the complete run. + +Eight controls distinguish repeated positions from distinct labels, +unit-price invocations from rank charges, forbidden free address maps, +free singular scalar maps, invalid idempotents, noncommutative order, +omitted calls and characteristic-two cancellation. The fixed seeded circuits +are probes, not an exhaustive search of circuit words. + +## Sources and scope + +Base is canonical main `e54523517d0f03e58352e647c403a5af3e525a57`, priority +revision 8, selected #7000 unchanged. The selected source-binding baseline +passed with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. It was orientation only. +[TASK.json](TASK.json) records the change from the bit-new-register-model +card to this formal all-group side result. [SOURCES.json](SOURCES.json) +contains provenance-only pins; the verifier has no external scientific inputs. + +Ali Romman #5394 supplies the model, cover theorem, triple result and open +question. The coefficient-span method has precedent in Arham Tahir #1919 +and the retained clean-workspace image-span reduction. Preserve the group +model lineage of Cinna Davis, JoyboyBrian and their cited register-model +predecessors. The new contribution is the rectangular common-image proof +and its complete arbitrary-group application, not a new general invention +of coefficient-span methods. Predecessor scientific suites are not replayed. + +The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540700) +precedes the new verifier. Main and merged object/formula searches, open PR +bodies, recent account work, active Discussions and local reservations were +checked. The overlap cache covers 502 open PRs and 7,179 Discussion records; +its local note coverage is sparse. All-main Git searches cover the relevant +omitted README texts. These are bounded overlap checks, not proof of novelty +against unpublished work or every historical diff. + +Formal coefficientwise equality, fixed schedules and scalar free maps are +essential. A quotient address representation, free address operation or +data-dependent control changes the model. This result prices no native +group action, physical caller, frame conversion, source access, precision, +tape movement, hosting or complete recursive invoice. No new kappa, +supplier admission or selected-frontier change is claimed. Selected cold +replay, Lean and Docker are unrun. Independent human and formal proof-kernel +review are unclaimed. + +## Code constraints + +The standalone checker has no recursion, subprocess, network call or file +mutation. Circuit widths are at most four, words have at most four gates, +groups have at most six elements, and the row-space oracle has at most +three rows and 125 combinations. Diagonal fixtures have at most seven +registers including the two dirty roles, so regular matrices have at most +42 rows and columns. All functions are shorter than sixty physical lines. +Every loop ranges over these fixed domains or a collection they bound. + +Power of Ten rule 3 has a managed-allocation deviation for this one-shot +CPython checker. Live state is bounded by the displayed shapes, at most +six coefficient matrices per formal product, and one row-space set of at +most 125 vectors. Runtime and standard-library allocation cannot be fixed +statically. A deployment requiring allocation-free operation would need +fixed buffers; this verifier claims no such deployment. Warning-strict +development-mode normal and optimized checks provide runtime diagnostics. +The rank-elimination and literal-row-space algorithms are separate. +Source compilation and function-size inspection are part of local checks. + +## Open next questions + +Can a specified native address quotient escape this formal coefficient +bound and still improve the complete supplier bill? Begin with one exact +representation and a new target whose formal coefficient images collapse +in that representation. A paid native implementation, dirty restoration, +precision and complete caller charges remain the blockers. The current +theorem does not price such a quotient or reserve a follow-up. + +For a fixed rank cap and positive invocation overhead, which subproduct +covers minimize the full rank and invocation bill together? Begin with one +four-target mixed-order example and retain both charges for each gate. +The present d bound and the predecessor's invocation optimum need not be +attained by the same word. Physical realization remains separate. diff --git a/research/all-group-diagonal-rank/SOURCES.json b/research/all-group-diagonal-rank/SOURCES.json new file mode 100644 index 0000000000..379616d5ec --- /dev/null +++ b/research/all-group-diagonal-rank/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-clean-workspace-compression/README.md", + "usage": "provenance", + "git_blob": "bd752384cc1061d912bbb49c970ba4a4d8aef00d", + "sha256": "ca2cc91629ccb36475cd38f9d8c13719d3b2742d96080653b545a45b5d991885" + }, + { + "path": "research/group-subproduct-cover/PROOF.md", + "usage": "provenance", + "git_blob": "308e63dcc668b0089b4a0c5152dda0733b01fed5", + "sha256": "7392dca9e7258dcdb4802a3c9f60cd8e5ccced271950a4ce2e4823f449586c00" + }, + { + "path": "research/group-subproduct-cover/README.md", + "usage": "provenance", + "git_blob": "36faba920c546d36f3a51a026e8e84d925acf723", + "sha256": "b9241c29301d2d20af35fe9f09ff2b0e7e7aca0566394b8e4c7708924e59d161" + }, + { + "path": "research/prime-exponent-rank-cut/README.md", + "usage": "provenance", + "git_blob": "a23cf9be5d5ec8b258156b7925a9349fe6bef8b3", + "sha256": "4e1936de8546a3ac91f58cb5176f11a2b35d7a1093814794b35622bd97347db7" + }, + { + "path": "research/ut3-rank-bounded-block-calls/README.md", + "usage": "provenance", + "git_blob": "dc0d1bac91fcebecc9fed4e8c3d26a11acca3ef5", + "sha256": "822574c7040b5571d729960951425a1ad9742ae8541a2af2882733f952975b5d" + }, + { + "path": "research/semilinear-mixed-tariff/README.md", + "usage": "provenance", + "git_blob": "dc95473ba57ec799194c33fc030f1f82dba484d2", + "sha256": "edecd78f1ab2661ac4115c09cd7b47d06274672f4a6a7a20202d9b5812a84c80" + } + ] +} diff --git a/research/all-group-diagonal-rank/TASK.json b/research/all-group-diagonal-rank/TASK.json new file mode 100644 index 0000000000..e41658c46f --- /dev/null +++ b/research/all-group-diagonal-rank/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Prove exact total scalar-projector-rank cost d for d nonidentity diagonal entries over every field and group, with arbitrary finite scalar workspace and singular or rectangular free maps. When target labels are allowed, rank-one count is also exactly d.", + "scope_change_reason": "Take the four-or-more-target question in Ali Romman PR5394 rather than rerun the historical three-register model. This is a formal obstruction, without a native implementation or paid supplier invoice.", + "bottleneck_link": "Rules out cross-register reductions of scalar-rank mass for independent formal group-label targets even in mixed-order and nonabelian models. Invocation savings at arbitrary rank still need a complete physical bill.", + "budget_minutes": 60, + "stop_rule": "Ship the common coefficient-image theorem after bounded finite corroboration; do not extend to a native quotient or optimize another tariff.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-group/all-field argument. verify.py checks new rectangular and singular circuits, independent regular-action products, literal row-space ranks and all-input direct diagonal words. No predecessor scientific verifier is replayed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a native address quotient escape the formal coefficient-image bound with a favorable complete supplier invoice?", + "why_it_matters": "Formal group-algebra independence may overstate the constraints in a concrete native quotient.", + "first_step": "Specify one exact representation and a new target with collapsed formal coefficient images; price the native word.", + "blocked_by": "A paid native implementation, restoration, precision and complete caller charges." + }, + { + "question": "Which rank-capped cover minimizes combined invocation and scalar-rank charges for a fixed mixed-order target?", + "why_it_matters": "The separate minimum invocation and rank bounds need not have a common attaining word.", + "first_step": "Choose one four-target mixed-order example and retain both charges at every gate.", + "blocked_by": "A concrete paid primitive and its complete invocation/rank tariff." + } + ] +} diff --git a/research/all-group-diagonal-rank/VERIFY.json b/research/all-group-diagonal-rank/VERIFY.json new file mode 100644 index 0000000000..295aa9d2de --- /dev/null +++ b/research/all-group-diagonal-rank/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-X", + "dev", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New full formal/regular circuit products, transported coefficient-image containment, literal row-space rank oracle, direct dirty-restoring diagonal endpoints and eight controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-X", + "dev", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New full formal/regular circuit products, transported coefficient-image containment, literal row-space rank oracle, direct dirty-restoring diagonal endpoints and eight controls." + } + ] +} diff --git a/research/all-group-diagonal-rank/verify.py b/research/all-group-diagonal-rank/verify.py new file mode 100644 index 0000000000..ede2d9c992 --- /dev/null +++ b/research/all-group-diagonal-rank/verify.py @@ -0,0 +1,312 @@ +"""Exact coefficient-image corroboration, produced by Nick Petalas. Apache-2.0.""" + +import hashlib +import itertools +import json +from pathlib import Path +import platform +import random + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def zeros(rows, cols): + return [[0] * cols for _ in range(rows)] + + +def identity(size): + return [[int(i == j) for j in range(size)] for i in range(size)] + + +def add(left, right, prime, sign=1): + return [[(x + sign * y) % prime for x, y in zip(a, b)] + for a, b in zip(left, right)] + + +def multiply(left, right, prime): + need(len(left[0]) == len(right), "incompatible matrix shapes") + return [[sum(x * y for x, y in zip(row, col)) % prime + for col in zip(*right)] for row in left] + + +def rank(matrix, prime): + work = [row[:] for row in matrix] + pivot = 0 + for col in range(len(work[0])): + found = next((i for i in range(pivot, len(work)) if work[i][col]), None) + if found is None: + continue + work[pivot], work[found] = work[found], work[pivot] + scale = pow(work[pivot][col], -1, prime) + work[pivot] = [(x * scale) % prime for x in work[pivot]] + for i in range(len(work)): + if i != pivot: + factor = work[i][col] + work[i] = [(x - factor * y) % prime + for x, y in zip(work[i], work[pivot])] + pivot += 1 + if pivot == len(work): + break + return pivot + + +def concatenate(matrices): + return [list(itertools.chain.from_iterable(rows)) for rows in zip(*matrices)] + + +def rowspace_rank(matrix, prime): + need(1 <= len(matrix) <= 3, "row-space oracle bound") + span = {tuple(sum(c * row[j] for c, row in zip(coefficients, matrix)) % prime + for j in range(len(matrix[0]))) + for coefficients in itertools.product(range(prime), repeat=len(matrix))} + dimensions = [d for d in range(len(matrix) + 1) if prime ** d == len(span)] + need(len(dimensions) == 1, "row space is not a prime power") + return dimensions[0] + + +def inverse(matrix, prime): + size = len(matrix) + work = concatenate([matrix, identity(size)]) + for col in range(size): + found = next((i for i in range(col, size) if work[i][col]), None) + need(found is not None, "singular change of basis") + work[col], work[found] = work[found], work[col] + scale = pow(work[col][col], -1, prime) + work[col] = [(x * scale) % prime for x in work[col]] + for i in range(size): + if i != col: + factor = work[i][col] + work[i] = [(x - factor * y) % prime + for x, y in zip(work[i], work[col])] + return [row[size:] for row in work] + + +def group_tables(): + groups = [] + for size in (4, 6): + groups.append((f"C{size}", [[(i + j) % size for j in range(size)] + for i in range(size)])) + permutations = list(itertools.permutations(range(3))) + table = [[permutations.index(tuple(a[b[i]] for i in range(3))) + for b in permutations] for a in permutations] + groups.append(("S3", table)) + return groups + + +def scalar(matrix): + return {0: matrix} + + +def formal_multiply(left, right, table, prime): + rows = len(next(iter(left.values()))) + cols = len(next(iter(right.values()))[0]) + result = {g: zeros(rows, cols) for g in range(len(table))} + for g, a in left.items(): + for h, b in right.items(): + label = table[g][h] + result[label] = add(result[label], multiply(a, b, prime), prime) + return result + + +def augmentation(formal, prime): + sample = next(iter(formal.values())) + total = zeros(len(sample), len(sample[0])) + for matrix in formal.values(): + total = add(total, matrix, prime) + return total + + +def coefficient_rank(formal, prime): + sample = next(iter(formal.values())) + columns = [matrix for g, matrix in formal.items() if g != 0] + return rank(concatenate(columns or [zeros(len(sample), 1)]), prime) + + +def gate(projector, label, prime): + size = len(projector) + need(label > 0, "paid identity label") + need(multiply(projector, projector, prime) == projector, "not idempotent") + return {0: add(identity(size), projector, prime, -1), label: projector} + + +def projector(size, chosen_rank, prime, rng): + basis = identity(size) + for _ in range(8): + i, j = rng.randrange(size), rng.randrange(size) + if i != j: + factor = rng.randrange(prime) + basis[i] = [(x + factor * y) % prime + for x, y in zip(basis[i], basis[j])] + diagonal = [[int(i == j and i < chosen_rank) for j in range(size)] + for i in range(size)] + result = multiply(multiply(basis, diagonal, prime), inverse(basis, prime), prime) + need(rank(result, prime) == chosen_rank, "projector rank") + return result + + +def random_matrix(rows, cols, prime, rng): + return [[rng.randrange(prime) for _ in range(cols)] for _ in range(rows)] + + +def regular_matrix(formal, table): + sample = next(iter(formal.values())) + rows, cols, order = len(sample), len(sample[0]), len(table) + result = zeros(rows * order, cols * order) + for g, matrix in formal.items(): + for i, row in enumerate(matrix): + for j, value in enumerate(row): + for address in range(order): + result[i * order + table[g][address]][j * order + address] = value + return result + + +def one_circuit(table, prime, case, rng): + length = 1 + case % 4 + widths = [rng.randrange(1, 5) for _ in range(length)] + free = [random_matrix(3, widths[0], prime, rng)] + free += [random_matrix(a, b, prime, rng) + for a, b in zip(widths, widths[1:])] + free.append(random_matrix(widths[-1], 3, prime, rng)) + value = scalar(free[0]) + literal = regular_matrix(value, table) + prefix, images, budget = free[0], [], 0 + for j, width in enumerate(widths): + chosen = (case + j) % (width + 1) + coupling = projector(width, chosen, prime, rng) + paid = gate(coupling, rng.randrange(1, len(table)), prime) + images.append(multiply(prefix, coupling, prime)) + prefix = multiply(prefix, free[j + 1], prime) + budget += chosen + value = formal_multiply(value, paid, table, prime) + value = formal_multiply(value, scalar(free[j + 1]), table, prime) + literal = multiply(literal, regular_matrix(paid, table), prime) + literal = multiply(literal, regular_matrix(scalar(free[j + 1]), table), prime) + need(augmentation(value, prime) == prefix, "augmentation baseline") + ambient = concatenate(images) + joined = concatenate([ambient] + [a for g, a in value.items() if g]) + need(rank(joined, prime) == rank(ambient, prime), "transported-image containment") + cost = coefficient_rank(value, prime) + need(cost <= budget, "coefficient-image rank exceeds paid rank") + nonidentity = concatenate([a for g, a in value.items() if g]) + need(cost == rowspace_rank(nonidentity, prime), "independent row-space rank") + need(literal == regular_matrix(value, table), "formal/regular circuit disagreement") + return {"circuits": 1, "paid_gates": length, + "regular_entries": len(literal) * len(literal[0]), + "rectangular_free_maps": sum(len(a) != len(a[0]) for a in free), + "singular_square_free_maps": sum(len(a) == len(a[0]) and + rank(a, prime) < len(a) for a in free), + "positive_coefficient_ranks": int(cost > 0)} + + +def circuit_checks(): + rng = random.Random(53941919) + counts = {} + for _, table in group_tables(): + for prime in (2, 3, 5): + for case in range(24): + for key, value in one_circuit(table, prime, case, rng).items(): + counts[key] = counts.get(key, 0) + value + for key in ("rectangular_free_maps", "singular_square_free_maps", + "positive_coefficient_ranks"): + need(counts[key] > 0, "vacuous circuit checks: " + key) + return counts + + +def diagonal(labels, order): + size = len(labels) + result = {g: zeros(size, size) for g in range(order)} + for i, label in enumerate(labels): + result[label][i][i] = 1 + return result + + +def direct_word(labels, table, prime): + size = len(labels) + value = diagonal([0] * size, len(table)) + used = 0 + for i, label in enumerate(labels): + if label != 0: + coupling = zeros(size, size) + coupling[i][i] = 1 + value = formal_multiply(value, gate(coupling, label, prime), table, prime) + used += 1 + return value, used + + +def endpoint_checks(): + counts = {"diagonal_fixtures": 0, "regular_basis_columns": 0, + "repeated_target_fixtures": 0} + for _, table in group_tables(): + targets = [[0, 0], [0, 1], [1, 1, 1], list(range(1, len(table))), + [0, 1, 2, 1, 0], [2, 2, 2]] + for prime in (2, 3, 5): + for labels in targets: + # Two independent dirty roles are retained with identity labels. + complete = labels + [0, 0] + value, cost = direct_word(complete, table, prime) + target = diagonal(complete, len(table)) + need(value == target, "direct all-input diagonal endpoint") + need(coefficient_rank(target, prime) == cost, "sharp diagonal rank") + literal = identity(len(complete) * len(table)) + for i, label in enumerate(complete): + if label: + coupling = zeros(len(complete), len(complete)) + coupling[i][i] = 1 + literal = multiply(literal, regular_matrix( + gate(coupling, label, prime), table), prime) + wanted = regular_matrix(target, table) + need(literal == wanted, "regular endpoint") + counts["regular_basis_columns"] += len(literal[0]) + counts["diagonal_fixtures"] += 1 + counts["repeated_target_fixtures"] += len(set(labels)) < len(labels) + return counts + + +def controls(): + table = group_tables()[2][1] + p = 2 + target = diagonal([1, 1, 1, 1], len(table)) + need(coefficient_rank(target, p) == 4, "repeated labels lost multiplicity") + need(sum(any(any(row) for row in a) for g, a in target.items() if g) == 1, + "distinct-label counting control") + high_rank = gate(identity(3), 1, p) + need(coefficient_rank(high_rank, p) > 1, "unit-price/rank-price distinction") + need(coefficient_rank(diagonal([1, 1], len(table)), p) > 0, + "free address-map exclusion") + need(coefficient_rank(scalar(zeros(3, 3)), p) == 0, "free singular map charged") + rejected = False + try: + gate([[0, 1], [0, 0]], 1, p) + except ValueError: + rejected = True + need(rejected, "invalid projector accepted") + a, b = next((a, b) for a in range(1, 6) for b in range(1, 6) + if table[a][b] != table[b][a]) + left = formal_multiply(gate([[1]], a, p), gate([[1]], b, p), table, p) + right = formal_multiply(gate([[1]], b, p), gate([[1]], a, p), table, p) + need(left != right, "noncommutative order control") + direct, _ = direct_word([a, b], table, p) + omitted, _ = direct_word([a, 0], table, p) + need(direct != omitted, "omitted call control") + scalar_only = formal_multiply(scalar([[1, 1]]), scalar([[1], [1]]), table, p) + need(augmentation(scalar_only, p) == [[0]], "characteristic-two cancellation") + need(coefficient_rank(scalar_only, p) == 0, "scalar cancellation has defect") + return 8 + + +def main(): + counts = circuit_checks() | endpoint_checks() + counts["controls"] = controls() + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() for name in names} + print(json.dumps({"status": "PASS_ALL_GROUP_DIAGONAL_RANK", "counts": counts, + "python": platform.python_version(), "source_sha256": hashes}, + sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()