diff --git a/research/right-vector-extension-residue/PROOF.md b/research/right-vector-extension-residue/PROOF.md new file mode 100644 index 0000000000..95f3ab5d40 --- /dev/null +++ b/research/right-vector-extension-residue/PROOF.md @@ -0,0 +1,146 @@ +# Rank-one lifts with a smaller base field + +Let K=F_q be a subfield of L=F_Q. Let R be a finite-dimensional associative +unital L-algebra, with L central, Jacobson radical J, and canonical residue +R/J=L. Thus R=L direct-sum J as a K-vector space. Put z=|J|. Neither +commutativity nor J squared zero is assumed. + +Use two roles. Paid factors are I+u v^T with u in R^2 and v in K^2. +Arbitrary GL_2(K) maps are free anywhere. The cost is the least number of +paid factors. Fix a rank-one matrix A in M_2(L), and consider all z^4 +lifts M=A+N with N in M_2(J). + +For a K-line D in K^2, call D eligible when A v belongs to K^2 minus {0} +for one, equivalently every, nonzero v in D. Let t(A) count these lines. + +## Theorem + +The eligible-line count belongs to {0,1,q}. For each fixed residue A, + +```text +cost 1: C_A = 0 if t(A)=0, + 1+t(A)*(z^2-1) if t(A)>0; +cost 2: z^4-C_A. +``` + +There are no cost-zero targets in these fibers and none needs a third paid +factor. Among all rank-one residues in M_2(L), the exact counts by t are + +```text +N_q = (q+1)*(q^2-1), +N_1 = (q+1)*(q^2-1)*(Q-q), +N_0 = (Q+1)*(Q^2-1) - N_q - N_1. +``` + +Consequently the complete rank-one-residue lift census has + +```text +cost 1: N_q*(q*z^2-q+1) + N_1*z^2 + = (q+1)*(q^2-1)*(Q*z^2-q+1); +cost 2: (Q+1)*(Q^2-1)*z^4 - cost_1. +``` + +When Q=q this specializes to #4770. When Q>q, the cost distribution depends +on the residue. The new contribution is this extension-field classification +and its exact lift and residue counts. The one-factor criterion and unit-pivot +upper bound below are cited predecessor results, not new claims. + +## The predecessor criteria + +Nick Petalas's #4276, Theorems A and D, and the specialization in #4770 give + +```text +cost(M)<=1 iff Mv=w for some nonzero v,w in K^2. +``` + +This criterion holds for any central K-algebra. Our R qualifies even though +its residue is larger than K. Reducing M=A+N modulo J shows that it becomes + +```text +cost(M)<=1 iff some eligible v satisfies Nv=0. +``` + +The split decomposition is essential here: Av is in L^2 and Nv is in +J times J, so Mv lies in K^2 minus {0} exactly when Av lies there and Nv=0. + +Every such M has a unit entry because A is nonzero. The unit-pivot two-factor +bound from #4276 therefore applies. A free GL_2(K) target has invertible +residue over L, so our rank-one residues exclude cost zero. These facts +give exact costs one and two after counting the one-factor lifts. + +## Why only zero, one, or q lines occur + +Write A=a r with nonzero column a in L^2 and nonzero row r over L. +If the L-image line La contains no nonzero K-vector, there is no eligible +line. Otherwise rescale a so a belongs to K^2 minus {0}. Then + +```text +Av belongs to K^2 iff rv belongs to K. +``` + +Indeed one nonzero coordinate of a lies in K and can be inverted in K. +Let U={v in K^2:rv in K} and V={v in K^2:rv=0}. These are K-subspaces, +V is contained in U, and eligible lines are precisely the lines of U outside V. +Put k=dim_K U and h=dim_K V. Since r is nonzero, h<=1. The induced map +U/V into K is injective, so k-h<=1. The only positive possibilities are +(k,h)=(1,0) and (2,1), giving respectively + +```text +t=(q^k-q^h)/(q-1)=1 or q. +``` + +If t=q, U=K^2, so both entries of r lie in K. Thus A itself has K entries +and rank one over K. Conversely every rank-one K-matrix has q eligible +lines. This proves the trichotomy and identifies the q-line class. + +## Count the lifts above each residue + +For each eligible line D, let E_D={N in M_2(J):Nv=0 for v in D}. +Choose a K-basis of K^2 beginning with v. The action of N on that first +basis vector is fixed at zero; its action on the second is arbitrary in +J times J. Hence |E_D|=z^2. If D and D' are distinct, they span K^2, +so E_D intersects E_D' only in N=0. + +When t=0 the union is empty. When t>0 its size is 1+t*(z^2-1). The zero +noise belongs to every nonempty family of events but not to an empty one. +This proves C_A, including J=0. No radical multiplication enters the count. + +## Count the three residue classes + +Over a field of order s there are (s^2-1)^2/(s-1)=(s+1)*(s^2-1) +rank-one 2-by-2 matrices. Count their nonzero outer products and divide by +the s-1 rescalings of either factor. Applying this with s=q gives N_q. + +Double-count pairs (A,D) with A rank one over L and D an eligible K-line. +Fix D and use a GL_2(K) change of input coordinates to make D=K e_1. +The first column w=Ae_1 may be any of the q^2-1 nonzero vectors in K^2. +Rank one over L then forces the second column to be c w for a unique +c in L, giving Q choices. There are q+1 input lines, so + +```text +sum_A t(A) = (q+1)*(q^2-1)*Q = N_1 + q*N_q. +``` + +Solve for N_1 and subtract N_1+N_q from the total number of rank-one +L-matrices to obtain N_0. Multiplying by the per-fiber lift counts proves +the aggregate formula. The projective-line and finite-field counting tools +are classical; their application here is the stated scoped result. + +## First example + +Let K=F2, L=F4, and R=L[e]/e^2, so Q=4 and z=4. Of the 75 rank-one +residues, 9 have t=2, 18 have t=1 and 48 have t=0. Each such residue has +256 lifts. Their respective one-factor counts are 31,16,0. In total, +567 lifts cost one and 18,633 cost two. + +If alpha belongs to F4 minus F2, the matrices + +```text +[[1,0],[0,0]], [[1,alpha],[0,0]], [[alpha,0],[0,0]] +``` + +have t=2,1,0 respectively. With L-valued right vectors and GL_2(L) free +maps instead, #4770's formula gives 4,575 one-factor lifts over these same +75 residues. The smaller base field therefore changes a concrete cost count. + +Produced by Nick Petalas. Predecessor credit and scope are in README.md. diff --git a/research/right-vector-extension-residue/README.md b/research/right-vector-extension-residue/README.md new file mode 100644 index 0000000000..61c1f1a72d --- /dev/null +++ b/research/right-vector-extension-residue/README.md @@ -0,0 +1,154 @@ +# Exact rank-one lift counts over a residue-field extension + +This package was produced by Nick Petalas. It answers Open next question 1 +of [#4770](https://github.com/CrocSwap/integer-mult-bounds/pull/4770) with a +**scoped counting proof and exact finite corroboration**. No new kappa is claimed. + +Let K=F_q be a subfield of L=F_Q. Let R be a finite-dimensional central local +L-algebra with canonical residue R/J=L, and put z=|J|. Paid factors are +I+u v^T with u in R^2 and v in K^2; arbitrary GL_2(K) maps are free anywhere. +Fix a rank-one residue A in M_2(L). Among the q+1 lines in K^2, let t(A) +count those whose nonzero vectors A sends into K^2 minus {0}. Then + +```text +t(A) belongs to {0,1,q}. + +For the z^4 lifts of A: + cost 1 = 0 if t(A)=0; + 1+t(A)*(z^2-1) otherwise. + cost 2 = z^4-cost_1. +``` + +The numbers of rank-one residues in these three classes are exactly + +```text +N_q = (q+1)*(q^2-1) +N_1 = (q+1)*(q^2-1)*(Q-q) +N_0 = (Q+1)*(Q^2-1)-N_q-N_1 +``` + +Thus the total number of one-factor lifts is +`(q+1)*(q^2-1)*(Q*z^2-q+1)`. The remaining rank-one-residue lifts cost two. +Neither radical multiplication nor its nilpotency index enters this formula. +The [proof](PROOF.md) classifies the eligible lines, counts their kernel +fibers, and double-counts eligible residue/line pairs. The one-factor criterion +and unit-pivot two-factor bound are credited inputs from #4276, specialized +in #4770; this package does not audit or rerun their verifiers. + +The first example is R=F4[e]/e^2 over K=F2. Its 75 rank-one residues split +into 9,18,48 residues with t=2,1,0 respectively. Their 19,200 lifts have +exact costs one and two in counts **567** and **18,633**. Allowing F4-valued +right vectors and free maps instead gives 4,575 one-factor lifts by #4770's +formula. The field allowed in the alphabet changes a concrete cost count. + +## Finite evidence + +The standard-library verifier constructs the literal one-factor image +`{(I+u v^T)G}` from every left vector, projective base-field right vector and +free endpoint G. It does not use the eligible-line criterion to construct +this image. It then enumerates every rank-one residue and every lift, comparing +literal membership counts separately at each residue with the new formulas. +The resulting cost-two counts use the cited unit-pivot theorem. + +The eight fixed fixtures use R=L[e]/e^k, including k=1, when J=0. Their +exact cost-one/cost-two counts are: + +- F4 over F2, k=1: 27 / 48. +- F4 over F2, k=2: 567 / 18,633. +- F4 over F2, k=3: 9,207 / 4,905,993. +- F8 over F2, k=1: 63 / 504. +- F8 over F2, k=2: 4,599 / 2,317,833. +- F9 over F3, k=1: 224 / 576. +- F9 over F3, k=2: 23,264 / 5,225,536. +- F16 over F4, k=1: 975 / 3,360. + +All **12,511,409** lifts are enumerated across these fixtures. The residue +classification is also checked separately for every residue. Fields are +polynomial quotients, and F4 inside F16 is identified by a^4=a. Nine controls +cover the three line classes, the empty-union exception, a scalar kernel with +zero image, a missing radical-kernel condition, the first example, changing +the base field, and changing the extension degree. + +Every run emits a generated SHA256 receipt for all six package files. It +writes only to stdout and does not rely on Git, network access, external +packages, cached data or predecessor executable code. All checks use explicit +exceptions and remain enabled with optimized Python. + +## Reproduction + +Run 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-extension-residue/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-extension-residue/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-extension-residue +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-extension-residue --check-source-history +``` + +Any CPython 3.12 interpreter may replace the local absolute path. Both verifier +commands are registered with a 120-second timeout. The expected final marker +is `PASS_RIGHT_VECTOR_EXTENSION_RESIDUE`. SOURCES.json pins the mathematical +predecessors as historical provenance at canonical main +`624de9dc66858af0945e5f8a0942488d62280d43`. There are no live external inputs. + +The current source-binding orientation control passed +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. This is orientation only, not a selected +operator replay. +The formal-interface-lemma card is explicitly changed to this algebraic side +question rather than a proof-assistant or selected-caller obligation. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131534) +identifies the exact question and credited sources. + +## Limits and implementation decisions + +The written proof quantifies over every finite-field extension and every +finite-dimensional central local L-algebra with canonical residue L. The +software checks only the fixed commutative fixtures. Nonsplit residue maps, +noncentral coefficient fields, other residue ranks and more than two roles +are outside the result. Native coefficient preparation, free-map realization, +routing, restoration, precision, stock and a complete supplier bill are unknown. +No supplier admission, complete multiplication theorem or selected-frontier +change is supplied. Independent human and formal proof-kernel review are +unclaimed. No Lean, Docker or selected-construction replay was run. + +The verifier has no recursion, subprocess, solver or variable-size command-line +input. Field size is at most 16, ring size at most 81, nilpotency length at +most three, and base-field size at most four. Arithmetic tables have at most +81^2 entries. A literal image loop has at most +`180*5*81^2` iterations, conservatively combining the separate enforced bounds. +A residue loop has at most 16^4 candidates and a noise loop at most 16^4 +candidates per residue. Only one case and one current target are live at a time. +Each function has fewer than 60 physical lines. Warning-strict ordinary and +optimized runs provide the diagnostics available without additional packages. + +Power of Ten rule 3 has a managed-runtime deviation. Python allocates tuples, +integers, dictionaries and set entries during the finite computation. Live +literal targets are bounded by the paid-image loop above, plus the fixed +arithmetic tables and at most 4,335 residue keys. Each receipt input is capped +at 1 MiB. No persistent resource or steady service is present. A future larger +census needs explicit new memory/runtime bounds; no domain expansion is claimed. + +## Open next questions + +1. What is the one-factor lift distribution above rank-one residues on more + than two roles? A one-factor word fixes a base-field hyperplane, so begin + with three roles and the intersections of eligible hyperplane kernels. + Pairwise intersections need not be just zero; the present line argument + does not classify them. This would test whether a comparable residue-only + count survives at larger role count. +2. Can a native producer and consumer realize this restricted alphabet with + a favorable complete cost? Specify one source and destination contract, + including coefficient preparation, free-map costs and dirty restoration. + These unknown physical costs prevent turning the count into a supplier. + +Structured questions, first steps and blockers are in TASK.json. + +## Credit + +Produced by Nick Petalas. Nick Petalas's #4770 supplies the explicit extension +question and scalar-residue count; #4276 supplies the one-factor and local +unit-pivot criteria; #4243 supplies the free-map normal form. ToikY's #4334 +and Nick Petalas's #4601/#4749 develop related shared-chart local/semilocal +interfaces. Wentao Li's #4099 supplies the paid alphabet and column bound, +following #2513. The finite-field and projective-line tools are classical. +The new claim is their extension-residue counting application. Apache-2.0. diff --git a/research/right-vector-extension-residue/SOURCES.json b/research/right-vector-extension-residue/SOURCES.json new file mode 100644 index 0000000000..8c5d155cef --- /dev/null +++ b/research/right-vector-extension-residue/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/right-vector-rankone-residue/PROOF.md", + "usage": "provenance", + "git_blob": "c3964055ed99504484203c7067bc09d1f79fb97b", + "sha256": "6fd956e364fb9134fb4408b7e117b2474afd38dce2e92d44299ecf011d65ebf5" + }, + { + "path": "research/right-vector-two-factor-criterion/PROOF.md", + "usage": "provenance", + "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c", + "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895" + } + ] +} diff --git a/research/right-vector-extension-residue/TASK.json b/research/right-vector-extension-residue/TASK.json new file mode 100644 index 0000000000..dd9f0366c3 --- /dev/null +++ b/research/right-vector-extension-residue/TASK.json @@ -0,0 +1,124 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "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": "Classify eligible base-field lines and count exact one/two-factor lifts of every rank-one residue over a finite-field extension.", + "scope_change_reason": "Answer explicit Open next question 1 of PR4770. This is an algebraic counting side result, not a selected-caller formalization or a new physical supplier.", + "bottleneck_link": "Shows exactly how restricting right vectors and free maps to a smaller base field changes the singular-interface cost distribution; physical supplier costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified extension-field lift formula. Do not extend to additional residue ranks or role counts.", + "outcome": "completed", + "evidence": "Written scoped proof and complete literal one-factor enumeration on eight fixed extension-field local-algebra fixtures.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the one-factor lift distribution above rank-one residues on more than two roles?", + "why_it_matters": "Tests whether a residue-only counting law survives beyond two roles.", + "first_step": "On three roles count eligible base-field hyperplanes and their common radical kernels.", + "blocked_by": "Kernel intersections need not be the zero tuple, unlike the two-role eligible-line events." + }, + { + "question": "Can a native producer and consumer implement this restricted alphabet at favorable complete cost?", + "why_it_matters": "A formal cost count is not a supplier without paid coefficient and access contracts.", + "first_step": "Specify one producer/consumer pair, including coefficients, free-map implementation and dirty restoration.", + "blocked_by": "Native preparation, routing, precision, restoration and stock costs are unknown." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131534", + "predecessors": [ + { + "pr": 4770, + "head": "39ef149ba3ea8adbda18478ea227d3d0826475ab", + "use": "Explicit extension-field question and scalar-residue count." + }, + { + "pr": 4276, + "use": "One-factor criterion and unit-pivot two-factor upper bound." + } + ], + "overlap": { + "local_notes_searched": 50, + "head_notes": 6319, + "complete_local_inventory": false, + "open_pr_records": 299, + "open_pr_fetched_at": "2026-10-22T19:45:13.565143+00:00", + "discussion_records": 3712, + "discussion_fetched_at": "2026-10-22T19:46:08.245656+00:00", + "complete_remote_pagination": true, + "limitations": "Sparse local notes, arbitrary code diffs and unpublished work are not exhausted. Distinctive main README and merged-PR searches supplement live claims and PR bodies." + } +} diff --git a/research/right-vector-extension-residue/VERIFY.json b/research/right-vector-extension-residue/VERIFY.json new file mode 100644 index 0000000000..78dbc5fc8b --- /dev/null +++ b/research/right-vector-extension-residue/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete literal one-factor image, every rank-one residue and lift, exact per-residue and aggregate formulas, and nine controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete literal one-factor image, every rank-one residue and lift, exact per-residue and aggregate formulas, and nine controls." + } + ] +} diff --git a/research/right-vector-extension-residue/verify.py b/research/right-vector-extension-residue/verify.py new file mode 100644 index 0000000000..80e4f61083 --- /dev/null +++ b/research/right-vector-extension-residue/verify.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +"""Literal finite corroboration of the extension-residue lift count. + +Produced by Nick Petalas. Apache-2.0. No predecessor code is imported. +""" + +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def digits(value: int, base: int, length: int) -> tuple[int, ...]: + result = [] + for _ in range(length): + result.append(value % base) + value //= base + require(value == 0, "coefficient encoding overflow") + return tuple(result) + + +def encode(values: tuple[int, ...], base: int) -> int: + return sum(value * base**i for i, value in enumerate(values)) + + +class Field: + def __init__(self, prime: int, modulus: tuple[int, ...]) -> None: + require((prime, modulus) in ( + (2, (1, 1, 1)), (2, (1, 1, 0, 1)), + (3, (1, 0, 1)), (2, (1, 1, 0, 0, 1))), "unsupported field") + self.p = prime + self.modulus = modulus + self.degree = len(modulus) - 1 + self.size = prime**self.degree + coefficients = [digits(a, prime, self.degree) for a in range(self.size)] + self.add = [[encode(tuple((x + y) % prime for x, y in zip(a, b)), prime) + for b in coefficients] for a in coefficients] + self.mul = [[self.multiply(a, b) for b in coefficients] for a in coefficients] + self.neg = [next(b for b in range(self.size) if self.add[a][b] == 0) + for a in range(self.size)] + require(all(sum(self.mul[a][b] == 1 for b in range(self.size)) == 1 + for a in range(1, self.size)), "not a field") + + def multiply(self, a: tuple[int, ...], b: tuple[int, ...]) -> int: + work = [0] * (2 * self.degree - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + work[i + j] = (work[i + j] + x * y) % self.p + for i in range(len(work) - 1, self.degree - 1, -1): + leading = work[i] + for j in range(self.degree + 1): + k = i - self.degree + j + work[k] = (work[k] - leading * self.modulus[j]) % self.p + return encode(tuple(work[:self.degree]), self.p) + + def power(self, value: int, exponent: int) -> int: + require(0 <= exponent <= 16, "power bound") + result = 1 + for _ in range(exponent): + result = self.mul[result][value] + return result + + +class Ring: + def __init__(self, field: Field, length: int) -> None: + require(1 <= length <= 3 and field.size**length <= 81, "ring bound") + self.field = field + self.length = length + self.size = field.size**length + coefficients = [digits(a, field.size, length) for a in range(self.size)] + self.add = [[encode(tuple(field.add[x][y] for x, y in zip(a, b)), field.size) + for b in coefficients] for a in coefficients] + self.mul = [[self.multiply(a, b) for b in coefficients] for a in coefficients] + + def multiply(self, a: tuple[int, ...], b: tuple[int, ...]) -> int: + f = self.field + work = [0] * self.length + for i in range(self.length): + for j in range(self.length - i): + work[i + j] = f.add[work[i + j]][f.mul[a[i]][b[j]]] + return encode(tuple(work), f.size) + + +def base_objects(field: Field, q: int) -> tuple[tuple[int, ...], list, list]: + require(q in (2, 3, 4) and field.size % q == 0, "base-field bound") + base = tuple(a for a in range(field.size) if field.power(a, q) == a) + require(len(base) == q, "wrong subfield size") + require(all(field.add[a][b] in base and field.mul[a][b] in base + for a in base for b in base), "subfield closure") + lines = [(1, a) for a in base] + [(0, 1)] + gl = [] + for a, b, c, d in product(base, repeat=4): + determinant = field.add[field.mul[a][d]][field.neg[field.mul[b][c]]] + if determinant: + gl.append((a, b, c, d)) + require(len(gl) == (q*q - 1)*(q*q - q), "GL cardinality") + return base, lines, gl + + +def rank_one(field: Field, matrix: tuple[int, ...]) -> bool: + a, b, c, d = matrix + return any(matrix) and field.mul[a][d] == field.mul[b][c] + + +def eligible(field: Field, matrix: tuple[int, ...], base: tuple, lines: list) -> list: + a, b, c, d = matrix + accepted = [] + for x, y in lines: + first = field.add[field.mul[a][x]][field.mul[b][y]] + second = field.add[field.mul[c][x]][field.mul[d][y]] + if (first or second) and first in base and second in base: + accepted.append((x, y)) + require(len(accepted) in (0, 1, len(base)), "eligible-line trichotomy") + return accepted + + +def literal_one_factor(ring: Ring, lines: list, gl: list) -> dict: + """Enumerate P(u,y)G directly; do not use the lift-count criterion.""" + f = ring.field + image = {} + for a, b, c, d in gl: + for x, y in lines: + row0 = f.add[f.mul[x][a]][f.mul[y][c]] + row1 = f.add[f.mul[x][b]][f.mul[y][d]] + for u, v in product(range(ring.size), repeat=2): + matrix = (ring.add[a][ring.mul[u][row0]], + ring.add[b][ring.mul[u][row1]], + ring.add[c][ring.mul[v][row0]], + ring.add[d][ring.mul[v][row1]]) + residue = tuple(entry % f.size for entry in matrix) + if rank_one(f, residue): + image.setdefault(residue, set()).add(encode(matrix, ring.size)) + return image + + +def counts(q: int, extension_size: int) -> dict[int, int]: + scalar = (q*q - 1)**2 // (q - 1) + single = (q + 1)*(q*q - 1)*(extension_size - q) + total = (extension_size**2 - 1)**2 // (extension_size - 1) + return {0: total - scalar - single, 1: single, q: scalar} + + +def predicted(t: int, z: int) -> int: + return 0 if t == 0 else 1 + t*(z*z - 1) + + +def census(ring: Ring, q: int) -> tuple[dict, dict]: + f = ring.field + base, lines, gl = base_objects(f, q) + image = literal_one_factor(ring, lines, gl) + z = ring.size // f.size + histogram = Counter() + one = two = residues = 0 + for matrix in product(range(f.size), repeat=4): + if not rank_one(f, matrix): + continue + residues += 1 + allowed = eligible(f, matrix, base, lines) + histogram[len(allowed)] += 1 + targets = image.get(matrix, set()) + observed = 0 + for noise in product(range(z), repeat=4): + lift = tuple(a + f.size*b for a, b in zip(matrix, noise)) + observed += encode(lift, ring.size) in targets + require(observed == len(targets), "literal image outside lift fiber") + require(observed == predicted(len(allowed), z), "per-residue count") + one += observed + two += z**4 - observed + expected = counts(q, f.size) + require(all(histogram[t] == count for t, count in expected.items()), "residue counts") + require(one + two == residues*z**4, "complete lift partition") + require(one == sum(count*predicted(t, z) for t, count in expected.items()), + "aggregate count") + require(one == (q + 1)*(q*q - 1)*(f.size*z*z - q + 1), "closed total") + result = {"q": q, "Q": f.size, "length": ring.length, "z": z, + "residues": residues, "by_t": expected, "cost1": one, "cost2": two} + return result, image + + +def controls(field: Field, image: dict, result: dict) -> int: + alpha = 2 + base, lines, _ = base_objects(field, 2) + require(len(eligible(field, (1, 0, 0, 0), base, lines)) == 2, "q-line fixture") + require(len(eligible(field, (1, alpha, 0, 0), base, lines)) == 1, "one-line fixture") + require(not eligible(field, (alpha, 0, 0, 0), base, lines), "zero-line fixture") + require(predicted(0, 1) == 0 and 1 + 0*(1 - 1) != predicted(0, 1), + "empty union must not count the zero noise") + ring_size = 16 + bad = (1 + 4, 0, 0, 0) + require(encode(bad, ring_size) not in image[(1, 0, 0, 0)], + "scalar kernel with zero image is ineligible") + bad = (1 + 4, 0, 0, 4) + require(encode(bad, ring_size) not in image[(1, 0, 0, 0)], "radical kill required") + require(result["cost1"] == 567 and result["cost2"] == 18633, "first example") + require(sum(counts(4, 4)[t]*predicted(t, 4) for t in (0, 1, 4)) == 4575 + and result["cost1"] != 4575, "changing the base field changes cost") + require(counts(2, 8) != counts(2, 4), "extension degree must affect residue counts") + return 9 + + +def receipt() -> dict[str, str]: + directory = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = directory / name + require(path.is_file() and not path.is_symlink(), "receipt input missing") + require(path.stat().st_size <= 1024*1024, "receipt input too large") + hashes[name] = sha256(path.read_bytes()).hexdigest() + return hashes + + +def main() -> None: + cases = ((2, (1, 1, 1), 2, 1), (2, (1, 1, 1), 2, 2), + (2, (1, 1, 1), 2, 3), (2, (1, 1, 0, 1), 2, 1), + (2, (1, 1, 0, 1), 2, 2), (3, (1, 0, 1), 3, 1), + (3, (1, 0, 1), 3, 2), (2, (1, 1, 0, 0, 1), 4, 1)) + results = [] + control_count = 0 + for prime, modulus, q, length in cases: + field = Field(prime, modulus) + result, image = census(Ring(field, length), q) + results.append(result) + if field.size == 4 and length == 2: + control_count = controls(field, image, result) + del image + require(control_count == 9, "controls were not run") + total = sum(row["cost1"] + row["cost2"] for row in results) + print(json.dumps({"cases": results, "controls": control_count, + "sha256": receipt()}, indent=2, sort_keys=True)) + print(f"PASS_RIGHT_VECTOR_EXTENSION_RESIDUE lifts={total} controls={control_count}") + + +if __name__ == "__main__": + main()