From fcc907921e1083f5f57fb1f6b6249bfc1f2cf142 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 14:04:52 +0100 Subject: [PATCH] feat(research): classify optimal second callees --- research/optimal-second-callees/PROOF.md | 168 +++++++++++++ research/optimal-second-callees/README.md | 120 +++++++++ research/optimal-second-callees/SOURCES.json | 24 ++ research/optimal-second-callees/TASK.json | 135 ++++++++++ research/optimal-second-callees/VERIFY.json | 34 +++ research/optimal-second-callees/verify.py | 252 +++++++++++++++++++ 6 files changed, 733 insertions(+) create mode 100644 research/optimal-second-callees/PROOF.md create mode 100644 research/optimal-second-callees/README.md create mode 100644 research/optimal-second-callees/SOURCES.json create mode 100644 research/optimal-second-callees/TASK.json create mode 100644 research/optimal-second-callees/VERIFY.json create mode 100644 research/optimal-second-callees/verify.py diff --git a/research/optimal-second-callees/PROOF.md b/research/optimal-second-callees/PROOF.md new file mode 100644 index 0000000000..4bd60b2214 --- /dev/null +++ b/research/optimal-second-callees/PROOF.md @@ -0,0 +1,168 @@ +# All optimal second callees in the fixed ordinary wrapper + +This proof is produced by Nick Petalas. Apache-2.0. + +Jerry Chen / CubeJerry's [PR2950](https://github.com/CrocSwap/integer-mult-bounds/pull/2950), +Theorem 2 of `research/weighted-wrapper-contract/README.md`, supplies the +optimal agreement value and the attainer Q=P. The new result here is the +complete equality classification and its scalar finite-field count. The +predecessor's optimum, source execution and census are not audited here. + +## 1. Exact model and statement + +Let V be an n-dimensional vector space over any field F, n>=1. Let P and +Q be invertible F-linear maps V to V. For a callee define + + F_P(H,D) = (P D, P^-1 H). + +Execute these six operations in chronological order: + + D -= H; F_P; D += H; F_Q; D = -D; D += H. + +Call their endpoint W_(P,Q), and let J(H,D)=(D,H). All inputs are arbitrary. +There is no restriction to a convenient subspace of the two input banks. +Put + + E = W_(P,Q) - J, A = P^2-I, R = Q-P, s = rank A. + +Choose any inner inverse G of A, meaning A G A=A. Such a G exists over every +field, including when A is singular. The choice need not commute with A or P. + +**Theorem.** Q attains the minimum possible error rank s if and only if + + im R is contained in im A, + ker A is contained in ker R, + R G R = 0. (1) + +The last condition is independent of the choice of G when the first two +hold. Over a finite field F_q, this is exactly the condition for Q to attain +PR2950's maximum q^(2n-s) correct input pairs. Q must still be invertible; +conditions (1) by themselves do not imply that requirement. + +Equivalently, let K=ker A and U=V/K. The map A induces an isomorphism +Abar: U to im A. Under the first two conditions, R induces Rbar: U to im A. +The endomorphism S=Abar^-1 Rbar of U must satisfy S^2=0. Thus all optimal +second maps have the complete parameterization + + Q = P + Abar S pi, S in End(U), S^2=0, Q invertible, (2) + +where pi: V to U is the quotient map. This describes an attaining set, not +an implementation of any of its elements. + +## 2. Reduce the literal error to one block matrix + +Set x=D-H. Direct execution of the six operations gives + + H' = Q P^-1 H + Q P x, + D' = H' - Q^-1 P x. + +If e1=H'-D and e2=D'-H, then + + e1 = R(P^-1 H+P x) + A x, + Q(e2-e1) = R x. + +Both changes of coordinates + + (H,D) to (x,y), y=P^-1 H+P x, + (e1,e2) to (e1,Q(e2-e1)) + +are invertible. Therefore E has the same rank as + + M = [ A R ] + [ R 0 ]. (3) + +This calculation preserves the order of noncommuting P,Q. It uses no +symmetry, diagonalizability or characteristic assumption. The A submatrix +shows rank M>=s; R=0 attains s. This short observation records the already +credited optimum while preparing its new equality case. + +## 3. Characterize equality + +If rank M=s, adjoining R to A horizontally or vertically cannot increase +rank. These are exactly the image and kernel containments in (1). + +Choose invertible L,T with L A T=D_s=diag(I_s,0). Apply L to both block +rows and T to both block columns in (3). Write B=L R T. The two +containments say exactly + + B = [ B0 0 ] + [ 0 0 ], + +where B0 is s by s. After deleting the zero rows and columns, the block +matrix becomes + + [ I_s B0 ] + [ B0 0 ]. + +Subtract B0 times the first block row from the second, then eliminate the +upper-right block by a block-column operation. This gives diagonal blocks +I_s and -B0^2. Hence + + rank M = s + rank(B0^2) (4) + +under the two containments. In particular equality holds exactly when B0^2=0. + +For any G satisfying A G A=A, put G'=T^-1 G L^-1. Its leading s by s block +is I_s because D_s G' D_s=D_s. Consequently + + L R G R T = B G' B = diag(B0^2,0). + +This proves (1), its independence of G and both directions of the theorem. +For (2), the identity pi G Abar=I_U follows from A G A=A and injectivity +of Abar. Thus R G R=Abar S^2 pi. Surjectivity of pi and injectivity of +Abar give the stated square-zero equivalence. If F=F_q, rank-nullity on +the 2n-dimensional input space counts the agreements as q^(2n-rank E). + +The case A=0 is included. Its image containment forces R=0, so an +involutory first map has a unique optimal second map, namely P itself. + +## 4. Count every optimal second map for a scalar first map + +**Corollary.** Let F=F_q and P=lambda I, with lambda nonzero and +lambda^2 different from 1. Every optimal second map is uniquely + + Q = lambda I + R, R^2=0. + +There are exactly + + sum_(r=0)^floor(n/2) [n choose r]_q [n-r choose r]_q |GL_r(F_q)| (5) + +such second maps. The summand is the exact count with rank(Q-P)=r. +Here [a choose b]_q counts b-dimensional subspaces of F_q^a and +|GL_0(F_q)|=1. Every one agrees with interchange on q^n input pairs. + +*Proof.* A=(lambda^2-1)I is invertible, so the first two conditions in +(1) are automatic and the third is R^2=0. Such a Q is invertible with +inverse lambda^-1 I-lambda^-2 R. For square-zero R of rank r, choose +its image I of dimension r and its kernel K of dimension n-r, with +I contained in K. Then choose the isomorphism V/K to I induced by R. +Conversely each such choice gives exactly one R. The numbers of choices +are [n choose r]_q, [n-r choose n-2r]_q=[n-r choose r]_q and |GL_r|. +The inclusion forces r<=floor(n/2), proving (5). Rank A=n gives the +agreement count. This flag-counting argument is standard linear algebra; +its application to all optimal wrapper callees is the scoped new consequence. + +At n=2, (5) is 1+(q+1)(q-1)=q^2. In particular P=2I over F5 has +exactly 25 optimal second maps, although PR2950 gives P as one attainer. +One different attainer is Q=[[2,1],[0,2]]. It agrees on 25 of 625 input +pairs, the same maximum as Q=P. None of these calls fixes the failed +wrapper on every input. No claim of exact interchange follows from optimal +agreement. + +Invertibility in (2) cannot be dropped for a nonscalar P. Over F5 take + + P = [2 0], A = 3I, R = [4 1], Q = [1 1]. + [0 3] [4 1] [4 4] + +All three conditions (1) hold, but Q is singular. This is an excluded +parameter, since F_Q is undefined. Finite tests explicitly retain this control. + +## 5. Limits + +The theorem is a written all-dimension, all-field linear algebra proof. +The verifier corroborates declared finite prime-field domains; it is not +a proof-kernel formalization. General finite abelian groups and nonlinear +callees are outside the equality classification. Callees are exact endpoint +oracles. Their implementation, normalization, frames, restoration, hosting, +precision, tape costs and supplier admission remain unproved here. The +selected conditional frontier and the multiplication theorem are unaffected. diff --git a/research/optimal-second-callees/README.md b/research/optimal-second-callees/README.md new file mode 100644 index 0000000000..01bf464c2c --- /dev/null +++ b/research/optimal-second-callees/README.md @@ -0,0 +1,120 @@ +# Classify every optimal second callee in the ordinary wrapper + +This contribution is produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written mathematical proof with exact finite corroboration. +For every invertible linear first map P over every field, this package +classifies all second maps Q attaining the fixed ordinary wrapper's known +minimum error rank. The new condition is a square-zero endomorphism on +V/ker(P^2-I), with an explicit invertibility filter on Q. + +Write A=P^2-I and R=Q-P. Choose any G satisfying A G A=A. Then an invertible +Q is optimal exactly when + + im R is contained in im A, + ker A is contained in ker R, + R G R=0. + +When the two containments hold, the condition is independent of G. +[PROOF.md](PROOF.md) proves necessity and sufficiency, including singular A, +noncommuting maps and every field characteristic. + +For P=lambda I over F_q with lambda nonzero and lambda^2 different from 1, +all optimal second maps are lambda I+R with R^2=0. Their exact number is + + sum_(r=0)^floor(n/2) [n choose r]_q [n-r choose r]_q |GL_r(F_q)|. + +The r-th summand counts rank(Q-P)=r. At n=2 there are exactly q^2 attainers. +For P=2I over F5 there are 25, including Q=[[2,1],[0,2]]. Each agrees +with interchange on 25 of 625 input pairs. Optimal agreement does not imply +exact interchange. For an involutory P, the unique optimal Q is P itself. + +## Relation to predecessor work + +Jerry Chen / CubeJerry's merged [PR2950](https://github.com/CrocSwap/integer-mult-bounds/pull/2950) +already proves the optimal error-image/agreement value and supplies Q=P as +one attainer. That theorem is a cited premise, not an audit deliverable. +This package adds its complete linear equality classification and the scalar +finite-field count. No predecessor executable or census is imported or replayed. +The rank-equality and square-zero flag-counting techniques are standard linear +algebra; no priority over those techniques is claimed. + +Nick Petalas / PR2808 and PR2786, David Arias / PR2753 and Jose Manuel / +PR2697/2899 retain the ordinary-wrapper, padding and stream lineage credit. +Wentao Li / PR4053, PR4063 and PR4070 studies paid normalization and reciprocal +weighted pairs. Those are different questions from the attaining set at the +unchanged two-callee boundary. Their package files and credit lines are untouched. +The predecessor README is pinned as historical provenance in SOURCES.json. + +## Reproduce + +From the repository root with CPython 3.12 and standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/optimal-second-callees +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/optimal-second-callees/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/optimal-second-callees/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/optimal-second-callees --check-source-history +``` + +Any CPython 3.12 interpreter path may replace the local path. The direct +marker is `PASS_OPTIMAL_SECOND_CALLEES no_new_kappa`. Normal execution +writes nothing. It prints a generated receipt binding the enumerated results +to SHA256 hashes of all six package files. No receipt is hand-written. + +The verifier checks the new equality criterion against literal six-operation +execution on every basis column in its declared complete invertible-map +pair domains. It separately enumerates arbitrary A,R and every inner inverse +in two small fields, and square-zero matrices by rank. These are finite +corroborations of the written theorem, not all-field computational proofs. +Six control groups distinguish different optimal maps, omitted image/kernel +conditions, a non-square-zero perturbation, singular candidate Q and the +involutory boundary. Explicit exceptions retain checks under Python -O. + +The finite domains contain 258,624 ordered invertible wrapper-map pairs, +6,817 arbitrary two-by-two A,R pairs, 1,087 inner inverses across all A in +the two declared fields, and 88,871 matrices for square-zero rank counts. +The wrapper domains are all P,Q in GL_3(F2) and GL_2(F5). The receipt lists +each domain and every observed count separately. + +## Scope and limits + +This is an algebraic side result. The `uniform-transfer-audit` card is +explicitly changed from auditing #4100 to a new equality statement at PR2950's +fixed wrapper interface. The source-bound selected-baseline orientation +passed; the selected construction itself was not replayed. Canonical base +is ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c, priority revision 7. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146072) +records the question and bounded method. Live PRs, active Discussions, recent +account posts, local reservations, cached overlap, main READMEs and merged +PR terms were checked. Sparse notes and unpublished work limit that coverage. +TASK.json records the exact scope change and SOURCES.json pins provenance. + +General finite abelian groups, nonlinear callees and changed surrounding +operations are outside scope. No attaining callee's physical implementation, +normalization, frames, restoration, hosting, tape, precision or recursive bill +is supplied. No supplier, new kappa, selected-frontier change or complete +multiplication theorem is claimed. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and the selected cold replay are unrun. + +The checker has fixed prime-field domains and at most four logical coordinates. +Assembled error matrices have at most six rows and six columns. +Its loops have finite enumeration bounds, it has no recursion or dynamic +imports, and functions fit within 60 lines. Python allocation is dynamic; +the fixed matrix domains bound live storage rather than implementing fixed +allocation. The largest stored invertible group has 480 matrices, and every +individual enumerator visits at most 65,536 matrices. Warning-strict normal +and optimized execution supply interpreter diagnostics. This is not a +whole-repository static-analysis or proof-kernel pass. + +## Open next questions + +- Count the invertibility-filtered square-zero quotient maps for nonscalar P + from its rational canonical data. Begin with one nonsemisimple block and + retain every singular-Q rejection. The present theorem gives the exact + set but no general closed form for that filtered count. +- Find an actual weighted caller with a less expensive second callee among + the classified maps. First pin its first map, required correctness domain + and complete paid invoice. No physical caller or cost advantage is supplied. + +Structured questions, relevance and blockers are in TASK.json. diff --git a/research/optimal-second-callees/SOURCES.json b/research/optimal-second-callees/SOURCES.json new file mode 100644 index 0000000000..5a901cc01c --- /dev/null +++ b/research/optimal-second-callees/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "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/weighted-wrapper-contract/README.md", + "usage": "provenance", + "git_blob": "f0a912efd96af3804f5663ba39323763bc0ed797", + "sha256": "e1565fb54651303258ef144f7b774e8ef1e7534d3b1129c516a6f88326408c71" + } + ] +} diff --git a/research/optimal-second-callees/TASK.json b/research/optimal-second-callees/TASK.json new file mode 100644 index 0000000000..42bdd5bf74 --- /dev/null +++ b/research/optimal-second-callees/TASK.json @@ -0,0 +1,135 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify all linear second callees attaining the fixed ordinary wrapper optimum over every field, and count every attainer for scalar first maps over finite fields.", + "scope_change_reason": "The donor requests original research rather than an audit. This changes the #4100 card to an uncovered equality question at Jerry Chen / PR2950's retained ordinary-wrapper boundary; predecessor optimum values are cited premises.", + "bottleneck_link": "Algebraic side result for choosing interchangeable second callees with equal endpoint agreement. It neither repairs exact interchange nor discharges a selected all-size obligation.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified equality classification and its planned scalar count. Package one scoped result without searching for a supplier or extending to other groups.", + "outcome": "completed", + "evidence": "Written all-field proof in PROOF.md, literal full-basis wrapper executions, complete finite equality domains, square-zero rank-stratum counts and six control groups.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "For a nonscalar first map P, can the invertibility filter in Q=P+Abar S pi be counted in a closed form from the rational canonical data of P?", + "why_it_matters": "The classification leaves an explicit finite admissibility filter, so its exact size can guide the choice of second endpoint.", + "first_step": "Count the square-zero quotient maps for one nonsemisimple rational canonical block, retaining the invertibility test.", + "blocked_by": "No general count of the filtered square-zero endomorphisms is supplied." + }, + { + "question": "Does an actual weighted caller have a less expensive second callee among the classified optimal maps?", + "why_it_matters": "Equal agreement alone gives no physical or recursive saving.", + "first_step": "Pin an actual first callee, required correctness domain and complete second-call invoice before selecting a different attainer.", + "blocked_by": "No physical first/second callee implementation or paid caller is supplied." + } + ], + "claim_type": "scoped written proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146072", + "overlap": { + "snapshot_utc": "2026-10-23T12:55:38Z", + "open_pr_records": 341, + "discussion_records": 4443, + "local_notes_searched": 170, + "local_head_notes": 6996, + "limitations": "Sparse local notes incomplete. Separate main README and quoted merged/all-state PR searches covered wrapper, second-callee and square-zero terms, not every diff or unpublished work.", + "predecessors": [ + 2950, + 2808, + 2753, + 2697, + 2899 + ], + "adjacent_normalization_work": [ + 4053, + 4063, + 4070 + ] + }, + "preserved_start": { + "branch": null, + "head": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "status": "clean detached HEAD; no earlier branch was checked out" + }, + "environment": { + "python": "Python 3.12.15", + "dependencies": "standard library only" + }, + "upstream_refresh": { + "main_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "priority_revision": 7, + "status": "Canonical main unchanged at precommit refresh. Live open PRs and latest 30 handoff posts checked again; no new matching wrapper equality work found." + }, + "verification": { + "local_registered": "Both normal and optimized registered commands passed. The initial combined package replay took 27.52 seconds; final command timings are recorded outside the checkout and in the PR body.", + "direct": "Warning-strict isolated direct normal and optimized replays passed in 13.784 and 14.002 seconds respectively; both printed PASS_OPTIMAL_SECOND_CALLEES no_new_kappa.", + "syntax": "AST parsing passed; every function has at most 29 physical lines.", + "unrun": [ + "Independent human review", + "Proof-kernel formalization", + "Native/physical callee implementation", + "Selected construction cold replay", + "Whole-repository static analysis" + ], + "finite_coverage": { + "literal_wrapper_map_pairs": 258624, + "arbitrary_A_R_pairs": 6817, + "inner_inverses": 1087, + "square_zero_domain_matrices": 88871, + "control_groups": 6 + } + } +} diff --git a/research/optimal-second-callees/VERIFY.json b/research/optimal-second-callees/VERIFY.json new file mode 100644 index 0000000000..b7a51a2735 --- /dev/null +++ b/research/optimal-second-callees/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Literal fixed-wrapper equality classification, all inner-inverse choices in the declared small domains, square-zero rank-stratum counts and six discriminating control groups." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same exact finite classification with Python assertions disabled; all checks use explicit exceptions." + } + ] +} diff --git a/research/optimal-second-callees/verify.py b/research/optimal-second-callees/verify.py new file mode 100644 index 0000000000..634ad5fc82 --- /dev/null +++ b/research/optimal-second-callees/verify.py @@ -0,0 +1,252 @@ +"""Exact finite corroboration of the optimal-second-callee classification. + +Produced by Nick Petalas. Apache-2.0. +Fixed prime-field domains only; normal execution writes nothing. +""" + +import hashlib +import itertools +import json +from pathlib import Path + +Matrix = tuple[tuple[int, ...], ...] +DOMAINS = ((2, 3), (5, 2)) +COUNT_DOMAINS = ((2, 1), (2, 2), (2, 3), (2, 4), + (3, 1), (3, 2), (3, 3), (5, 1), (5, 2), (7, 1), (7, 2)) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def eye(n: int) -> Matrix: + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def zero(n: int) -> Matrix: + return tuple((0,) * n for _ in range(n)) + + +def add(a: Matrix, b: Matrix, q: int, sign: int = 1) -> Matrix: + return tuple(tuple((x + sign * y) % q for x, y in zip(ar, br)) + for ar, br in zip(a, b)) + + +def mul(a: Matrix, b: Matrix, q: int) -> Matrix: + return tuple(tuple(sum(x * y for x, y in zip(ar, bc)) % q + for bc in zip(*b)) for ar in a) + + +def vector(a: Matrix, x: tuple[int, ...], q: int) -> tuple[int, ...]: + return tuple(sum(u * v for u, v in zip(row, x)) % q for row in a) + + +def row_reduce(a: Matrix, q: int) -> tuple[Matrix, Matrix, tuple[int, ...]]: + """Return R,U,pivots with U A=R, using bounded row elimination.""" + n, m = len(a), len(a[0]) + rows, transform, pivots = [list(row) for row in a], [list(r) for r in eye(n)], [] + for col in range(m): + pivot = next((i for i in range(len(pivots), n) if rows[i][col]), None) + if pivot is None: + continue + k = len(pivots) + rows[k], rows[pivot] = rows[pivot], rows[k] + transform[k], transform[pivot] = transform[pivot], transform[k] + scale = pow(rows[k][col], -1, q) + rows[k] = [(x * scale) % q for x in rows[k]] + transform[k] = [(x * scale) % q for x in transform[k]] + for i in range(n): + if i != k: + factor = rows[i][col] + rows[i] = [(x - factor * y) % q for x, y in zip(rows[i], rows[k])] + transform[i] = [(x - factor * y) % q + for x, y in zip(transform[i], transform[k])] + pivots.append(col) + return tuple(map(tuple, rows)), tuple(map(tuple, transform)), tuple(pivots) + + +def rank(a: Matrix, q: int) -> int: + return len(row_reduce(a, q)[2]) + + +def inverse(a: Matrix, q: int) -> Matrix: + reduced, transform, pivots = row_reduce(a, q) + need(len(pivots) == len(a), "inverse of a singular matrix") + need(reduced == eye(len(a)), "invalid inverse reduction") + need(mul(a, transform, q) == eye(len(a)), "inverse postcondition") + return transform + + +def inner_inverse(a: Matrix, q: int) -> Matrix: + _, transform, pivots = row_reduce(a, q) + rows = [list(r) for r in zero(len(a))] + for i, pivot in enumerate(pivots): + rows[pivot] = list(transform[i]) + g = tuple(map(tuple, rows)) + need(mul(mul(a, g, q), a, q) == a, "A G A must equal A") + return g + + +def matrices(q: int, n: int): + need(q in (2, 3, 5, 7) and 1 <= n <= 4, "unsupported finite domain") + need(q ** (n * n) <= 65536, "matrix enumeration capacity exceeded") + for entries in itertools.product(range(q), repeat=n * n): + yield tuple(tuple(entries[i * n:(i + 1) * n]) for i in range(n)) + + +def block(a: Matrix, r: Matrix) -> Matrix: + z = zero(len(a)) + return tuple(x + y for x, y in zip(a, r)) + tuple(x + y for x, y in zip(r, z)) + + +def conditions(a: Matrix, r: Matrix, g: Matrix, q: int) -> tuple[bool, bool, bool]: + s = rank(a, q) + horizontal = tuple(x + y for x, y in zip(a, r)) + return (rank(horizontal, q) == s, + rank(a + r, q) == s, + mul(mul(r, g, q), r, q) == zero(len(a))) + + +def literal_error(p: Matrix, pi: Matrix, t: Matrix, ti: Matrix, q: int) -> Matrix: + """Execute the six body operations on every complete basis input.""" + n = len(p) + columns = [] + for j in range(2 * n): + h0 = tuple(int(j == i) for i in range(n)) + d0 = tuple(int(j == n + i) for i in range(n)) + h, d = h0, tuple((x - y) % q for x, y in zip(d0, h0)) + h, d = vector(p, d, q), vector(pi, h, q) + d = tuple((x + y) % q for x, y in zip(d, h)) + h, d = vector(t, d, q), vector(ti, h, q) + d = tuple((-x) % q for x in d) + d = tuple((x + y) % q for x, y in zip(d, h)) + columns.append(tuple((x - y) % q for x, y in zip(h, d0)) + + tuple((x - y) % q for x, y in zip(d, h0))) + return tuple(zip(*columns)) + + +def equality_lemma() -> dict: + cases = alternate_g = 0 + for q in (2, 3): + domain = tuple(matrices(q, 2)) + for a in domain: + g, s = inner_inverse(a, q), rank(a, q) + for r in domain: + actual = rank(block(a, r), q) == s + need(actual == all(conditions(a, r, g, q)), "block equality iff failed") + cases += 1 + for other_g in domain: + if mul(mul(a, other_g, q), a, q) == a: + for r in domain: + need(conditions(a, r, g, q) == conditions(a, r, other_g, q) + or not all(conditions(a, r, g, q)[:2]), + "inner inverse dependence under containments") + alternate_g += 1 + return {"all_A_R_pairs": cases, "all_inner_inverses": alternate_g} + + +def wrapper_classification() -> list[dict]: + rows = [] + for q, n in DOMAINS: + group = tuple(a for a in matrices(q, n) if rank(a, q) == n) + inverses = {a: inverse(a, q) for a in group} + optimal = pairs = changed = 0 + by_rank = [0] * (n + 1) + for p in group: + a = add(mul(p, p, q), eye(n), q, -1) + g, s = inner_inverse(a, q), rank(a, q) + for t in group: + r = add(t, p, q, -1) + actual = rank(literal_error(p, inverses[p], t, inverses[t], q), q) == s + predicted = all(conditions(a, r, g, q)) + need(actual == predicted, "new equality classification failed") + if actual: + optimal += 1 + by_rank[rank(r, q)] += 1 + changed += int(r != zero(n)) + pairs += 1 + rows.append({"q": q, "n": n, "invertible_first_maps": len(group), + "ordered_pairs": pairs, "optimal_pairs": optimal, + "changed_optimal_pairs": changed, "optimal_by_rank_Q_minus_P": by_rank}) + return rows + + +def gaussian(n: int, r: int, q: int) -> int: + numerator = denominator = 1 + for j in range(r): + numerator *= q ** n - q ** j + denominator *= q ** r - q ** j + need(numerator % denominator == 0, "nonintegral Gaussian coefficient") + return numerator // denominator + + +def square_zero_counts() -> list[dict]: + rows = [] + for q, n in COUNT_DOMAINS: + observed = [0] * (n // 2 + 1) + visited = 0 + for s in matrices(q, n): + visited += 1 + if mul(s, s, q) == zero(n): + r = rank(s, q) + need(r <= n // 2, "square-zero rank bound") + observed[r] += 1 + expected = [] + for r in range(n // 2 + 1): + gl = 1 + for j in range(r): + gl *= q ** r - q ** j + expected.append(gaussian(n, r, q) * gaussian(n - r, r, q) * gl) + need(observed == expected, "square-zero rank-stratum count failed") + rows.append({"q": q, "n": n, "matrices_enumerated": visited, + "count_by_rank": observed, "total": sum(observed)}) + return rows + + +def controls() -> dict: + q, p = 5, ((2, 0), (0, 2)) + a = add(mul(p, p, q), eye(2), q, -1) + g = inner_inverse(a, q) + t = ((2, 1), (0, 2)) + e = literal_error(p, inverse(p, q), t, inverse(t, q), q) + need(t != p and all(conditions(a, add(t, p, q, -1), g, q)), "changed optimum") + agreements = 0 + for x in itertools.product(range(q), repeat=4): + agreements += int(vector(e, x, q) == (0,) * 4) + need(agreements == 25, "first fixture must attain 25 of 625 pairs") + bad_square = ((3, 0), (0, 2)) + need(not all(conditions(a, add(bad_square, p, q, -1), g, q)), "square-zero control") + singular_a = ((1, 0), (0, 0)) + bad_image, bad_kernel = ((0, 0), (1, 0)), ((0, 1), (0, 0)) + need(conditions(singular_a, bad_image, singular_a, q) == (False, True, True), + "image containment is necessary") + need(conditions(singular_a, bad_kernel, singular_a, q) == (True, False, True), + "kernel containment is necessary") + need(rank(block(singular_a, bad_image), q) > 1, "image mutant rank") + need(rank(block(singular_a, bad_kernel), q) > 1, "kernel mutant rank") + r = ((4, 1), (4, 1)) + singular_t = add(((2, 0), (0, 3)), r, q) + need(all(conditions(a, r, g, q)) and rank(singular_t, q) == 1, + "admissible Q must separately be invertible") + nilpotent = ((0, 1), (0, 0)) + need(not all(conditions(zero(2), nilpotent, zero(2), 2)), "involutory uniqueness") + return {"changed_scalar_optimum_agreements": agreements, + "first_fixture_pairs": 625, "control_groups": 6} + + +def main() -> None: + result = {"claim_type": "scoped written proof with exact finite corroboration", + "block_equality": equality_lemma(), + "wrapper_classification": wrapper_classification(), + "square_zero_counts": square_zero_counts(), "controls": controls()} + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["source_sha256"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, indent=2, sort_keys=True)) + print("PASS_OPTIMAL_SECOND_CALLEES no_new_kappa") + + +if __name__ == "__main__": + main()