From 913a75e5735702cc39559af1be8a8fd510c42c02 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:12:11 +0000 Subject: [PATCH] feat(research): prove singular Veronese reachability obstruction --- .../veronese-singular-obstruction/PROOF.md | 132 ++++++++++ .../veronese-singular-obstruction/README.md | 158 +++++++++++ .../SOURCES.json | 36 +++ .../veronese-singular-obstruction/TASK.json | 124 +++++++++ .../veronese-singular-obstruction/VERIFY.json | 34 +++ .../veronese-singular-obstruction/verify.py | 249 ++++++++++++++++++ 6 files changed, 733 insertions(+) create mode 100644 research/veronese-singular-obstruction/PROOF.md create mode 100644 research/veronese-singular-obstruction/README.md create mode 100644 research/veronese-singular-obstruction/SOURCES.json create mode 100644 research/veronese-singular-obstruction/TASK.json create mode 100644 research/veronese-singular-obstruction/VERIFY.json create mode 100644 research/veronese-singular-obstruction/verify.py diff --git a/research/veronese-singular-obstruction/PROOF.md b/research/veronese-singular-obstruction/PROOF.md new file mode 100644 index 0000000000..92c8b1674a --- /dev/null +++ b/research/veronese-singular-obstruction/PROOF.md @@ -0,0 +1,132 @@ +# Singular reachability over coefficient domains + +This contribution was produced by Nick Petalas. Apache-2.0. + +Let K be any field and R any commutative integral domain containing K. +There are exactly two data roles. A paid factor is `I+u v^T`, where +`u in R^2` and `v in K^2`. Any `GL_2(K)` factor is free, anywhere in a +finite word. There are no extra roles. Multiplication is ordinary matrix +multiplication over R. Reachability means equality of the complete matrix, +so every input column is covered. It does not mean a reversible dirty +workspace contract or a native implementation. + +## Theorem + +For a matrix M in `M_2(R)` with determinant zero, the following are equivalent: + +1. M is reachable by a finite word in this alphabet. +2. M factors as `M=a b`, with `a in R^2` a column and `b in R^(1 by 2)` a row. +3. M is reachable with at most three paid factors. + +In particular a singular target is either reachable within three paid factors +or unreachable at every finite length. This is a reachability classification, +not an exact classification of the minimum within the reachable cases. + +### Necessity + +The determinant identity for a paid factor N is + +```text +det(I+u v^T) = 1+v^T u. +``` + +The determinant of a free factor is nonzero. Since R is an integral domain, +a word with determinant zero must contain a paid factor N with determinant +zero. Then `v != 0` and + +```text +v^T N = (1+v^T u) v^T = 0. +``` + +The kernel of the nonzero constant row `v^T` is a free rank-one R-module +generated by a constant column. This requires only division by a nonzero +element of K. Explicitly, if `v1 != 0`, take + +```text +a0 = (-v2/v1, 1)^T, b0 = row 2 of N. +``` + +Each column of N is in that kernel, so `N=a0 b0`. If `v1=0`, then `v2 != 0` +and `N=e1 (row 1 of N)`. Write the whole word as `M=A N B`, with A and B +the products on its two sides, including all free factors. Therefore + +```text +M = (A a0) (b0 B). +``` + +Both factors have entries in R. Neither A nor B needs to be invertible. +This proves necessity without bounding the length or assuming a special +position for the singular factor. + +### Sufficiency + +We use the outer-product constructor of Nick Petalas's #4808, cited rather +than claimed as new. For any a and b over R, + +```text +[[a1,0],[a2,1]] [[1,b2],[0,0]] [[b1,0],[0,1]] = a b. +``` + +The three right vectors are respectively `e1,e2,e1`; hence these are legal +paid factors. This also handles zero factors. The identity gives (2) => (3), +and (3) => (1) is immediate. The new direction is the necessity above. + +## An all-field unreachable singular target + +Take `R=K[s^2,st,t^2]`, the indicated subring of the polynomial domain +`K[s,t]`, and + +```text +M = [[s^2,st],[st,t^2]]. +``` + +Its determinant is zero, and its rank over the fraction field is one. +Nevertheless it has no outer-product factorization over R. + +Suppose `M=a b`. All four entries of a and b are nonzero, because all four +entries of M are nonzero. In the polynomial UFD `K[s,t]`, the entry a1 +divides both `s^2` and `st`. Thus a1 divides their gcd s, so a1 is a nonzero +constant or a nonzero constant times s. Every polynomial in R has only +monomials of even total degree, so the second case is impossible. Write +`a1=c in K^*`. Then `b1=s^2/c`, while `a2 b1=st` would require + +```text +a2 = c t/s, +``` + +which is not in `K[s,t]`. This is a contradiction. The proof works in every +characteristic. By the theorem, M is unreachable at every finite paid length, +even with free `GL_2(K)` factors anywhere. + +The polynomial UFD fact and gcd computation are classical. The new result +is the right-vector reachability criterion and its consequence for the +explicit open target in #4808. No general ring-theory priority is claimed. + +## Why the hypotheses matter + +Over the larger coefficient domain `K[s,t]`, the same target is +`(s,t)^T (s,t)` and is reachable within three paid factors by the cited word. +The missing coefficients s and t matter. Every scalar specialization of +s and t is also an outer product over K. Such finite evaluations cannot +prove the polynomial obstruction. + +The domain hypothesis is used to obtain a determinant-zero factor from a +determinant-zero product. No version for rings with zero divisors is asserted. +The proof uses exactly two roles and constant right vectors; additional +restored roles or a different alphabet require a separate argument. + +## Credit and limits + +Nick Petalas #4808 supplies the explicit nonprincipal-domain open question +and the sufficient three-factor constructor. ToikY #4334 leaves singular +endpoints outside its commutative field-product theorem. Nick Petalas +#4276/#4243 supplies the right-vector and free-map context, following +Wentao Li #4099 and #2513. Those contributions are dependencies and context, +not audit deliverables. Their sources and credit remain unchanged. + +This is a scoped algebraic proof. The verifier corroborates exact identities +and stated finite domains; it is not a proof-kernel formalization. Native +coefficient preparation, access, routing, precision, reversible restoration, +stock and complete supplier costs are unknown. No new kappa, supplier +admission, selected-frontier change or complete multiplication theorem is +claimed. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/veronese-singular-obstruction/README.md b/research/veronese-singular-obstruction/README.md new file mode 100644 index 0000000000..0027325998 --- /dev/null +++ b/research/veronese-singular-obstruction/README.md @@ -0,0 +1,158 @@ +# Singular reachability and a Veronese obstruction + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped algebraic proof with exact finite corroboration. For every field K +and every commutative integral domain R containing K, a determinant-zero +matrix on exactly two roles is reachable in the constant-right-vector +alphabet if and only if it has an outer-product factorization over R. +Every reachable singular target therefore needs at most three paid factors. + +```text +paid factors: I+u v^T, u in R^2, v in K^2 +free factors: arbitrary GL_2(K) maps anywhere +singular M: reachable <=> M=a b over R <=> cost <= 3 +``` + +The explicit target `[[s²,st],[st,t²]]` over `K[s²,st,t²]` has determinant +zero and fraction-field rank one, but is unreachable at every finite paid +length, over every field K. This answers Open next question 1 of #4808. +The new result is the necessary factorization invariant and its application +to that target. The sufficient three-factor constructor is cited from +Nick Petalas's #4808, not claimed as new. [PROOF.md](PROOF.md) gives the +complete argument. No new kappa or supplier admission is claimed. + +## Evidence + +The standard-library verifier checks the new singular-factor extraction +and its preservation through complete wrapped matrix words. Over F2 it +examines all 768 paid-factor parameter choices with nonzero constant right +vector and coefficients in the span of `1,s²,st,t²`, finding 48 singular +choices. Over F3 it examines all 52,488 such choices, finding 648 singular +choices. Different parameter choices may give the same matrix. All 696 +extracted factorizations and all 696 wrapped endpoints +pass literal polynomial matrix multiplication. Each wrapped word includes +paid factors on both sides and nontrivial free maps. + +Complete factor searches for the Veronese target consider 256 first-entry +pairs over F2, 6,561 over F3 and 390,625 over F5. Respectively 2, 4 and 8 +pairs multiply to s², and none extends to the complete target. These are +397,442 first-entry candidate pairs across three separate domains. No +outer-product factors of higher degree are omitted: each nonzero factor +entry has total degree at most two, since total degrees add in a polynomial +domain and every target entry has degree two. The full degree-at-most-two +part of R is exactly the span of `1,s²,st,t²`. + +Controls cover ten constructor words over Z,F2,F3,F5,F7, all fifteen +single-factor omissions in five nonconstant words, five determinant +mutations and five larger-ring controls. The larger ring `K[s,t]` admits +the target as `(s,t)^T(s,t)`, so allowing the missing coefficients removes +the obstruction. Another 3,123 scalar input comparisons over F2,F3,F5,F7 +show that scalar specializations are outer products; these do not prove +the polynomial obstruction. Three invalid-domain/degree controls, one +accepted capacity boundary and two capacity/singular-premise rejection +controls pass. All counts are enumerated by the verifier. + +The universal claim is the written proof. Exact finite checks corroborate +only the stated domains. The generated stdout receipt binds all six +package files by SHA256; no receipt is handwritten. No predecessor +scientific verifier is imported or replayed. + +## Reproduce + +From the repository root, with the CPython 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/veronese-singular-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/veronese-singular-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/veronese-singular-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/veronese-singular-obstruction --check-source-history +``` + +Another CPython 3.12 installation may replace the displayed interpreter. +Expected markers are `PASS_VERONESE_SINGULAR_OBSTRUCTION no_new_kappa`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +Each registered command has a 120-second limit. Explicit checks remain +enabled under optimized Python. The last command needs committed package +bytes and full Git history. The direct verifier also runs in a Git-free +export without predecessor files. + +## Scope and provenance + +Base is canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority +revision 8. The selected source-binding orientation passed and separates +complex, ordinary BIT, admitted BIT and outer budgets. It is metadata +orientation, not a selected scientific replay. Selected conditional kappa +remains `62009/20000000`. + +The original `formal-interface-lemma` card is explicitly changed to this +algebraic side result in [TASK.json](TASK.json). Its relevance is target +feasibility in a declared alphabet, not a reduction of the selected five +framework assumptions. [SOURCES.json](SOURCES.json) pins the original card, +selected record and predecessor proof text as historical provenance. The +verifier reads no predecessor source as a live input. + +[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214451). +Live PRs, recent account PRs, handoffs, active Discussions, local reservations, +all-main README terms and distinctive merged-PR searches were checked. +The overlap cache covers 416 open PRs and 5,312 Discussion records with +complete remote pagination. Local notes are sparse and incomplete; arbitrary +historical diffs, unpublished work and global literature priority are not +covered. Merged #4808 is the explicit open-target predecessor. Merged +Ali Romman #5454 concerns factorable targets over cube-zero algebras and +does not establish this domain obstruction. + +## Credit + +Nick Petalas #4808 supplies the explicit question and the sufficient +three-factor constructor; #4276/#4243 supplies the two-role right-vector +and free-map context, following Wentao Li #4099 and #2513. ToikY #4334 +supplies the commutative field-product result and its singular-endpoint +gap. Classical polynomial UFD, gcd and rank-one factorization facts retain +their classical status. The new direction is singular reachability implies +factorization over the coefficient domain, together with the resulting +all-field unreachable target. All predecessor files and credit are retained. + +## Limits and code constraints + +Exactly two roles, a commutative integral domain, base-field right vectors +and base-field free maps are essential hypotheses. No new classification of +exact cost one versus two versus three, zero-divisor rings or extra roles +is supplied. Native coefficient preparation, frames, routing, precision, +reversible restoration, stock and a complete supplier invoice remain +unknown. No complete multiplication theorem or selected-frontier change +follows. Independent human and formal proof-kernel review are unclaimed. +Lean, Docker and the selected scientific replay are outside scope and unrun. + +The verifier has no recursion, subprocess, network, dynamic code or write +path. Its nineteen functions are at most 42 physical lines. Fixed fields +and degree limits bound every loop: each polynomial has at most 45 terms, +each product considers at most 2,025 term pairs, the largest factor search +considers 625² first-entry pairs, and scalar input loops have at most 7^4 +iterations. Matrix dimensions are two and wrapped words have five factors. +Receipt reads are capped at 128 KiB plus one guard byte for each of six +fixed files. Warning-strict normal/optimized execution and in-memory +compilation supply the available diagnostics; no external analyzer was +installed or run. + +Power of Ten rule 3 deviation: CPython and the standard library allocate +dynamically. Scope is this fixed finite verifier only. Immutable polynomial +values, explicit degree/term limits, at most 625 live search polynomials +and six bounded receipt reads limit live collections; temporary product +dictionaries have at most 2,025 keys before capacity rejection. This is not +a real-time or allocator-internals claim. The verifier checks malformed +fields/degrees and capacity at polynomial construction. Any larger domain +must revise and verify these limits before expansion. + +## Open next questions + +1. Can one extra restored role realize `diag(M,1)` for the obstructed target? + Start with the same constant-right-vector alphabet and preserve the third + input and output exactly. The two-role rank-one argument does not supply + a three-role obstruction or construction. +2. Which reachable singular targets over a specified non-PID domain need + one, two or three paid factors? Start with a factorable target and the + cited constant-chart two-factor divisibility criterion. The reachability + theorem does not determine its exact finite minimum. + +TASK.json records the relevance, first step and blocker for each question. diff --git a/research/veronese-singular-obstruction/SOURCES.json b/research/veronese-singular-obstruction/SOURCES.json new file mode 100644 index 0000000000..29b43804bb --- /dev/null +++ b/research/veronese-singular-obstruction/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/right-vector-commutative-products/README.md", + "usage": "provenance", + "git_blob": "fc9889d41621b596209c707b6057517744b4642f", + "sha256": "6222431360182204f502334d1c707eefc39a174d06578ef75c52f37b5873055f" + }, + { + "path": "research/singular-polynomial-cost/PROOF.md", + "usage": "provenance", + "git_blob": "90536da515be841a4bc60d44c675860b21418068", + "sha256": "ccd4dc2413ff16c452f18f1f8a4a534252073765f7f6760f9e9637aa8450bed1" + }, + { + "path": "research/singular-polynomial-cost/README.md", + "usage": "provenance", + "git_blob": "59c5769281b6ffb78a5bdddd21ed5e8c9290342d", + "sha256": "79164b1f996b0916175bade051a42cfdab2dd6a50d8e39b9aae852e644b75150" + } + ] +} diff --git a/research/veronese-singular-obstruction/TASK.json b/research/veronese-singular-obstruction/TASK.json new file mode 100644 index 0000000000..5e04c7dec9 --- /dev/null +++ b/research/veronese-singular-obstruction/TASK.json @@ -0,0 +1,124 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "All-length singular two-role reachability over commutative K-domains is equivalent to an R-valued outer-product factorization; the explicit Veronese target is unreachable over every field.", + "scope_change_reason": "The formal-interface card is changed to an original algebraic side result answering the explicit nonprincipal-domain question in PR4808 and the singular-endpoint gap in ToikY PR4334. This is a written proof, not a predecessor audit or proof-assistant/caller binding.", + "bottleneck_link": "A determinant-zero endpoint need not be implementable even by an arbitrarily long word in the constant-right-vector alphabet. This separates formal target feasibility from a favorable recursive price. No selected supplier or complete budget is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved new implication and explicit target obstruction. Do not extend to more roles, further rings or physical construction.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py; exact singular-factor and wrapped-word checks over F2,F3, complete degree-bounded factor searches over F2,F3,F5, symbolic controls over Z and four prime fields.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one extra restored role realize the obstructed Veronese target?", + "why_it_matters": "The proof uses a rank-one singular factor only in two roles; stabilization may change reachability.", + "first_step": "Study diag(M,1) with the same constant-right-vector alphabet, retaining the third input and output exactly.", + "blocked_by": "No three-role factorization obstruction or attaining word is supplied." + }, + { + "question": "For reachable singular targets over a general commutative K-domain, which require one, two or three paid factors?", + "why_it_matters": "Reachability is settled here, but exact finite tariffs beyond the K[t] predecessor remain open.", + "first_step": "Apply the cited constant-chart two-factor divisibility criterion to one specified non-PID domain and factorable target.", + "blocked_by": "The present theorem establishes only a three-factor upper bound and no new exact minimum." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214451", + "environment": { + "interpreter": "CPython 3.12.15", + "interpreter_path": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "platform": "macOS arm64", + "dependencies": "Python standard library only" + }, + "prior_state": { + "branch": null, + "state": "detached HEAD", + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "preserved": true + }, + "overlap": { + "canonical_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at": "2026-10-27T10:04:00Z", + "open_pr_records": 416, + "discussion_records": 5312, + "remote_pagination_complete": true, + "local_notes": "sparse and incomplete; main README and merged-PR searches performed separately", + "limits": "No claim about unpublished work, arbitrary historical diffs or global literature priority." + } +} diff --git a/research/veronese-singular-obstruction/VERIFY.json b/research/veronese-singular-obstruction/VERIFY.json new file mode 100644 index 0000000000..30d7a0f28a --- /dev/null +++ b/research/veronese-singular-obstruction/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": 120, + "checks": "Exact new singular-factor extraction and full wrapped endpoints; complete Veronese factor searches; symbolic larger-ring, determinant and omission controls; source-bound generated receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete finite coverage with explicit checks retained under optimization." + } + ] +} diff --git a/research/veronese-singular-obstruction/verify.py b/research/veronese-singular-obstruction/verify.py new file mode 100644 index 0000000000..f8ec9e8e20 --- /dev/null +++ b/research/veronese-singular-obstruction/verify.py @@ -0,0 +1,249 @@ +"""Exact corroboration of the two-role domain obstruction. Standard library only.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +DEGREE_LIMIT = 8 +TERM_LIMIT = 45 +Poly = tuple[tuple[int, int, int], ...] +Matrix = tuple[Poly, Poly, Poly, Poly] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def polynomial(terms: dict[tuple[int, int], int], p: int) -> Poly: + require(p in (0, 2, 3, 5, 7), "unsupported coefficient domain") + require(len(terms) <= TERM_LIMIT, "polynomial capacity exceeded") + result = [] + for (i, j), value in sorted(terms.items()): + require(i >= 0 and j >= 0 and i + j <= DEGREE_LIMIT, "degree limit") + value = value % p if p else value + if value: + result.append((i, j, value)) + return tuple(result) + + +def constant(value: int, p: int) -> Poly: + return polynomial({(0, 0): value}, p) + + +def add(a: Poly, b: Poly, p: int) -> Poly: + terms = {(i, j): value for i, j, value in a} + for i, j, value in b: + terms[i, j] = terms.get((i, j), 0) + value + return polynomial(terms, p) + + +def scale(a: Poly, value: int, p: int) -> Poly: + return polynomial({(i, j): value * c for i, j, c in a}, p) + + +def multiply(a: Poly, b: Poly, p: int) -> Poly: + terms: dict[tuple[int, int], int] = {} + for i, j, c in a: + for k, ell, d in b: + key = i + k, j + ell + terms[key] = terms.get(key, 0) + c * d + return polynomial(terms, p) + + +def identity(p: int) -> Matrix: + one, zero = constant(1, p), constant(0, p) + return one, zero, zero, one + + +def matmul(a: Matrix, b: Matrix, p: int) -> Matrix: + entries = [] + for i, j in itertools.product(range(2), repeat=2): + entries.append(add(multiply(a[2 * i], b[j], p), + multiply(a[2 * i + 1], b[2 + j], p), p)) + return tuple(entries) + + +def outer(a: tuple[Poly, Poly], b: tuple[Poly, Poly], p: int) -> Matrix: + return tuple(multiply(x, y, p) for x in a for y in b) + + +def determinant(a: Matrix, p: int) -> Poly: + return add(multiply(a[0], a[3], p), scale(multiply(a[1], a[2], p), -1, p), p) + + +def paid(u: tuple[Poly, Poly], v: tuple[int, int], p: int) -> Matrix: + unit = identity(p) + return tuple(add(unit[2 * i + j], scale(u[i], v[j], p), p) + for i, j in itertools.product(range(2), repeat=2)) + + +def even_quadratics(p: int) -> tuple[Poly, ...]: + require(p in (2, 3, 5), "finite search requires a declared prime") + monomials = ((0, 0), (2, 0), (1, 1), (0, 2)) + return tuple(polynomial(dict(zip(monomials, values)), p) + for values in itertools.product(range(p), repeat=4)) + + +def factor_singular(n: Matrix, v: tuple[int, int], p: int): + require(v != (0, 0) and not determinant(n, p), "singular factor premise") + if v[0]: + a = constant(-v[1] * pow(v[0], -1, p), p), constant(1, p) + b = n[2], n[3] + else: + a = constant(1, p), constant(0, p) + b = n[0], n[1] + require(outer(a, b, p) == n, "singular factor extraction") + return a, b + + +def check_singular_factors(p: int) -> dict[str, int]: + values = even_quadratics(p) + count = tested = 0 + s2, st, t2 = (polynomial({m: 1}, p) for m in ((2, 0), (1, 1), (0, 2))) + prefix = paid((s2, st), (0, 1), p) + suffix = paid((t2, s2), (1, 0), p) + free = (constant(0, p), constant(1, p), constant(-1, p), constant(1, p)) + for v in itertools.product(range(p), repeat=2): + if v == (0, 0): + continue + for u in itertools.product(values, repeat=2): + tested += 1 + n = paid(u, v, p) + if determinant(n, p): + continue + a, b = factor_singular(n, v, p) + left = matmul(free, suffix, p) + right = matmul(prefix, free, p) + endpoint = matmul(matmul(left, n, p), right, p) + aa = tuple(add(multiply(left[2 * i], a[0], p), + multiply(left[2 * i + 1], a[1], p), p) for i in range(2)) + bb = tuple(add(multiply(b[0], right[j], p), + multiply(b[1], right[2 + j], p), p) for j in range(2)) + require(endpoint == outer(aa, bb, p), "full wrapped endpoint") + count += 1 + require(count == (p * p - 1) * len(values), "complete singular-factor count") + return {"p": p, "tested_parameter_choices": tested, + "singular_parameter_choices": count, "wrapped_words": count} + + +def check_veronese(p: int) -> dict[str, int]: + values = even_quadratics(p) + s2, st, t2 = (polynomial({m: 1}, p) for m in ((2, 0), (1, 1), (0, 2))) + target = s2, st, st, t2 + require(not determinant(target, p), "target determinant") + first_pairs = completions = 0 + for a1, b1 in itertools.product(values, repeat=2): + if multiply(a1, b1, p) != s2: + continue + first_pairs += 1 + a2s = tuple(x for x in values if multiply(x, b1, p) == st) + b2s = tuple(x for x in values if multiply(a1, x, p) == st) + for a2, b2 in itertools.product(a2s, b2s): + if multiply(a2, b2, p) == t2: + completions += 1 + require(first_pairs == 2 * (p - 1), "complete first-entry divisor pairs") + require(completions == 0, "unexpected Veronese factorization") + return {"p": p, "first_entry_pairs_tested": len(values) ** 2, + "first_entry_solutions": first_pairs, "factorizations": completions} + + +def three_factors(a: tuple[Poly, Poly], b: tuple[Poly, Poly], p: int): + one, zero = constant(1, p), constant(0, p) + factors = ((a[0], zero, a[1], one), (one, b[1], zero, zero), + (b[0], zero, zero, one)) + us = ((add(a[0], scale(one, -1, p), p), a[1]), + (b[1], scale(one, -1, p)), + (add(b[0], scale(one, -1, p), p), zero)) + vs = ((1, 0), (0, 1), (1, 0)) + for n, u, v in zip(factors, us, vs): + require(n == paid(u, v, p), "constructor factor legality") + endpoint = matmul(matmul(factors[0], factors[1], p), factors[2], p) + require(endpoint == outer(a, b, p), "outer-product word endpoint") + return factors + + +def check_controls() -> dict[str, int]: + constructors = deletions = specializations = 0 + larger_rings = determinant_mutations = 0 + for p in (0, 2, 3, 5, 7): + one = constant(1, p) + s, t = polynomial({(1, 0): 1}, p), polynomial({(0, 1): 1}, p) + s2, st, t2 = multiply(s, s, p), multiply(s, t, p), multiply(t, t, p) + a, b = (add(one, s2, p), st), (t2, add(one, st, p)) + factors = three_factors(a, b, p) + constructors += 1 + for index in range(3): + altered = list(factors) + altered[index] = identity(p) + require(matmul(matmul(altered[0], altered[1], p), altered[2], p) + != outer(a, b, p), "omitted paid factor went undetected") + deletions += 1 + three_factors((s, t), (s, t), p) + require(outer((s, t), (s, t), p) == (s2, st, st, t2), "larger-ring control") + require(any((i + j) % 2 for i, j, c in s + t), "ring restriction control") + constructors += 1 + larger_rings += 1 + require(determinant((s2, st, st, add(t2, one, p)), p) == s2, + "determinant mutation control") + determinant_mutations += 1 + for p in (2, 3, 5, 7): + for s, t, x, y in itertools.product(range(p), repeat=4): + actual = ((s * s * x + s * t * y) % p, + (s * t * x + t * t * y) % p) + source = (s * x + t * y) % p + require(actual == (s * source % p, t * source % p), "scalar action") + specializations += 1 + invalid = 0 + for terms, p in (({(9, 0): 1}, 2), ({(-1, 0): 1}, 3), ({(0, 0): 1}, 4)): + try: + polynomial(terms, p) + except ValueError: + invalid += 1 + require(invalid == 3, "invalid polynomial accepted") + return {"constructor_words": constructors, "omission_controls": deletions, + "scalar_input_cases": specializations, "invalid_inputs": invalid, + "larger_ring_controls": larger_rings, + "determinant_mutations": determinant_mutations} + + +def check_bounds() -> dict[str, int]: + maximum = {(i, j): 1 for i in range(9) for j in range(9 - i)} + require(len(polynomial(maximum, 2)) == TERM_LIMIT, "capacity boundary") + failures = 0 + try: + polynomial({(i, 0): 1 for i in range(46)}, 2) + except ValueError: + failures += 1 + try: + factor_singular(identity(2), (1, 0), 2) + except ValueError: + failures += 1 + require(failures == 2, "capacity or singular-premise guard missing") + return {"accepted_capacity_boundaries": 1, "rejected_premises": failures} + + +def main() -> None: + result = { + "singular_factors": [check_singular_factors(p) for p in (2, 3)], + "veronese_searches": [check_veronese(p) for p in (2, 3, 5)], + "controls": check_controls(), + "bound_controls": check_bounds(), + "claim_type": "scoped written proof with finite corroboration", + "all_field_obstruction": "written polynomial-divisibility proof, not finite evaluation", + } + package = Path(__file__).resolve().parent + hashes = {} + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + with (package / name).open("rb") as stream: + payload = stream.read(128 * 1024 + 1) + require(len(payload) <= 128 * 1024, "source receipt capacity") + hashes[name] = hashlib.sha256(payload).hexdigest() + print(json.dumps({"results": result, "source_sha256": hashes}, sort_keys=True)) + print("PASS_VERONESE_SINGULAR_OBSTRUCTION no_new_kappa") + + +if __name__ == "__main__": + main()