From e35e8bb95491e6bb64b8a7dc7f227360f760f74f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 09:07:57 +0000 Subject: [PATCH] feat(research): classify distinct-pencil quadratic lift costs --- .../distinct-pencil-quadratic-lifts/PROOF.md | 137 +++++++++++ .../distinct-pencil-quadratic-lifts/README.md | 113 +++++++++ .../SOURCES.json | 30 +++ .../distinct-pencil-quadratic-lifts/TASK.json | 121 ++++++++++ .../VERIFY.json | 34 +++ .../distinct-pencil-quadratic-lifts/verify.py | 215 ++++++++++++++++++ 6 files changed, 650 insertions(+) create mode 100644 research/distinct-pencil-quadratic-lifts/PROOF.md create mode 100644 research/distinct-pencil-quadratic-lifts/README.md create mode 100644 research/distinct-pencil-quadratic-lifts/SOURCES.json create mode 100644 research/distinct-pencil-quadratic-lifts/TASK.json create mode 100644 research/distinct-pencil-quadratic-lifts/VERIFY.json create mode 100644 research/distinct-pencil-quadratic-lifts/verify.py diff --git a/research/distinct-pencil-quadratic-lifts/PROOF.md b/research/distinct-pencil-quadratic-lifts/PROOF.md new file mode 100644 index 0000000000..2985b8a869 --- /dev/null +++ b/research/distinct-pencil-quadratic-lifts/PROOF.md @@ -0,0 +1,137 @@ +# Exact cost of distinct-factor quadratic lifts + +Let K be any field, R=K[x,y]/(x,y)^3, and J=(x,y). There are exactly two +roles. The paid alphabet is P(u,v)=I+u v^T with u in R^2 and v in K^2. +Arbitrary GL2(K) factors are free anywhere; singular paid factors are allowed. +The endpoint acts on every input in R^2, with no auxiliary roles. + +Write + +``` +M = [[a,b],[c,d]] = diag(x,y) + Q, Q in M2(J^2), +b = alpha*x^2 + beta*x*y + gamma*y^2, +c = delta*x^2 + epsilon*x*y + zeta*y^2. +``` + +Then the exact minimum number of paid factors is + +``` +cost(M) = 2 if gamma=0 or delta=0; +cost(M) = 3 if gamma and delta are both nonzero. +``` + +The contribution is this distinct-factor pencil classification and its +attaining words. Ali Romman's #5320 asks for another first-order pencil and +classifies a different, repeated-factor binary pencil. Nick Petalas's #4276, +Theorem B, supplies the exact two-factor criterion used below. We cite that +criterion, rather than reprove or scientifically replay its package. + +## Three factors always suffice + +Set s=alpha*x+beta*y. Since J^3=0, + +``` +a*s = alpha*x^2 + beta*x*y, +c*s = 0, y*c = 0, y*d = y^2. +``` + +Consequently the following is an exact identity in M2(R): + +``` +M = [[1,gamma*y],[0,1]] [[a,0],[c,1]] [[1,s],[0,d]]. +``` + +The factors are respectively + +``` +P((gamma*y,0)^T,e2), +P((a-1,c)^T,e1), +P((s,d-1)^T,e2). +``` + +Thus all three are legal paid factors, and there are no free endpoint maps +or preparation assumptions in this formal identity. Multiplication order is +algebraic; execution on column inputs is from right to left. This proves +cost at most three for every Q over every field. + +If gamma=0, omit the identity first factor to obtain a two-factor word. +If delta=0, put r=epsilon*x+zeta*y. Then d*r=c and b*r=0, giving instead + +``` +M = [[1,b],[0,d]] [[a,0],[r,1]]. +``` + +These are paid factors with right rows e2 and e1. They prove the stated +two-factor upper bounds, including their intersection. + +## No other lift has a two-factor word + +Use #4276's criterion: cost(M)<=2 exactly when some G,H in GL2(K) give +N=GMH with N12 in N11 R. Suppose this occurs. Let phi be the first row of +G and t,s the first and second columns of H. There is h in R with + +``` +phi*M*s = (phi*M*t)*h. +``` + +Write h=lambda+h1, with lambda in K and h1 in J, and put v=s-lambda*t. +The vector v is nonzero and t,v remain a K-basis. The equation becomes + +``` +phi*M*v = (phi*M*t)*h1. +``` + +The right side has no linear part. Write phi=(p,q) and v=(v1,v2)^T. +The linear part of the left side is + +``` +p*v1*x + q*v2*y. +``` + +The two linear monomials are independent, so p*v1=q*v2=0. Since both phi +and v are nonzero, exactly one of these cases holds: + +1. phi is a nonzero multiple of e1^T and v is a nonzero multiple of e2. + Then t1 is nonzero because t,v are independent. The left side is a + nonzero K-multiple of b. The linear part of phi*M*t is a nonzero + K-multiple of x. Multiplication by h1 can therefore give only an element + of xJ=span_K{x^2,xy}. Quadratic parts times h1 vanish. Hence b is in xJ, + which is precisely gamma=0. +2. phi is a nonzero multiple of e2^T and v is a nonzero multiple of e1. + Now t2 is nonzero. The same argument places c in + yJ=span_K{xy,y^2}, which is precisely delta=0. + +Thus the cited criterion excludes every word of cost at most two when +gamma and delta are nonzero. This argument includes all constant free charts, +all paid right rows, and factors not aligned with coordinate columns. + +Finally, M has zero scalar residue modulo J. A free endpoint has invertible +residue. A single paid factor has residue I+u0*v^T of rank at least one, +because it fixes ker(v^T) if v is nonzero and is I if v=0. Free factors +preserve that rank. Therefore cost is at least two for every Q. Together +with the constructions, this proves the exact classification. + +## Finite-field count + +For a finite field K of size q, Q has twelve independent coefficients. +The cost-three condition makes gamma and delta nonzero and leaves the other +ten coefficients arbitrary. Therefore, among all q^12 lifts, + +``` +number of cost-three lifts = (q-1)^2*q^10, +number of cost-two lifts = (2*q-1)*q^10. +``` + +For q=2 these counts are 1,024 and 3,072. The total and the classification +are proved by the preceding argument; the software exhaustively enumerates +this binary case. It samples F3, F5 and F7 and does not enumerate their +entire lift spaces or any extension field. + +## Limits + +This is a scoped theorem in the specified formal alphabet. It does not +classify arbitrary first-order pencils or all cube-zero radical targets. +It supplies no native coefficient producer, routing, restoration, precision, +stock, physical caller or recursive supplier bill. Those obligations are +unrun and unknown. No new kappa or complete multiplication theorem follows. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/distinct-pencil-quadratic-lifts/README.md b/research/distinct-pencil-quadratic-lifts/README.md new file mode 100644 index 0000000000..c813c8bcaa --- /dev/null +++ b/research/distinct-pencil-quadratic-lifts/README.md @@ -0,0 +1,113 @@ +# Exact two-versus-three cost for distinct-factor quadratic lifts + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof with exhaustive binary corroboration.** +For every field K, let R=K[x,y]/(x,y)^3 and J=(x,y). On exactly two roles, +allow paid factors I+u v^T with u in R^2 and v in K^2, arbitrary free +GL2(K) maps, and singular paid factors. Write + +``` +M = diag(x,y) + Q, Q in M2(J^2), +gamma = coefficient of y^2 in Q12, +delta = coefficient of x^2 in Q21. + +cost(M) = 2 if gamma=0 or delta=0, and 3 otherwise. +``` + +Every lift is reachable. For a finite field of size q, the exact counts are +(2q-1)q^10 lifts of cost two and (q-1)^2 q^10 of cost three. For F2 the +counts are 3,072 and 1,024. No new kappa is claimed. + +[PROOF.md](PROOF.md) gives the all-field argument. A radical shear followed +by two column replacements supplies the upper bound. The cited two-factor +ideal criterion reduces the lower bound to the two displayed coefficients. +The exact cost concerns arbitrary inputs in R^2, with no zero-input or +scratch assumption. + +## What this adds + +Ali Romman's [#5320](https://github.com/CrocSwap/integer-mult-bounds/pull/5320), +`research/cube-zero-lift-obstruction`, asks for another first-order pencil. +It classifies the binary repeated-factor pencil [[x,y],[y,x]], with some +unreachable lifts. This package settles the distinct-factor pencil diag(x,y) +over every field, with every lift reachable and some needing a third factor. +Its proof and computations concern the new pencil only. No predecessor +scientific verifier or census is imported, replayed or audited. + +Nick Petalas's [#4276](https://github.com/CrocSwap/integer-mult-bounds/pull/4276) +supplies the exact two-factor criterion; #4764 supplies an earlier separate +pure-quadratic cost-three example. Wentao Li's #4099 following #2513 supplies +the alphabet, and ToikY's #4334 supplies related common-chart context. Classical +truncated-polynomial arithmetic and coefficient counting retain their credit. + +## Evidence and reproduction + +From the repository root, use CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/distinct-pencil-quadratic-lifts/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/distinct-pencil-quadratic-lifts/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/distinct-pencil-quadratic-lifts +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/distinct-pencil-quadratic-lifts --check-source-history +``` + +Another CPython 3.12 path may replace the local path. The direct scientific +marker is `PASS_DISTINCT_PENCIL_QUADRATIC_LIFTS no_new_kappa`. The checker +writes nothing and emits a generated receipt binding all package files. + +The checker enumerates all 4,096 binary lifts. For each, it compares the new +coefficient test with the cited principal-ideal criterion. It searches free +GL2(F2) endpoint pairs until a witness is found, and exhausts all 36 pairs +for each rejection. It replays every attaining word and checks the action on +all twelve K-basis inputs of R^2. There are 49,152 basis-input comparisons. +The coefficientwise ring multiplication and packed binary action are separate +calculation paths. The criterion is a cited theorem; these checks apply it +to the new targets rather than independently validating that predecessor. + +The checker also replays explicit words on 34, 74 and 122 distinct samples +over F3, F5 and F7. Samples include every single-coordinate perturbation and +one dense perturbation for every pair (gamma,delta), with exact deduplication. +Eight rejecting controls cover four omitted/reversed words, an odd-field +sign error, and three invalid inputs. Ring controls distinguish square-zero +from cube-zero truncation. Checks stay active under optimized Python. +Both registered commands were timed separately on CPython 3.12.15 at +0.33 seconds each. The complete registered launcher also passed. + +[SOURCES.json](SOURCES.json) pins the unchanged source prose, catalogue and +selected record as historical provenance at canonical main +`e54523517d0f03e58352e647c403a5af3e525a57`. No external runtime input is read. +The source-binding orientation passed with +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it is not a selected operator replay. + +## Scope and implementation limits + +The card formal-interface-lemma is explicitly changed to an algebraic side +question. This locates one boundary where cubic nilpotence permits a third +paid update; it does not discharge a selected framework assumption. The +selected frontier is unchanged. Native preparation, physical movement, +restoration, precision, stock and the complete recursive invoice remain +unknown. No native, compiler, Lean, Docker or selected scientific cold replay +was run. Independent human and formal proof-kernel review are unclaimed. + +The offline checker has no recursion, subprocesses or dynamic evaluation. +All loops have fixed finite domains: six monomials, 64 binary ring elements, +six binary free matrices, 4,096 binary targets, twelve basis inputs, and at +most 122 stored samples per odd field. Every function is under sixty physical +lines. CPython managed allocation is a deviation from fixed allocation, +bounded by these domains and the 64-by-64 multiplication table. Explicit +contracts and warning-strict normal/optimized runs provide the available +runtime diagnostics. No external static analyzer or proof kernel is claimed. + +## Open next questions + +1. Classify lifts with a rank-one first-order pencil, such as diag(x,0). + Start with a three-factor normal form and retain its second-order terms. + The present proof uses two independent diagonal linear forms and does + not supply the necessary all-word obstruction for that pencil. +2. Bind an attaining three-factor word to a literal native producer and + consumer. First price its radical coefficient shear, overwritten inputs + and restoration in one actual caller. Coefficient availability and a + complete physical invoice remain the blockers. + +Structured next steps and the bounded stop rule are in [TASK.json](TASK.json). diff --git a/research/distinct-pencil-quadratic-lifts/SOURCES.json b/research/distinct-pencil-quadratic-lifts/SOURCES.json new file mode 100644 index 0000000000..411355fad7 --- /dev/null +++ b/research/distinct-pencil-quadratic-lifts/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/cube-zero-lift-obstruction/README.md", + "usage": "provenance", + "git_blob": "10044ad7c5bdce30e67d756805b790f8fab1f07e", + "sha256": "36fc090489e43f8d73355aeeb7eac717d3d3a359b3abdf22530fc51a4068da20" + }, + { + "path": "research/right-vector-two-factor-criterion/PROOF.md", + "usage": "provenance", + "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c", + "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895" + } + ] +} diff --git a/research/distinct-pencil-quadratic-lifts/TASK.json b/research/distinct-pencil-quadratic-lifts/TASK.json new file mode 100644 index 0000000000..b7ee40fb2b --- /dev/null +++ b/research/distinct-pencil-quadratic-lifts/TASK.json @@ -0,0 +1,121 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact two-versus-three paid right-vector cost of every quadratic lift of diag(x,y) over K[x,y]/(x,y)^3, for every field K and exactly two roles.", + "scope_change_reason": "Ali Romman PR5320 leaves another first-order pencil open. This algebraic side result does not formalize a selected caller or discharge the original card acceptance gate.", + "bottleneck_link": "It distinguishes a local algebraic boundary where all quadratic lifts are reachable but a third paid update is sometimes necessary. Physical coefficient preparation and the complete supplier bill remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact pencil classification, written proof, bounded replay and publication; leave other pencils and physical lowering open.", + "outcome": "completed", + "evidence": "All-field written proof; all 4096 binary lifts, 3072 cost-two and 1024 cost-three, 49152 basis actions, 34/74/122 odd-field samples, and eight rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Classify quadratic lifts with first-order pencil diag(x,0).", + "why_it_matters": "It is the next first-order rank stratum and tests which parts of the distinct-factor proof survive.", + "first_step": "Analyze a three-factor normal form and its retained second-order terms for this rank-one pencil.", + "blocked_by": "The current proof uses two independent diagonal linear forms." + }, + { + "question": "Can an actual native caller realize and fully price the attaining three-factor word?", + "why_it_matters": "Formal paid factors do not by themselves supply a recursive improvement.", + "first_step": "Price one radical coefficient shear, input preservation and restoration for a named caller.", + "blocked_by": "No native coefficient producer or complete physical invoice is supplied." + } + ], + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538491", + "upstream_checkpoint": { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "priority_revision": 8, + "checked_at": "2026-11-11T09:07:00Z" + }, + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library only", + "local_interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "overlap": { + "checked_at": "2026-11-11T09:07:00Z", + "source_pr": 5320, + "source_author": "aliromman", + "main_search": "Git-object README searches for quadratic lifts, diagonal pencils, distinct factors and diag(x,y); targeted merged PR search repeated before commit.", + "live_search": "Open PR metadata and last sixteen handoff comments refreshed immediately before commit; local reservations read.", + "coverage_limits": "The overlap helper has complete cached remote pagination but sparse local-note coverage; arbitrary historical diffs and unpublished work are not covered.", + "related_open_work": "No open PR studying this quadratic-lift pencil identified in the checked titles and bodies." + } +} diff --git a/research/distinct-pencil-quadratic-lifts/VERIFY.json b/research/distinct-pencil-quadratic-lifts/VERIFY.json new file mode 100644 index 0000000000..87525235b1 --- /dev/null +++ b/research/distinct-pencil-quadratic-lifts/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 4096 new binary lifts, complete principal-ideal/free-chart comparison, attaining words, 49152 basis actions, odd-field samples and eight rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 4096 new binary lifts, complete principal-ideal/free-chart comparison, attaining words, 49152 basis actions, odd-field samples and eight rejecting controls." + } + ] +} diff --git a/research/distinct-pencil-quadratic-lifts/verify.py b/research/distinct-pencil-quadratic-lifts/verify.py new file mode 100644 index 0000000000..1722ee2713 --- /dev/null +++ b/research/distinct-pencil-quadratic-lifts/verify.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Exact new-pencil checks; no predecessor executable is imported.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +MONOMIALS = ((0, 0), (1, 0), (0, 1), (2, 0), (1, 1), (0, 2)) +ZERO = (0,) * 6 +ONE = (1, 0, 0, 0, 0, 0) +X = (0, 1, 0, 0, 0, 0) +Y = (0, 0, 1, 0, 0, 0) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(a, b, p): + return tuple((a[i] + b[i]) % p for i in range(6)) + + +def scale(a, scalar, p): + return tuple(scalar * value % p for value in a) + + +def multiply(a, b, p): + result = [0] * 6 + for i, (ax, ay) in enumerate(MONOMIALS): + for j, (bx, by) in enumerate(MONOMIALS): + power = (ax + bx, ay + by) + if sum(power) <= 2: + result[MONOMIALS.index(power)] += a[i] * b[j] + return tuple(value % p for value in result) + + +def matmul(a, b, p): + return tuple(add(multiply(a[2*i], b[j], p), + multiply(a[2*i+1], b[2+j], p), p) + for i in range(2) for j in range(2)) + + +def target(coefficients, p): + require(len(coefficients) == 12, "twelve quadratic coefficients required") + require(p in (2, 3, 5, 7), "unsupported prime field") + require(all(type(c) is int and 0 <= c < p for c in coefficients), + "noncanonical field coefficient") + entries = tuple((0, 0, 0, *coefficients[3*i:3*i+3]) for i in range(4)) + return (add(X, entries[0], p), entries[1], entries[2], + add(Y, entries[3], p)) + + +def construct(m, p): + a, b, c, d = m + gamma, delta = b[5], c[3] + if gamma == 0: + s = (0, b[3], b[4], 0, 0, 0) + return ((a, ZERO, c, ONE), (ONE, s, ZERO, d)) + if delta == 0: + r = (0, c[4], c[5], 0, 0, 0) + return ((ONE, b, ZERO, d), (a, ZERO, r, ONE)) + s = (0, b[3], b[4], 0, 0, 0) + return ((ONE, scale(Y, gamma, p), ZERO, ONE), + (a, ZERO, c, ONE), (ONE, s, ZERO, d)) + + +def check_word(m, word, p): + product = (ONE, ZERO, ZERO, ONE) + for factor in word: + first = (factor[0] != ONE or factor[2] != ZERO) + second = (factor[1] != ZERO or factor[3] != ONE) + require(first != second, "factor must change exactly one scalar column") + product = matmul(product, factor, p) + require(product == m, "literal paid word has wrong endpoint") + + +def binary_tables(): + elements = tuple(tuple((a >> i) & 1 for i in range(6)) for a in range(64)) + table = tuple(tuple(sum(c << i for i, c in enumerate(multiply(a, b, 2))) + for b in elements) for a in elements) + ideals = tuple(frozenset(row) for row in table) + gl = tuple(m for m in itertools.product(range(2), repeat=4) + if (m[0]*m[3] - m[1]*m[2]) % 2 == 1) + require(len(gl) == 6 and len(ideals) == 64, "binary table bounds") + return table, ideals, gl + + +def binary_matmul(a, b, table): + return tuple(table[a[2*i]][b[j]] ^ table[a[2*i+1]][b[2+j]] + for i in range(2) for j in range(2)) + + +def binary_two_factor(m, table, ideals, gl): + # Literal cited criterion: some GMH has N12 in the principal ideal N11 R. + # This scans every free endpoint; it does not use the new coefficient test. + for g in gl: + gm = binary_matmul(g, m, table) + for h in gl: + n = binary_matmul(gm, h, table) + if n[1] in ideals[n[0]]: + return True + return False + + +def binary_action(m, v, table): + return (table[m[0]][v[0]] ^ table[m[1]][v[1]], + table[m[2]][v[0]] ^ table[m[3]][v[1]]) + + +def pack(m): + return tuple(sum(c << i for i, c in enumerate(entry)) for entry in m) + + +def binary_census(): + table, ideals, gl = binary_tables() + counts = {2: 0, 3: 0} + basis = tuple((1 << i, 0) for i in range(6)) + tuple( + (0, 1 << i) for i in range(6)) + digest = hashlib.sha256() + actions = 0 + for coefficients in itertools.product(range(2), repeat=12): + m = target(coefficients, 2) + word = construct(m, 2) + encoded = pack(m) + predicted = coefficients[5] == 0 or coefficients[6] == 0 + require(binary_two_factor(encoded, table, ideals, gl) == predicted, + "new cost test disagrees with complete free-chart criterion") + require(len(word) == (2 if predicted else 3), "wrong paid length") + check_word(m, word, 2) + packed_word = tuple(pack(factor) for factor in word) + for v in basis: + state = v + for factor in reversed(packed_word): + state = binary_action(factor, state, table) + require(state == binary_action(encoded, v, table), "basis action") + actions += 1 + counts[len(word)] += 1 + digest.update(bytes((*encoded, len(word)))) + require(counts == {2: 3072, 3: 1024}, "binary closed-form count") + return {"targets": sum(counts.values()), "cost_counts": counts, + "basis_actions": actions, "records_sha256": digest.hexdigest()} + + +def odd_samples(): + report = {} + for p in (3, 5, 7): + coefficients = {(0,) * 12} + for i in range(12): + for value in range(1, p): + row = [0] * 12 + row[i] = value + coefficients.add(tuple(row)) + for gamma, delta in itertools.product(range(p), repeat=2): + row = [(i*i + 3*i + gamma + 2*delta) % p for i in range(12)] + row[5], row[6] = gamma, delta + coefficients.add(tuple(row)) + counts = {2: 0, 3: 0} + for row in sorted(coefficients): + m = target(row, p) + word = construct(m, p) + check_word(m, word, p) + counts[len(word)] += 1 + require(sum(counts.values()) == len(coefficients), "sample accounting") + report[str(p)] = {"targets": len(coefficients), "word_lengths": counts} + return report + + +def controls(): + row = [0] * 12 + row[5], row[6] = 1, 1 + m = target(row, 3) + word = construct(m, 3) + rejected = 0 + mutants = (word[1:], tuple(reversed(word)), word[:1] + word[2:], word[:2]) + for mutant in mutants: + try: + check_word(m, mutant, 3) + except ValueError: + rejected += 1 + require(rejected == 4, "omission or order mutant survived") + wrong_sign = ((ONE, scale(Y, -1, 3), ZERO, ONE), *word[1:]) + try: + check_word(m, wrong_sign, 3) + except ValueError: + rejected += 1 + require(rejected == 5, "odd-characteristic sign mutant survived") + for bad, p in (((0,) * 11, 2), ((0,) * 12, 4), ((3,) * 12, 3)): + try: + target(bad, p) + except ValueError: + rejected += 1 + require(rejected == 8, "input boundary mutant survived") + require(multiply(X, Y, 2) != ZERO, "cube-zero differs from square-zero") + require(multiply(multiply(X, Y, 2), X, 2) == ZERO, "cubic truncation") + return rejected + + +def main(): + result = {"binary": binary_census(), "odd_field_samples": odd_samples(), + "rejecting_controls": controls()} + package = Path(__file__).resolve().parent + result["files_sha256"] = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", + "VERIFY.json", "verify.py") + } + print(json.dumps(result, sort_keys=True)) + print("PASS_DISTINCT_PENCIL_QUADRATIC_LIFTS no_new_kappa") + + +if __name__ == "__main__": + main()