From bd22290761451093aa7aef1fa7b1421627ab0f37 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 21:21:44 +0100 Subject: [PATCH] feat(research): classify singular polynomial right-vector costs --- research/singular-polynomial-cost/PROOF.md | 138 ++++++++++ research/singular-polynomial-cost/README.md | 116 ++++++++ .../singular-polynomial-cost/SOURCES.json | 30 +++ research/singular-polynomial-cost/TASK.json | 101 +++++++ research/singular-polynomial-cost/VERIFY.json | 32 +++ research/singular-polynomial-cost/verify.py | 249 ++++++++++++++++++ 6 files changed, 666 insertions(+) create mode 100644 research/singular-polynomial-cost/PROOF.md create mode 100644 research/singular-polynomial-cost/README.md create mode 100644 research/singular-polynomial-cost/SOURCES.json create mode 100644 research/singular-polynomial-cost/TASK.json create mode 100644 research/singular-polynomial-cost/VERIFY.json create mode 100644 research/singular-polynomial-cost/verify.py diff --git a/research/singular-polynomial-cost/PROOF.md b/research/singular-polynomial-cost/PROOF.md new file mode 100644 index 0000000000..90536da515 --- /dev/null +++ b/research/singular-polynomial-cost/PROOF.md @@ -0,0 +1,138 @@ +# Exact singular polynomial costs + +Let K be any field, R=K[t], and let the two data roles have paid factors +`I+u y^T`, where u is in R² and y is in K². Every GL2(K) map is free anywhere +in a word. Cost means the least number of paid factors. No scratch is used. + +## Theorem + +The zero matrix has cost two. Every nonzero matrix M with det M=0 has a +factorization `M=a b`, where a is a primitive column in R² and b is a nonzero +row in R². Primitive means that the entries generate R. Write + +```text +V = span_K{b1,b2}, d = monic gcd(b1,b2). +``` + +Its exact cost is + +```text +1 if a belongs to K² and V contains a nonzero constant; +2 otherwise, if a belongs to K² or d belongs to V; +3 otherwise. +``` + +Multiplying a by a nonzero scalar and b by its inverse does not change these +conditions. Every singular target is reachable with at most three factors, +although invertible polynomial targets can have unbounded cost as in #4763. + +## Primitive factorization + +Choose a nonzero column c of M and divide its entries by their monic gcd g, +obtaining a primitive a. Write the other column as c'. The determinant +condition says that c' is a fraction-field multiple h a. Choose r,s in R +with r a1+s a2=1. Then h=r c'1+s c'2 is a polynomial, so both columns are +polynomial multiples of a. This constructs b and proves existence. Two such +primitive a differ by a unit of R, hence by a nonzero scalar. These are +classical PID and Bezout facts. + +A primitive a has a nonzero K-linear annihilating row exactly when a is in +K². Indeed, a nonzero relation makes its entries proportional over K, and +primitivity then makes the common polynomial factor a unit. The converse is +ordinary two-dimensional linear algebra. + +## Three-factor construction + +For every column a and row b over any associative unital ring, direct +multiplication gives + +```text +[[a1,0],[a2,1]] [[1,b2],[0,0]] [[b1,0],[0,1]] = a b. +``` + +The three displayed factors have right vectors e1,e2,e1 respectively, so +all are legal paid factors over R. This uses no free maps. Applying the same +word with a=0 and b=0 also gives zero, but zero already equals the product +`diag(0,1) diag(1,0)` of two paid factors. + +## Exact two-factor boundary + +We use Theorem B of Nick Petalas's #4276, not a new proof of that predecessor: +a two-role target costs at most two exactly when some G,H in GL2(K) make +`N=G M H` satisfy `N12 in N11 R`. In this case `N11 C=N12` supplies the +literal two-factor word + +```text +N = [[N11,0],[N21,1]] [[1,C],[0,N22-N21 C]]. +``` + +For M=a b let phi be the first row of G and let x,z be the columns of H. +Then `N11=(phi a)(b x)` and `N12=(phi a)(b z)`. + +If a is constant, choose phi annihilating a. Both entries vanish and the +criterion passes. If a is not constant, the primitive observation above +makes phi a nonzero for every allowed phi. Since R is an integral domain, +its factor cancels. The criterion becomes `b x divides b z`. The two +polynomials b x,b z generate the same ideal as b1,b2 because H is invertible. +Thus b x must be a nonzero scalar multiple of d. Conversely, if d is a +K-linear combination b x, then x is nonzero, extends to such an H, and d +divides b z. This proves + +```text +cost(M)<=2 iff a is constant or d belongs to V. +``` + +The cancellation and unit statements are specific to K[t]. They do not +assert the same classification in rings with zero divisors. + +## Exact one-factor boundary + +For every two-role target, cost at most one is equivalent to the existence +of nonzero x,w in K² with Mx=w. To see necessity, put a one-factor word in +the predecessor free-map normal form `(I+u y^T) S`. A nonzero constant v in +ker y is fixed by the paid factor; take x=S^-1 v and w=v. The free-only case +has the same property. For sufficiency, choose T in GL2(K) with Tw=x. +Then `(MT-I)w=0`, so the columns of MT-I span at most a one-dimensional +K-space. It is `u y^T` for some allowed u,y, hence `M=(I+u y^T)T^-1`. +This is the one-factor criterion already implicit in #4276, applied here. + +For nonzero rank-one M=a b, equality Mx=w says `a(bx)` is a nonzero constant +column. A nonzero scalar polynomial times a nonzero polynomial has the sum +of their degrees. Consequently a is constant and bx is a nonzero constant. +The converse is immediate. Rank one prevents cost zero since free maps are +invertible. Zero has no nonzero constant image and cannot cost one; its +explicit two-factor word therefore has exact cost two. Combining these +bounds proves every case of the theorem. + +## Sharp example over every field + +Take + +```text +a = (1,t)^T, b = (t,t²+1), +M = [[t,t²+1],[t²,t³+t]]. +``` + +The column is primitive and nonconstant. The row gcd is 1, but no K-linear +combination of t and t²+1 is 1, by comparing degrees two and one. Therefore +cost M=3 over every field, while the general column lower bound delta is at +most two. The above three factors attain it. Multiplying b by a nonzero +nonconstant polynomial leaves the exact cost three unchanged. + +## Scope and credit + +This contribution was produced by Nick Petalas. ToikY's #4334 explicitly +leaves singular targets outside its field-product theorem. Nick Petalas's +#4276 supplies the exact general two-factor criterion, and #4243 supplies +the free-map normal form, following Wentao Li's #4099 and #2513. The +invertible polynomial results #4763 and #4784 are complementary context. +The fixed e1,e2,e1 field-product template of #4780 is related precedent for +the outer-product construction; its basic matrix identity is elementary. +The new result is the complete singular K[t] classification, including the +attaining outer-product word and the all-field sharp example. The gcd and +rank-one factorization facts retain their classical status. Apache-2.0. + +This is a scoped algebraic proof. Native coefficient preparation, routing, +precision, reversible restoration, stock and complete supplier costs remain +unknown. No new kappa, supplier admission or complete multiplication theorem +follows. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/singular-polynomial-cost/README.md b/research/singular-polynomial-cost/README.md new file mode 100644 index 0000000000..59c5769281 --- /dev/null +++ b/research/singular-polynomial-cost/README.md @@ -0,0 +1,116 @@ +# Exact costs for singular polynomial targets + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped algebraic proof with finite corroboration. For every field K, every +determinant-zero target in M2(K[t]) has paid right-vector cost at most three, +with free GL2(K) maps anywhere and no scratch roles. The exact classification +is in [PROOF.md](PROOF.md). No new kappa or supplier admission is claimed. + +For nonzero M, take its primitive polynomial column factorization M=a b. +Let V be the K-span of the two entries of b, and let d be their monic gcd. + +```text +cost 1: a is constant and V contains a nonzero constant; +cost 2: otherwise, a is constant or d belongs to V; +cost 3: otherwise. +zero: cost 2. +``` + +An attaining three-factor word has fixed right vectors e1,e2,e1. Over every +field, `a=(1,t)^T`, `b=(t,t²+1)` gives exact cost three. This settles singular +polynomial endpoints at every degree. Invertible polynomial endpoints can +have unbounded cost, as proved in #4763 and counted in #4784; those results +are complementary, cited context. + +ToikY's #4334 leaves singular targets outside its field-product theorem. +Nick Petalas's #4276 supplies the exact two-factor criterion and #4243 the +free-map normal form, following Wentao Li's #4099 and #2513. These are +credited dependencies, not audit deliverables. The primitive PID and gcd +facts are classical. The e1,e2,e1 field-product template in #4780 is related +precedent for the outer-product word. SOURCES.json pins #4334 and #4276 as +historical provenance. No predecessor code or live input is imported. + +## Evidence + +The verifier enumerates every determinant-zero matrix with the listed entry +degree bounds, using literal polynomial determinants. For each nonzero +matrix it constructs its primitive factorization, compares the new formula +against a separate constant-chart divisibility test, checks the one-factor +constant-image condition and multiplies all three literal paid factors. +The direct two-factor test also returns and multiplies a complete witness, +including its free endpoint maps. Zero is tested separately. + +| Field | Maximum entry degree | Targets | Cost 1 | Cost 2 | Cost 3 | +|---|---:|---:|---:|---:|---:| +| F2 | 4 | 8704 | 279 | 7489 | 936 | +| F3 | 2 | 6561 | 800 | 5761 | 0 | +| F4 | 1 | 2176 | 975 | 1201 | 0 | +| F5 | 1 | 6625 | 3024 | 3601 | 0 | + +These are 24066 distinct targets across four separate domains. Each row +includes zero once in cost two. All 35 enumerated control groups pass. They +cover the sharp example in all four fields, factor order and omission, +constant-image and constant-column exceptions, row-content normalization, +gcd membership, invalid fields and a zero polynomial divisor. All checks +remain active under optimized Python. The generated stdout receipt binds +all six package files by SHA256; no receipt is handwritten. + +## Reproduce + +From the repository root, with the Python 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/singular-polynomial-cost/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/singular-polynomial-cost/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/singular-polynomial-cost +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/singular-polynomial-cost --check-source-history +``` + +Any Python 3.12 interpreter may replace the displayed local path. The direct +marker is `PASS_SINGULAR_POLYNOMIAL_COST targets=24066 controls=35 no_new_kappa`. +Both registered checks must finish within 120 seconds each. + +The original card is explicitly changed to this algebraic side question. +Its historical baseline command stops at an omitted sparse input, +`research/fresh-helper-thinned/PROOF.md`; no baseline or selected scientific +replay pass is claimed. The selected record remains 60403/20000000. + +## Limits and code constraints + +The universal result is the written proof. The finite census corroborates +only the displayed fields and degrees. The exact classification requires +two roles, one polynomial variable and a field of constants. No statement +about multivariate rings, general singular coefficient algebras or more roles +is supplied. Native coefficient preparation, access, routing, precision, +reversible dirty restoration, stock and complete supplier costs are unknown. +No complete multiplication theorem, selected-frontier update, independent +human review or formal proof-kernel acceptance is claimed. Lean, Docker and +selected operator replay are outside scope and were not run. + +The verifier has no recursion, subprocess, dynamic code or indirect callback +chain. Every function is below 60 physical lines. Explicit exceptions retain +checks under -O, and registered commands make warnings errors. Polynomial +capacity is 33 coefficients, bounded division and gcd take at most 34 +iterations, and census inputs are fixed. The largest matrix census considers +32^4 matrices over F2. Product caches contain at most 1024 entries; only +accepted targets are processed further, one at a time. Field operations are +bounded to F2,F3,F4,F5, with F4 represented modulo x²+x+1. Python and the +standard library allocate dynamically. This is a managed-runtime deviation +from fixed allocation, bounded by those input and live-collection capacities. +There is no real-time claim. A future larger census must revise and verify +the resource bounds first. Optional external Python analyzers are not +required and were unavailable; in-memory compilation is the syntax check. + +## Open next questions + +1. Which singular targets are reachable over the nonprincipal domain + K[s²,st,t²]? Start with `[[s²,st],[st,t²]]`, testing its outer-product + factorization and restricted-right-vector reachability. The one-variable + primitive-factorization argument does not supply that step. +2. Can an actual native producer and consumer use one of these words at a + favorable complete cost? Specify coefficient preparation, ownership, + overwrites, restoration, precision and the full paid list before expanding + the construction. Unknown costs are not zero. + +TASK.json records the motivation, first steps and blockers for both questions. diff --git a/research/singular-polynomial-cost/SOURCES.json b/research/singular-polynomial-cost/SOURCES.json new file mode 100644 index 0000000000..2c6cbbc815 --- /dev/null +++ b/research/singular-polynomial-cost/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-commutative-products/README.md", + "usage": "provenance", + "git_blob": "fc9889d41621b596209c707b6057517744b4642f", + "sha256": "6222431360182204f502334d1c707eefc39a174d06578ef75c52f37b5873055f" + }, + { + "path": "research/right-vector-two-factor-criterion/PROOF.md", + "usage": "provenance", + "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c", + "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895" + } + ] +} diff --git a/research/singular-polynomial-cost/TASK.json b/research/singular-polynomial-cost/TASK.json new file mode 100644 index 0000000000..425881fa52 --- /dev/null +++ b/research/singular-polynomial-cost/TASK.json @@ -0,0 +1,101 @@ +{ + "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": "Exact paid right-vector costs for every determinant-zero two-role target over K[t], over any field K.", + "scope_change_reason": "This is an algebraic side result prompted by the singular-target gap in ToikY #4334, rather than a proof-assistant binding of the selected construction.", + "bottleneck_link": "Side result for the restricted right-vector coefficient alphabet. It separates reachable singular polynomial endpoints from the unbounded invertible family; native coefficient preparation, access, restoration and the complete supplier bill remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original classification and package it; no further construction search.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-field classification; verify.py independently enumerates 24066 determinant-zero polynomial matrices, checks the one/two-factor boundaries and constructs every three-factor word. Thirty-five enumerated control groups distinguish sharp and boundary cases.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which singular targets are reachable over K[s\u00b2,st,t\u00b2]?", + "why_it_matters": "A nonprincipal coefficient domain tests the primitive outer-product assumption of the one-variable proof.", + "first_step": "Test outer-product factorization and restricted-right-vector reachability of [[s\u00b2,st],[st,t\u00b2]] in that subring.", + "blocked_by": "A replacement for the one-variable primitive-factorization argument." + }, + { + "question": "Can one native producer and consumer realize a singular polynomial factor word at a favorable complete cost?", + "why_it_matters": "Formal factor counts alone do not admit a recursive supplier.", + "first_step": "Specify coefficient preparation, data ownership, overwrites, restoration, precision and every paid transition at one actual caller.", + "blocked_by": "All native cost and restoration contracts remain unknown." + } + ] +} diff --git a/research/singular-polynomial-cost/VERIFY.json b/research/singular-polynomial-cost/VERIFY.json new file mode 100644 index 0000000000..c11a0bec6b --- /dev/null +++ b/research/singular-polynomial-cost/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": "Literal determinant-zero polynomial census, primitive exact-cost classification, independent constant-chart divisibility, attaining words and 35 boundary/mutation controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all scientific checks with optimization; explicit exceptions remain active." + } + ] +} diff --git a/research/singular-polynomial-cost/verify.py b/research/singular-polynomial-cost/verify.py new file mode 100644 index 0000000000..9bb2c12cdc --- /dev/null +++ b/research/singular-polynomial-cost/verify.py @@ -0,0 +1,249 @@ +"""Bounded, exact corroboration of the singular polynomial cost theorem.""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def addc(a, b, q): + return a ^ b if q == 4 else (a + b) % q + + +def mulc(a, b, q): + if q != 4: + return a * b % q + raw = (a if b & 1 else 0) ^ (a << 1 if b & 2 else 0) + return raw ^ 7 if raw & 4 else raw + + +def negc(a, q): + return a if q == 4 else -a % q + + +def norm(a): + require(len(a) <= 33, 'polynomial capacity') + end = len(a) + for _ in range(len(a)): + if end == 0 or a[end - 1]: + break + end -= 1 + return tuple(a[:end]) + + +def add(a, b, q): + return norm(tuple(addc(a[i] if i < len(a) else 0, + b[i] if i < len(b) else 0, q) + for i in range(max(len(a), len(b))))) + + +def scale(a, c, q): + return norm(tuple(mulc(x, c, q) for x in a)) + + +def mul(a, b, q): + if not a or not b: + return () + require(len(a) + len(b) <= 34, 'product capacity') + out = [0] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + out[i + j] = addc(out[i + j], mulc(x, y, q), q) + return norm(out) + + +def divmodp(a, b, q): + require(bool(b), 'zero polynomial divisor') + r = a + out = [0] * max(0, len(a) - len(b) + 1) + inv = next(c for c in range(1, q) if mulc(c, b[-1], q) == 1) + for _ in range(len(a) + 1): + if len(r) < len(b): + return norm(out), r + shift = len(r) - len(b) + c = mulc(r[-1], inv, q) + out[shift] = c + r = add(r, (0,) * shift + scale(b, negc(c, q), q), q) + raise ValueError('polynomial division exhausted') + + +def gcd(a, b, q): + for _ in range(34): + if not b: + if not a: + return () + inv = next(c for c in range(1, q) if mulc(c, a[-1], q) == 1) + return scale(a, inv, q) + a, b = b, divmodp(a, b, q)[1] + raise ValueError('gcd exhausted') + + +def mm(a, b, q): + return tuple(add(mul(a[2*i], b[j], q), + mul(a[2*i+1], b[2+j], q), q) + for i in range(2) for j in range(2)) + + +def inv2(a, q): + det = addc(mulc(a[0], a[3], q), negc(mulc(a[1], a[2], q), q), q) + require(det != 0, 'singular free map') + c = next(x for x in range(1, q) if mulc(x, det, q) == 1) + return tuple(scale((x,), c, q) for x in + (a[3], negc(a[1], q), negc(a[2], q), a[0])) + + +def dot(a, b, q): + return add(scale(a[0], b[0], q), scale(a[1], b[1], q), q) + + +def directions(q): + return tuple((1, x) for x in range(q)) + ((0, 1),) + + +def primitive(m, q): + j = 0 if m[0] or m[2] else 1 + d = gcd(m[j], m[2+j], q) + a = (divmodp(m[j], d, q)[0], divmodp(m[2+j], d, q)[0]) + b = [] + i = 0 if a[0] else 1 + for k in range(2): + quotient, remainder = divmodp(m[2*i+k], a[i], q) + require(not remainder, 'primitive factorization divisibility') + b.append(quotient) + require(tuple(mul(x, y, q) for x in a for y in b) == m, + 'primitive factorization reconstruction') + require(gcd(*a, q) == (1,), 'primitive column gcd') + return a, tuple(b) + + +def predicted(a, b, q): + constant = all(len(x) <= 1 for x in a) + values = tuple(dot(b, v, q) for v in directions(q)) + if constant and any(len(x) == 1 for x in values): + return 1 + d = gcd(*b, q) + if constant or any(x and len(x) == len(d) and not divmodp(x, d, q)[1] + for x in values): + return 2 + return 3 + + +def direct_one(m, q): + return any((w := (dot(m[:2], v, q), dot(m[2:], v, q))) != ((), ()) + and all(len(x) <= 1 for x in w) for v in directions(q)) + + +def direct_two(m, q): + for phi in directions(q): + row = (dot((m[0], m[2]), phi, q), dot((m[1], m[3]), phi, q)) + for t in directions(q): + s = (0, 1) if t[0] else (1, 0) + left, right = dot(row, t, q), dot(row, s, q) + if not left and right: + continue + if left and divmodp(right, left, q)[1]: + continue + psi = (0, 1) if phi[0] else (1, 0) + g = tuple((x,) if x else () for x in phi + psi) + hraw = (t[0], s[0], t[1], s[1]) + h = tuple((x,) if x else () for x in hraw) + n = mm(mm(g, m, q), h, q) + c = divmodp(n[1], n[0], q)[0] if n[0] else () + f1 = (n[0], (), n[2], (1,)) + f2 = ((1,), c, (), add(n[3], scale(mul(n[2], c, q), negc(1, q), q), q)) + graw = phi + psi + restored = mm(mm(mm(inv2(graw, q), f1, q), f2, q), inv2(hraw, q), q) + require(restored == m, 'two-factor witness') + return True + return False + + +def upper_word(a, b, q): + f = (a[0], (), a[1], (1,)) + g = ((1,), b[1], (), ()) + h = (b[0], (), (), (1,)) + require(mm(mm(f, g, q), h, q) == tuple(mul(x, y, q) for x in a for y in b), + 'three-factor word') + return f, g, h + + +def census(q, degree): + require((q, degree) in ((2, 4), (3, 2), (4, 1), (5, 1)), 'census domain') + polys = tuple(norm(x) for x in product(range(q), repeat=degree + 1)) + products = {(a, b): mul(a, b, q) for a in polys for b in polys} + histogram = [0, 0, 0, 0] + total = 0 + for m in product(polys, repeat=4): + if products[m[0], m[3]] != products[m[1], m[2]]: + continue + total += 1 + if not any(m): + require(not direct_one(m, q) and direct_two(m, q), 'zero exact cost') + histogram[2] += 1 + continue + a, b = primitive(m, q) + cost = predicted(a, b, q) + require((cost == 1) == direct_one(m, q), 'one-factor classification') + require((cost <= 2) == direct_two(m, q), 'two-factor classification') + upper_word(a, b, q) + histogram[cost] += 1 + require(sum(histogram) == total, 'census partition') + return {'q': q, 'degree_at_most': degree, 'targets': total, 'costs': histogram} + + +def controls(): + count = 0 + for q in (2, 3, 4, 5): + a, b = ((1,), (0, 1)), ((0, 1), (1, 0, 1)) + m = tuple(mul(x, y, q) for x in a for y in b) + require(predicted(a, b, q) == 3 and not direct_two(m, q), 'sharp target') + f, g, h = upper_word(a, b, q) + require(mm(mm(h, g, q), f, q) != m, 'reversed word control') + require(mm(f, g, q) != m and mm(g, h, q) != m, 'omitted factors') + require(not direct_one(m, q), 'false one-factor shortcut') + # Scaling the row content cannot turn the cost-three target into cost two. + bscaled = tuple(mul(x, (0, 1), q) for x in b) + require(predicted(a, bscaled, q) == 3, 'gcd normalization control') + require(predicted(((1,), ()), bscaled, q) == 2, 'constant column exception') + require(predicted(((1,), ()), ((1,), (0, 1)), q) == 1, 'cost-one boundary') + require(predicted(a, ((0, 1), (0, 1, 1)), q) == 2, 'gcd in row span') + count += 8 + for invalid in (0, 6): + try: + census(invalid, 1) + except ValueError: + count += 1 + else: + raise ValueError('invalid field accepted') + try: + divmodp((1,), (), 2) + except ValueError: + count += 1 + else: + raise ValueError('zero divisor accepted') + return count + + +def main(): + cases = ((2, 4), (3, 2), (4, 1), (5, 1)) + results = [census(q, d) for q, d in cases] + expected = ((0, 279, 7489, 936), (0, 800, 5761, 0), + (0, 975, 1201, 0), (0, 3024, 3601, 0)) + require(tuple(tuple(x['costs']) for x in results) == expected, 'frozen census counts') + control_count = controls() + require(control_count == 35, 'control coverage') + package = Path(__file__).resolve().parent + hashes = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + receipt = {'results': results, 'control_checks': control_count, 'sha256': hashes} + print(json.dumps(receipt, sort_keys=True)) + print('PASS_SINGULAR_POLYNOMIAL_COST targets=' + str(sum(x['targets'] for x in results)) + + ' controls=' + str(control_count) + ' no_new_kappa') + + +if __name__ == '__main__': + main()