From c125e0765f0a28f5c3cc2e5d1d599babbcd292ed Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 09:17:19 +0000 Subject: [PATCH] feat(research): prove exact costs for small local products --- .../PROOF.md | 151 ++++++ .../README.md | 139 +++++ .../SOURCES.json | 36 ++ .../TASK.json | 101 ++++ .../VERIFY.json | 36 ++ .../verify.py | 477 ++++++++++++++++++ 6 files changed, 940 insertions(+) create mode 100644 research/right-vector-small-local-products/PROOF.md create mode 100644 research/right-vector-small-local-products/README.md create mode 100644 research/right-vector-small-local-products/SOURCES.json create mode 100644 research/right-vector-small-local-products/TASK.json create mode 100644 research/right-vector-small-local-products/VERIFY.json create mode 100644 research/right-vector-small-local-products/verify.py diff --git a/research/right-vector-small-local-products/PROOF.md b/research/right-vector-small-local-products/PROOF.md new file mode 100644 index 0000000000..68dd126d4f --- /dev/null +++ b/research/right-vector-small-local-products/PROOF.md @@ -0,0 +1,151 @@ +# Common scalar pivot flags in small local products + +Let K be a finite field of cardinality q. Let + + R = R_1 x ... x R_k, 1 <= k <= q, + +where each R_i is an associative unital central K-algebra whose nonunits +form a proper two-sided ideal J_i. Thus D_i=R_i/J_i is a division algebra. +No commutativity, finite dimension, nilpotence, or equality D_i=K is assumed. +Fix n>=1 and an invertible M in M_n(R). + +A paid factor is I+u y^T, with u in R^n and y in K^n. Arbitrary common +GL_n(K) maps are free anywhere in a word. In particular the free maps and +right vectors cannot be chosen separately in the product components. +Let pi:R^n -> (R/K)^n use the diagonal central copy of K. The theorem is + + cost_R(M) = delta_R(M) = rank_K(pi M|_{K^n}) <= n, + delta_R(M) = min_{T in GL_n(K)} dim_K((MT-I)K^n). + +The column lower bound cost>=delta is cited from #4243/#4099. The new +step extends #4787's local arbitrary-role upper bound to these products. +#4601 and ToikY #4334 already give the two-role small-product case. + +## Avoiding the component kernels + +A union of k<=q proper K-linear subspaces of K^d cannot equal K^d, for +every d>=1. Each subspace has at most q^(d-1) elements and contains zero. +Their union therefore has size at most + + 1 + k(q^(d-1)-1) <= q^d-q+1 < q^d. + +We use only this elementary finite-vector-space count. + +For any invertible A in M_d(R), its reduction Abar_i is invertible over +D_i. The K-linear map + + L_i : K^d -> D_i, phi -> phi Abar_i e_1 + +is nonzero, since otherwise every entry in the first column of Abar_i +would vanish. Thus ker L_i is a proper scalar subspace. Choose one phi +outside their union. Then every phi A_i e_1 is a unit in R_i, since its +residue is nonzero. Hence a=phi A e_1 is a unit in R. This argument uses +one common scalar row phi, including when the division residues differ. + +## A common full pivot flag + +We prove by induction on d that some Q in GL_d(K) makes every leading +square corner of QA invertible over R. The d=0 statement is vacuous. +For d>=1 choose phi as above, and extend it to the first row of a scalar +basis matrix Q_0. Write + + Q_0 A = [[a,b],[c,F]], S=F-c a^(-1)b. + +Here a is a unit in R. Block triangular elimination makes diag(a,S), +so S is invertible. Apply the induction hypothesis to S, obtaining +P in GL_(d-1)(K), and set Q=diag(1,P)Q_0. Each leading corner of size +j>=2 in QA has pivot a and Schur complement the leading corner of PS +of size j-1. Both are invertible, so that corner is invertible. The +size-one corner is a. All ring products retain the displayed order; +no commutativity of R_i or D_i has been used. + +This proves existence of one common scalar pivot flag. The finite +constructor in verify.py searches scalar rows at each step and performs +this induction iteratively on its fixed bounded examples. + +## The exact number of active columns + +The following chart reduction is the cited #4787 argument, included to +connect the new flag to the precise cost. Put + + E={v in K^n : Mv belongs to K^n}, + s=dim_K E, d=n-s=rank_K(pi M|_{K^n}). + +Invertibility makes M:E -> M(E) injective. Choose a scalar basis of E, +extend it to a basis H of K^n, and extend its images to a basis B of K^n. +Then N=B^(-1)MH has its first s columns equal to those of I, so + + N=[[I_s,C],[0,A]], + +with A invertible. For any scalar T, pi(MT-I)=pi MT has rank d, giving +delta>=d. Conversely T=HB^(-1) gives + + MT-I=B(N-I)B^(-1), + +whose scalar column rank is at most d. Therefore delta=d. This reduction +needs invertibility but does not need the local-product hypothesis. + +Apply the common-flag lemma to A and left-multiply N by diag(I_s,Q). +This is free and preserves the first s fixed columns. Call the resulting +matrix N again. Its active leading corners are all invertible. + +For j=0,...,d let A_j consist of the first s+j columns of N and the +remaining columns of I. All A_j are invertible by the corner property. +A_0=I and A_d=N. Set h=s+j for j=1,...,d and + + u_j=A_(j-1)^(-1)(N e_h-e_h), F_j=I+u_j e_h^T. + +The h-th column of A_(j-1) is still e_h. Right multiplication by F_j +therefore replaces exactly that column, giving A_(j-1)F_j=A_j. Hence + + N=F_1 ... F_d. + +Every right vector e_h is scalar and common to all components. Undoing +the free charts gives a legal word for M with at most d paid factors. +Together with the cited lower bound, its cost is exactly d. If d=0, +M itself is a common free map and no paid factor is needed. There is no +auxiliary role or componentwise free operation in this construction. + +## Coverage of the separate binary metric + +The finite oracle treats invertible pairs (A,B) over F_2. A free common +left map sends this pair to (I,C), where C=A^(-1)B. Common free right +multiplication by T sends C to T^(-1)CT. A paid factor has components +P_0=I+u_0 y^T and P_1=I+u_1 y^T. Applied at the normalized representative, +it sends C to P_0^(-1)P_1 C. At an arbitrary representative, conjugating +the paid factor by A gives the same alphabet with a changed scalar y. +Thus all normalized paid transitions are exactly the generators enumerated +by the bit-matrix oracle. Both P_i must be invertible on any path to an +invertible endpoint, since singular matrices cannot regain rank over a field. + +BFS gives attaining paid paths. The verifier also checks every paid edge +against the distance labels and checks that every free conjugation leaves +its label unchanged. These inequalities prove the lower bound for every +word with arbitrary interleaved free maps. Hence the independent finite +metric is exact, without using the common-pivot theorem to prune its words. + +## What is new and what remains open + +The new statement is the arbitrary-role small-product theorem, in particular +all invertible targets over two local F_2-algebras at every role count. +The finite-subspace avoidance argument and Gaussian elimination are +classical. Their use to choose a complete common scalar pivot flag closes +the product gap left in #4787 while preserving the exact column bound. +The k<=q condition is necessary for a theorem covering every role count: +ToikY #4334 and #4601 already give two-role cost-three examples with +k=q+1 and delta=2. Their examples are cited, not replayed as this result. +No claim is made that k<=q is necessary for an individual target. + +Singular endpoints, products with more than q components at n>=3, matrix +blocks in a semilocal quotient, and a complete physical supplier are not +classified. Native coefficient preparation, routing, frames, restoration, +precision, stock and the full recursive bill remain unknown. This is a +scoped algebraic proof, not a complete multiplication theorem or new kappa. +Independent human and formal proof-kernel review are unclaimed. + +This contribution was produced by Nick Petalas. Credit Nick Petalas #4787 +for the local arbitrary-role theorem, active-column chart and open product +question; #4601 for the local-product two-role theorem; ToikY #4334 for +the field-product threshold; and Nick Petalas #4243 and Wentao Li #4099, +following #2513, for the alphabet, normal form and column lower bound. +Predecessor files and attribution are unchanged. Apache-2.0. diff --git a/research/right-vector-small-local-products/README.md b/research/right-vector-small-local-products/README.md new file mode 100644 index 0000000000..fbdea59a8f --- /dev/null +++ b/research/right-vector-small-local-products/README.md @@ -0,0 +1,139 @@ +# Exact all-role right-vector cost for small local products + +Scoped algebraic proof with finite corroboration. No new kappa. + +Let K=F_q and R=R_1 x ... x R_k, where 1<=k<=q and each R_i is an +associative central local K-algebra. Its nonunits must form a proper +two-sided ideal. For every n>=1 and every invertible M in M_n(R), + +```text +cost_R(M) = delta_R(M) = rank_K(pi M|_{K^n}) <= n, +delta_R(M) = min_{T in GL_n(K)} dim_K((MT-I)K^n), +pi : R^n -> (R/K)^n. +``` + +K embeds diagonally in R. A paid factor is I+u y^T with u in R^n and +y in K^n. Arbitrary common GL_n(K) maps are free anywhere. No extra role +is used. The residue division algebras may differ from K and may be +noncommutative. No finite-dimensionality or nilpotence assumption is needed. + +[PROOF.md](PROOF.md) gives the universal statement and attaining words. +It answers the arbitrary-role product question explicitly left open by +Nick Petalas #4787. ToikY #4334 and Nick Petalas #4601 already prove the +two-role small-product case. The new step chooses a common scalar pivot +at every Schur complement. Each component forbids a proper scalar +subspace; at most q such subspaces cannot cover the scalar row space. +This gives one common full pivot flag, followed by exactly delta column +replacements. Classical finite-vector-space counting and elimination +retain their ordinary mathematical credit. + +The component hypothesis cannot be removed from an all-role theorem: +the cited two-role predecessors already give k=q+1 examples with cost +three and delta two. That is predecessor credit, not a new certificate +in this package. Necessity for individual higher-role targets is open. + +## Finite evidence + +The standard-library verifier imports no predecessor code. It constructs +literal common-chart words and checks their full matrix products on all +28,224 invertible three-role targets over F2 x F2. Its exact paid-cost +histogram, in cost order zero through three, is + +```text +[168, 3528, 16464, 8064]. +``` + +A separate bit-matrix implementation enumerates GL3(F2). It normalizes a +pair (A,B) by its free left map to (I,A^(-1)B). Literal paid pairs with a +common right vector give 22 distinct normalized generators, including the +identity. BFS covers all 168 normalized states. Its labels satisfy all +3,696 paid edges and 28,224 free-conjugation edges, so they certify the +actual normalized alphabet metric. Every constructor length agrees. +Left normalization transports its witnesses to all 28,224 ordered pairs. +All 1,008 base-field basis-data actions on the 168 normalized words pass. + +The verifier also checks 431 distinct bounded examples on three and four +roles over (F2[e]/e^2)^2, F3^3 and (F3[e]/e^2)^3. These are samples, not +complete target censuses. They exercise every active dimension from zero +through the role count. All 6,644 basis-data actions and 18,200 literal +scalar-subspace input checks pass. The latter independently enumerate E +and check |E|=p^(n-d), rather than using the constructor's row reduction. + +Eight rejection controls cover missing factors, reversal, changed +coefficients, componentwise free maps, singular targets, too many +components, nonunit inversion and an illegal paid right-vector shape. +Two additional boundary fixtures require a non-coordinate common pivot +and demonstrate the covering failure at q+1 scalar hyperplanes. Checks +use explicit exceptions and remain active under optimized Python. +The verifier writes nothing and emits a generated receipt bound to all +six package files. No receipt is handwritten or committed. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-small-local-products/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-small-local-products/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-small-local-products +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-small-local-products --check-source-history +``` + +Any CPython 3.12 installation may replace the local path. Expected marker: + +```text +PASS_RIGHT_VECTOR_SMALL_LOCAL_PRODUCTS binary_pairs=28224 sampled_targets=431 controls=8 no_new_kappa +``` + +Both registered commands have 120-second limits and run the same complete +checks. SOURCES.json pins predecessor documents to canonical base +`de5ec2e7a6074068452f45b1a191b5c72832df4a`. They are cited dependencies, +not audited deliverables. The original card is explicitly changed to this +algebraic side result in TASK.json. Its selected-baseline first command +passed after sparse inputs were materialized; it is source-binding +orientation only. No selected operator replay was run. + +## Limits and implementation discipline + +The all-q, all-n result is the written proof. Software corroboration uses +base fields F2 and F3, the complete binary pair domain, and the stated +three-/four-role samples. It does not enumerate extension base fields or +noncommutative local products. Singular targets, more than q components +at n>=3 and matrix blocks in a semilocal quotient are not classified. +Native coefficient preparation, frames, routing, restoration, precision, +stock and a full supplier bill remain unknown. No supplier admission, +selected-frontier change or complete multiplication theorem is claimed. +Independent human and formal proof-kernel review are unclaimed. Lean, +Docker and the selected construction's cold replay are outside scope. + +The verifier has no recursion or subprocesses. Matrices have at most four +roles; local coefficient tables have at most nine elements; products have +at most three components. Scalar row searches and literal scalar inputs +have at most 3^4=81 candidates. The binary group has 168 states, its BFS +has exactly 168 iterations, and the complete pair loop has 168^2 cases. +Each sampler generates at most 80 candidates and stores at most 80 target +matrices. All functions fit within 60 lines. Python requires dynamic +allocation, a managed-runtime deviation bounded by these fixed domains. +Eight fixed negative-control callbacks are bounded local dispatch. +Warning-strict normal/optimized replay and in-memory source compilation +supply the available Python diagnostics. No shared configuration changes. + +## Open next questions + +1. For n>=3 and more than q components, determine which common scalar + flags still attain delta. Start with a three-component binary + three-role target. The present subspace count ceases to guarantee a + row, so an individual flag criterion is needed. +2. Specify one native producer/consumer for a column replacement and + price coefficient preparation, access, frames, restoration, precision + and stock before implementing a supplier. Those costs are unknown. + +## Credit + +This contribution was produced by Nick Petalas. Credit Nick Petalas #4787 +for the local arbitrary-role theorem, chart reduction and open product +question; #4601 for the two-role local-product extension; ToikY #4334 for +the field-product threshold; and Nick Petalas #4243 and Wentao Li #4099, +following #2513, for the alphabet, normal form and column lower bound. +The exact source documents and predecessor attribution are unchanged. +Apache-2.0. diff --git a/research/right-vector-small-local-products/SOURCES.json b/research/right-vector-small-local-products/SOURCES.json new file mode 100644 index 0000000000..b4a003b169 --- /dev/null +++ b/research/right-vector-small-local-products/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/right-vector-commutative-products/README.md", + "usage": "input", + "git_blob": "fc9889d41621b596209c707b6057517744b4642f", + "sha256": "6222431360182204f502334d1c707eefc39a174d06578ef75c52f37b5873055f" + }, + { + "path": "research/right-vector-local-all-roles/PROOF.md", + "usage": "input", + "git_blob": "46d63f385b1036db0019f9dd8b1909eac39bba99", + "sha256": "ce08b72a33602f5bd7ecae575711e584fe2ba3fb46deb797fe8109a6a2b98142" + }, + { + "path": "research/right-vector-local-products/PROOF.md", + "usage": "input", + "git_blob": "7230a0e7bb82384758114990a8c8958efd73d6e2", + "sha256": "c8ffdb932990533d1b1b5eda1b05ac2430cc6a1b2d7a263ca1f0bf76c414da0f" + } + ] +} diff --git a/research/right-vector-small-local-products/TASK.json b/research/right-vector-small-local-products/TASK.json new file mode 100644 index 0000000000..406a0a6837 --- /dev/null +++ b/research/right-vector-small-local-products/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "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": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove exact right-vector cost equal to the column lower bound for every invertible target at every role count over a product of at most q local central F_q-algebras.", + "scope_change_reason": "This is a scoped algebraic side result answering the common-pivot product question left by #4787, extending the two-role small-product theorem of ToikY #4334 and #4601. It is not a proof-assistant formalization, a supplier audit, or a complete physical caller.", + "bottleneck_link": "The theorem identifies when a shared scalar chart preserves the exact formal recursive-interface factor count across different local components. Native coefficient preparation, frames, routing, restoration, precision, stock and a complete supplier invoice remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved common-pivot extension with bounded corroboration. Do not extend to more components, singular targets or physical construction after this result.", + "outcome": "completed", + "evidence": "PROOF.md proves the all-role theorem by finite-subspace avoidance, common scalar pivot flags and the cited active-column reduction. The standalone verifier checks all 28224 binary two-component three-role invertible targets, a separate 168-state normalized literal-alphabet BFS, 431 distinct bounded product examples, 7652 basis actions, 18200 scalar-subspace input checks, eight rejection controls and two boundary fixtures. The current selected baseline passes after materializing omitted sparse inputs. Advance claim: https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213541.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "For n>=3 and products with more than q local components, which simultaneous scalar flags still attain delta?", + "why_it_matters": "The two-role threshold cannot classify individual higher-role targets. A flag criterion would distinguish actual chart conflicts from a component-count sufficient condition.", + "first_step": "Fix three invertible three-role components over F2 and test their scalar flags while retaining the complete common-free-map alphabet.", + "blocked_by": "The union-of-subspaces bound used here no longer guarantees an available row." + }, + { + "question": "Can a named native producer and consumer realize one common-chart column replacement with a favorable complete invoice?", + "why_it_matters": "Formal paid factors alone do not improve an admitted supplier.", + "first_step": "Specify the coefficient preparation, access, frame, restoration and output contracts before constructing a caller.", + "blocked_by": "All physical preparation, routing, precision, stock and implementation costs remain unknown." + } + ] +} diff --git a/research/right-vector-small-local-products/VERIFY.json b/research/right-vector-small-local-products/VERIFY.json new file mode 100644 index 0000000000..83277200d1 --- /dev/null +++ b/research/right-vector-small-local-products/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/right-vector-commutative-products/README.md", + "research/right-vector-local-all-roles/PROOF.md", + "research/right-vector-local-products/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full binary pair census, separate normalized literal-alphabet BFS and all free/paid edges, sampled local products, matrix/basis words, literal scalar subspaces, eight rejection controls and two boundary fixtures." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full binary pair census, separate normalized literal-alphabet BFS and all free/paid edges, sampled local products, matrix/basis words, literal scalar subspaces, eight rejection controls and two boundary fixtures." + } + ] +} diff --git a/research/right-vector-small-local-products/verify.py b/research/right-vector-small-local-products/verify.py new file mode 100644 index 0000000000..6292e4dadf --- /dev/null +++ b/research/right-vector-small-local-products/verify.py @@ -0,0 +1,477 @@ +#!/usr/bin/env python3 +"""Bounded literal corroboration of the common scalar pivot theorem.""" +from collections import Counter, deque +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import random + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +class Ring: + """A product of k copies of F_p[e]/e^ell, within fixed replay bounds.""" + + def __init__(self, p, ell, k): + require(p in (2, 3) and ell in (1, 2) and 1 <= k <= 3, 'ring bounds') + self.p, self.ell, self.k = p, ell, k + self.size = p ** ell + self.zero, self.one = (0,) * k, (1,) * k + self.add_table = tuple(tuple(self.local_add(a, b) for b in range(self.size)) + for a in range(self.size)) + self.mul_table = tuple(tuple(self.local_mul(a, b) for b in range(self.size)) + for a in range(self.size)) + self.neg_table = tuple(self.local_add(0, -a % p) if ell == 1 else + (-a % p) + p * (-(a // p) % p) + for a in range(self.size)) + self.inv_table = {} + for a in range(self.size): + if a % p: + candidates = [b for b in range(self.size) if self.mul_table[a][b] == 1] + require(len(candidates) == 1, 'local inverse') + self.inv_table[a] = candidates[0] + + def local_add(self, a, b): + return (a + b) % self.p if self.ell == 1 else ( + (a % self.p + b % self.p) % self.p + + self.p * ((a // self.p + b // self.p) % self.p)) + + def local_mul(self, a, b): + if self.ell == 1: + return a * b % self.p + return ((a % self.p) * (b % self.p) % self.p + + self.p * ((a // self.p * (b % self.p) + + b // self.p * (a % self.p)) % self.p)) + + def scalar(self, a): + return (a % self.p,) * self.k + + def add(self, a, b): + return tuple(self.add_table[x][y] for x, y in zip(a, b, strict=True)) + + def neg(self, a): + return tuple(self.neg_table[x] for x in a) + + def mul(self, a, b): + return tuple(self.mul_table[x][y] for x, y in zip(a, b, strict=True)) + + def unit(self, a): + return all(x % self.p for x in a) + + def inv(self, a): + require(self.unit(a), 'nonunit inverse') + return tuple(self.inv_table[x] for x in a) + + +def ident(r, n): + return tuple(tuple(r.one if i == j else r.zero for j in range(n)) + for i in range(n)) + + +def scalar_matrix(r, a): + return tuple(tuple(r.scalar(x) for x in row) for row in a) + + +def mm(r, a, b): + n = len(a) + require(1 <= n <= 4 and len(b) == n, 'matrix dimension') + out = [] + for i in range(n): + row = [] + for j in range(n): + value = r.zero + for h in range(n): + value = r.add(value, r.mul(a[i][h], b[h][j])) + row.append(value) + out.append(tuple(row)) + return tuple(out) + + +def inverse(r, a): + """Componentwise inversion is internal arithmetic, never a free map.""" + n = len(a) + require(1 <= n <= 4, 'inverse dimension') + components = [] + for c in range(r.k): + rows = [[a[i][j][c] for j in range(n)] + + [int(i == j) for j in range(n)] for i in range(n)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i][j] % r.p), None) + require(pivot is not None, 'singular component') + rows[j], rows[pivot] = rows[pivot], rows[j] + v = r.inv_table[rows[j][j]] + rows[j] = [r.mul_table[v][x] for x in rows[j]] + for i in range(n): + if i != j: + v = rows[i][j] + rows[i] = [r.add_table[x][r.neg_table[r.mul_table[v][y]]] + for x, y in zip(rows[i], rows[j], strict=True)] + components.append(rows) + return tuple(tuple(tuple(components[c][i][n+j] for c in range(r.k)) + for j in range(n)) for i in range(n)) + + +def rref(rows, p, n): + a = [list(row) for row in rows] + require(len(a) <= 24 and n <= 4, 'scalar system bounds') + pivots = [] + for j in range(n): + h = len(pivots) + pivot = next((i for i in range(h, len(a)) if a[i][j] % p), None) + if pivot is None: + continue + a[h], a[pivot] = a[pivot], a[h] + scale = pow(a[h][j], -1, p) + a[h] = [x * scale % p for x in a[h]] + for i in range(len(a)): + if i != h: + v = a[i][j] + a[i] = [(x-v*y) % p for x, y in zip(a[i], a[h], strict=True)] + pivots.append(j) + return a, pivots + + +def nullspace(rows, p, n): + a, pivots = rref(rows, p, n) + out = [] + for j in range(n): + if j not in pivots: + v = [int(h == j) for h in range(n)] + for i, h in enumerate(pivots): + v[h] = -a[i][j] % p + out.append(tuple(v)) + return out + + +def extend(vectors, p, n): + out = list(vectors) + require(len(rref(out, p, n)[1]) == len(out), 'dependent scalar basis') + for i in range(n): + v = tuple(int(i == j) for j in range(n)) + if len(rref(out+[v], p, n)[1]) > len(out): + out.append(v) + require(len(out) == n, 'basis extension') + return out + + +def mv(r, a, v): + """Literal action, separate from matrix multiplication.""" + result = [] + for row in a: + value = r.zero + for coefficient, datum in zip(row, v, strict=True): + value = r.add(value, r.mul(coefficient, datum)) + result.append(value) + return tuple(result) + + +def common_flag(r, a): + d = len(a) + require(r.k <= r.p, 'too many local components') + q = ident(r, d) + residual = a + for h in range(d): + m = d-h + phi = None + for v in product(range(r.p), repeat=m): + pivot = r.zero + for j in range(m): + pivot = r.add(pivot, r.mul(r.scalar(v[j]), residual[j][0])) + if r.unit(pivot): + phi = v + break + require(phi is not None, 'no common scalar pivot') + rows = extend([phi], r.p, m) + transform = [list(row) for row in ident(r, d)] + for i in range(m): + for j in range(m): + transform[h+i][h+j] = r.scalar(rows[i][j]) + q = mm(r, tuple(tuple(row) for row in transform), q) + if m > 1: + s = mm(r, scalar_matrix(r, rows), residual) + ai = r.inv(s[0][0]) + residual = tuple(tuple(r.add(s[i][j], r.neg(r.mul( + r.mul(s[i][0], ai), s[0][j]))) for j in range(1, m)) + for i in range(1, m)) + return q + + +def scalar_columns(r, m): + n = len(m) + equations = [] + for i in range(n): + for c in range(r.k): + if c: + equations.append(tuple((m[i][j][c]-m[i][j][0]) % r.p + for j in range(n))) + if r.ell == 2: + equations.append(tuple(m[i][j][c] // r.p for j in range(n))) + return nullspace(equations, r.p, n) + + +def construct(r, m): + n = len(m) + require(1 <= n <= 4 and r.k <= r.p, 'constructor domain') + inverse(r, m) # Reject a singular target before choosing scalar charts. + fixed = scalar_columns(r, m) + images = [] + for v in fixed: + image = mv(r, m, tuple(r.scalar(x) for x in v)) + require(all(x == r.scalar(x[0]) for x in image), 'nonscalar image') + images.append(tuple(x[0] for x in image)) + hb, bb = extend(fixed, r.p, n), extend(images, r.p, n) + h = scalar_matrix(r, tuple(zip(*hb, strict=True))) + b = scalar_matrix(r, tuple(zip(*bb, strict=True))) + left = inverse(r, b) + target = mm(r, mm(r, left, m), h) + s, d = len(fixed), n-len(fixed) + if d: + active = tuple(tuple(target[i][j] for j in range(s, n)) + for i in range(s, n)) + q = common_flag(r, active) + full = [list(row) for row in ident(r, n)] + for i in range(d): + for j in range(d): + full[s+i][s+j] = q[i][j] + left = mm(r, tuple(tuple(row) for row in full), left) + target = mm(r, mm(r, left, m), h) + prefix = ident(r, n) + factors = [] + for j in range(s, n): + column = tuple(r.add(target[i][j], r.neg(r.one if i == j else r.zero)) + for i in range(n)) + u = mv(r, inverse(r, prefix), column) + f = [list(row) for row in ident(r, n)] + for i in range(n): + f[i][j] = r.add(f[i][j], u[i]) + f = tuple(tuple(row) for row in f) + prefix = mm(r, prefix, f) + inverse(r, prefix) # Check that the replacement prefix is invertible. + factors.append(f) + require(prefix == target, 'column reconstruction') + return inverse(r, left), tuple(factors), inverse(r, h), d + + +def word_matrix(r, word): + left, factors, right, _ = word + out = left + for f in factors: + out = mm(r, out, f) + return mm(r, out, right) + + +def check_word(r, m, word, basis=False): + left, factors, right, d = word + require(len(factors) == d and d <= len(m), 'paid length') + for index, f in enumerate(factors): + column = len(m)-d+index + require(all(f[i][j] == (r.one if i == j else r.zero) + for i in range(len(m)) for j in range(len(m)) + if j != column), 'illegal paid right vector') + for free in (left, right): + require(all(x == r.scalar(x[0]) for row in free for x in row), + 'componentwise free map') + require(word_matrix(r, word) == m, 'literal word mismatch') + if not basis: + return 0 + count = 0 + for role in range(len(m)): + for component in range(r.k): + for degree in range(r.ell): + data = [r.zero] * len(m) + value = [0] * r.k + value[component] = r.p ** degree + data[role] = tuple(value) + actual = mv(r, right, data) + for f in reversed(factors): + actual = mv(r, f, actual) + actual = mv(r, left, actual) + require(actual == mv(r, m, data), 'basis action mismatch') + count += 1 + return count + + +def bmul(a, b): + return tuple((b[0] if row & 1 else 0) ^ (b[1] if row & 2 else 0) + ^ (b[2] if row & 4 else 0) for row in a) + + +def binary_group(): + identity = (1, 2, 4) + group = tuple(a for a in product(range(8), repeat=3) + if len({((a[0]&x).bit_count() % 2) + | (((a[1]&x).bit_count() % 2) << 1) + | (((a[2]&x).bit_count() % 2) << 2) + for x in range(8)}) == 8) + inverses = {a: next(b for b in group if bmul(a, b) == identity) for a in group} + paid = set() + for y in range(1, 8): + factors = [] + for u in range(8): + a = tuple(identity[i] ^ (y if u >> i & 1 else 0) for i in range(3)) + if a in inverses: + factors.append(a) + for a in factors: + for b in factors: + paid.add(bmul(inverses[a], b)) + distance = {identity: 0} + queue = deque([identity]) + for _ in range(len(group)): + require(bool(queue), 'BFS queue exhausted early') + a = queue.popleft() + for f in paid: + b = bmul(f, a) + if b not in distance: + distance[b] = distance[a]+1 + queue.append(b) + require(not queue and len(distance) == len(group), 'BFS coverage') + for a in group: + for f in paid: + require(distance[bmul(f, a)] <= distance[a]+1, 'paid edge lower bound') + for t in group: + require(distance[bmul(bmul(inverses[t], a), t)] == distance[a], + 'free conjugation distance') + return group, inverses, distance, len(paid) + + +def binary_census(): + r = Ring(2, 1, 2) + group, inverses, distance, generators = binary_group() + require(len(group) == 168, 'binary group coverage') + words = {} + basis = 0 + for a in group: + m = tuple(tuple((int(i == j), a[i] >> j & 1) for j in range(3)) + for i in range(3)) + word = construct(r, m) + require(word[3] == distance[a], 'independent BFS cost mismatch') + basis += check_word(r, m, word, basis=True) + words[a] = word + histogram = Counter() + for a in group: + scalar = scalar_matrix(r, tuple(tuple(a[i] >> j & 1 for j in range(3)) + for i in range(3))) + for b in group: + relative = bmul(inverses[a], b) + left, factors, right, d = words[relative] + word = (mm(r, scalar, left), factors, right, d) + m = tuple(tuple((a[i] >> j & 1, b[i] >> j & 1) for j in range(3)) + for i in range(3)) + check_word(r, m, word) + histogram[d] += 1 + return {'targets': sum(histogram.values()), 'cost_histogram': dict(histogram), + 'normalized_targets': len(words), 'basis_actions': basis, + 'normalized_paid_generators': generators}, r, words + + +def sampled_products(): + rng = random.Random(102209) + records = [] + for p, ell, k in ((2, 2, 2), (3, 1, 3), (3, 2, 3)): + r = Ring(p, ell, k) + units = tuple(x for x in range(r.size) if x % p) + for n in (3, 4): + seen, hist, actions, scalar_tests = set(), Counter(), 0, 0 + for nominal in range(n+1): + for _ in range(16): + m = ident(r, n) + for j in range(n-nominal, n): + f = [list(row) for row in ident(r, n)] + for i in range(n): + f[i][j] = tuple(rng.randrange(r.size) for _ in range(k)) + f[j][j] = tuple(rng.choice(units) for _ in range(k)) + m = mm(r, m, tuple(tuple(row) for row in f)) + for _ in range(2*n): + i, j = rng.sample(range(n), 2) + f = [list(row) for row in ident(r, n)] + f[i][j] = r.scalar(rng.randrange(1, p)) + f = tuple(tuple(row) for row in f) + m = mm(r, f, m) if rng.randrange(2) else mm(r, m, f) + if m in seen: + continue + seen.add(m) + word = construct(r, m) + actions += check_word(r, m, word, basis=True) + scalar_count = 0 + for v in product(range(p), repeat=n): + image = mv(r, m, tuple(r.scalar(x) for x in v)) + scalar_count += all(x == r.scalar(x[0]) for x in image) + scalar_tests += 1 + require(scalar_count == p ** (n-word[3]), 'literal scalar subspace') + hist[word[3]] += 1 + records.append({'p': p, 'ell': ell, 'components': k, 'roles': n, + 'targets': len(seen), 'cost_histogram': dict(hist), + 'basis_actions': actions, 'scalar_input_tests': scalar_tests}) + return records + + +def rejected(call): + try: + call() + except ValueError: + return + raise ValueError('negative control was accepted') + + +def controls(r, words): + candidates = [word for word in words.values() if word[3] == 3] + word = next(w for w in candidates + if word_matrix(r, (w[0], tuple(reversed(w[1])), w[2], w[3])) + != word_matrix(r, w)) + m = word_matrix(r, word) + left, factors, right, d = word + rejected(lambda: check_word(r, m, (left, factors[:-1], right, d))) + rejected(lambda: check_word(r, m, (left, tuple(reversed(factors)), right, d))) + changed = [list(row) for row in factors[0]] + changed[0][0] = r.add(changed[0][0], (1, 0)) + bad = (tuple(tuple(row) for row in changed),) + factors[1:] + rejected(lambda: check_word(r, m, (left, bad, right, d))) + changed = [list(row) for row in left] + changed[0][0] = r.add(changed[0][0], (1, 0)) + rejected(lambda: check_word(r, m, (tuple(tuple(row) for row in changed), + factors, right, d))) + singular = tuple((r.zero,) * 3 for _ in range(3)) + rejected(lambda: construct(r, singular)) + rejected(lambda: construct(Ring(2, 1, 3), ident(Ring(2, 1, 3), 3))) + rejected(lambda: r.inv((0, 1))) + illegal = [list(row) for row in ident(r, 3)] + illegal[0][1], illegal[1][2] = r.one, r.one + illegal = tuple(tuple(row) for row in illegal) + rejected(lambda: check_word(r, illegal, + (ident(r, 3), (illegal,), ident(r, 3), 1))) + # The binary kernels x=0 and y=0 cover coordinate choices, not x+y. + a = (((1, 0), (0, 1)), ((0, 1), (1, 0))) + require(not r.unit(a[0][0]) and not r.unit(a[1][0]), 'row conflict fixture') + q = common_flag(r, a) + require(r.unit(mm(r, q, a)[0][0]), 'non-coordinate scalar pivot') + require(q != ident(r, 2), 'required scalar basis change') + # The q+1 hyperplanes really can cover, so the component bound matters. + require(all(x == 0 or y == 0 or x == y + for x, y in product(range(2), repeat=2)), 'cover boundary') + return 8 + + +def main(): + census, ring, words = binary_census() + samples = sampled_products() + control_count = controls(ring, words) + root = Path(__file__).resolve().parent + hashes = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(root.iterdir()) if p.is_file()} + receipt = {'claim_type': 'scoped proof with finite corroboration', + 'binary_pair_census': census, 'samples': samples, + 'rejection_controls': control_count, 'boundary_fixtures': 2, + 'file_sha256': hashes} + print(json.dumps(receipt, sort_keys=True)) + print('PASS_RIGHT_VECTOR_SMALL_LOCAL_PRODUCTS', + f"binary_pairs={census['targets']}", + f"sampled_targets={sum(x['targets'] for x in samples)}", + f'controls={control_count}', 'no_new_kappa') + + +if __name__ == '__main__': + main()