From a4436fab4164eccc498d4d9885eec68211c869de Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:53:00 +0100 Subject: [PATCH] feat(research): prove the singular product factor threshold --- research/singular-product-threshold/PROOF.md | 155 +++++++++++ research/singular-product-threshold/README.md | 152 +++++++++++ .../singular-product-threshold/SOURCES.json | 36 +++ research/singular-product-threshold/TASK.json | 122 +++++++++ .../singular-product-threshold/VERIFY.json | 32 +++ research/singular-product-threshold/verify.py | 248 ++++++++++++++++++ 6 files changed, 745 insertions(+) create mode 100644 research/singular-product-threshold/PROOF.md create mode 100644 research/singular-product-threshold/README.md create mode 100644 research/singular-product-threshold/SOURCES.json create mode 100644 research/singular-product-threshold/TASK.json create mode 100644 research/singular-product-threshold/VERIFY.json create mode 100644 research/singular-product-threshold/verify.py diff --git a/research/singular-product-threshold/PROOF.md b/research/singular-product-threshold/PROOF.md new file mode 100644 index 0000000000..a36f102ede --- /dev/null +++ b/research/singular-product-threshold/PROOF.md @@ -0,0 +1,155 @@ +# Singular rank-one product threshold + +Let K be a field and R=K^k for a positive finite k. Scalars embed diagonally +in R. Use two roles. Paid factors are I+u y^T, where u belongs to R^2 and y +belongs to K^2. Common GL_2(K) maps are free anywhere. A target is an ordered +tuple M=(M_1,...,M_k) of 2-by-2 matrices over K. All M_i in the main theorem +have rank exactly one. Cost means the least number of paid factors. + +## Cited criterion and the changed target contract + +Nick Petalas's #4276, Theorem B, states that cost(M)<=2 exactly when common +G,H in GL_2(K) make N=GMH satisfy N12 in the right ideal N11 R. This criterion +allows singular targets. We cite it as a predecessor theorem, rather than +claiming or auditing it. Free maps can be collected at one endpoint by +#4243's normal form, following Wentao Li's #4099/#2513 alphabet. + +For R=K^k, right-ideal membership is componentwise. Write t for the first +column of H and phi for the first row of G. The other column of H completes +t to a basis. In component i the ideal condition is equivalent to + +```text +phi M_i t != 0, or phi M_i = 0. +``` + +Indeed a nonzero pivot generates the entire field. A zero pivot requires +the other entry of the row to be zero, which means the entire row is zero. +Conversely every nonzero t and phi extend to suitable H and G. Thus the +displayed condition must hold for every i with the SAME t and phi. + +ToikY's #4334 studies invertible components, for which a zero row is +impossible, and proves the sharp threshold q+1. The present theorem changes +every component to a nonzero rank-one matrix. The zero-row alternative is +essential, so applying the invertible common-unit-pivot test would be wrong. +Nick Petalas's #4601 leaves singular local-product targets open. + +## Theorem 1: exact kernel/image criterion + +For each line T in K^2, let S_T be the span of the image lines im(M_i) for +those i with ker(M_i)=T. The span of an empty collection is zero. Then + +```text +cost(M)<=2 iff some T has dim(S_T)<=1. +``` + +Proof. Fix a nonzero t spanning T. If t is not in ker(M_i), then M_i t is a +nonzero vector spanning im(M_i). Every phi either evaluates nontrivially on +this vector or kills the entire image. Both satisfy the cited criterion. +If ker(M_i)=T, then M_i t=0. The criterion requires phi to kill im(M_i). +Therefore a common nonzero phi exists exactly when it kills S_T, which is +equivalent to dim(S_T)<=1 in a two-dimensional space. Taking all T proves +both directions. + +## Lemma 2: three factors suffice + +In fact every target in M_2(K^k), without any rank assumption, has cost at +most three. It is enough to factor each component with the common ordered +right vectors e1,e2,e1. Left-vector entries can vary by component, so the +following per-component choices assemble into three paid R-valued factors. + +For M_i=[[a,b],[c,d]] with b=0 use + +```text +[[a,0],[c,1]] [[1,0],[0,d]] I = M_i. +``` + +For b!=0 put l=(d-1)/b, f=c-l*a, and e=a-b*f. Then use + +```text +F1=[[1,0],[l,1]], F2=[[1,b],[0,1]], F3=[[e,0],[f,1]]. +F1 F2 F3 = [[e+b*f,b],[l*(e+b*f)+f,l*b+1]] = M_i. +``` + +Every displayed factor is I+u e_j^T for its stated right vector. The +identity may use e1 and a zero left vector. These are algebraic product +orders, so column-vector execution applies F3 first. No free endpoint is +needed. The construction extends the invertible-only upper-word scope in +#4334 to this pure-field product domain. It does not apply to general local +algebras, where a nonzero b may fail to be invertible. + +## Theorem 3: sharp finite-field threshold + +Let K=F_q. Among tuples with all component matrices nonzero and rank one, + +```text +k < 2(q+1): every target has cost <=2; +k >= 2(q+1): some target has exact cost 3; +every target has cost <=3. +``` + +Proof. There are q+1 possible kernel lines. If cost(M)>2, Theorem 1 says +that every S_T has dimension two. Each such span needs at least two +component matrices with kernel T and distinct image lines. A component has +only one kernel, so k>=2(q+1). + +For sharpness, for each T choose a nonzero row r_T with kernel T. Include +both e1*r_T and e2*r_T as component matrices. They have rank one, share +kernel T and have different image lines. Now every S_T=K^2. Theorem 1 +excludes two factors, while Lemma 2 gives three. For larger k repeat any +component. Repetition preserves the obstruction and the three-factor word. +This proves all assertions. + +Over an infinite K, a finite tuple omits some possible kernel line T. +Then S_T=0, and every such rank-one tuple costs at most two. This is a +direct case of Theorem 1, not a finite-field enumeration claim. + +## Binary finite certificate + +Over F2 there are nine nonzero rank-one matrices. Literal zero-, one- and +two-factor images are enumerated with all common free endpoints and all +right-vector lines. Allowing arbitrary left vectors includes singular paid +factors. Projective representatives suffice because a nonzero rescaling of +y can be absorbed in u. A free map anywhere can be collected at the right +endpoint by the cited normal form. + +For fixed common right-vector lines and endpoint, every component may +choose its left vectors independently. Thus a tuple belongs to this chart +exactly when every component belongs to its local image. Membership depends +only on its support among the nine matrices. Comparing all 2^9 support +sets with Theorem 1 is an exhaustive comparison for tuples of ANY length +over this binary rank-one alphabet, without enumerating infinitely many +tuples. There are 64 support sets outside the two-factor image, with minimum +size six. A finite recurrence enumerates ordered-tuple multiplicities, +starting with the empty support and adding one of nine entries at each +step. It covers every tuple through length six exactly once. + +At length six the resulting exact cost histogram is + +```text +cost 0: 0; cost 1: 567; cost 2: 511434; cost 3: 19440. +total: 531441 = 9^6. +``` + +The 19,440 count also follows from the threshold criterion. Assign the six +ordered positions in pairs to the three kernel lines, in 6!/(2!)^3=90 ways. +For each kernel the ordered pair has 3*2=6 different image-line choices, +and over F2 each kernel/image pair specifies one matrix. Thus the count is +90*6^3=19440. The verifier checks the literal chart census independently of +this arithmetic count. + +## Scope and credit + +The quantified result is a scoped algebraic proof, with a separate finite +certificate over the stated binary domain and finite word checks over five +fields. It is not a complete multiplication theorem. Native preparation, +access, routing, restoration, precision, stock and complete supplier costs +are unknown. Local radical lifts, matrix-algebra blocks, mixed-rank lower +thresholds and more than two roles are outside scope. No supplier admission +or new kappa is claimed. Independent human and formal proof-kernel review +are unclaimed. + +This package was produced by Nick Petalas. The exact low-factor criterion +and common-free normal form are credited above to Nick Petalas, the +invertible-product predecessor and open gap to ToikY, and the alphabet and +column bound to Wentao Li following #2513. Projective-line counting and +elementary matrix multiplication are classical. Apache-2.0. diff --git a/research/singular-product-threshold/README.md b/research/singular-product-threshold/README.md new file mode 100644 index 0000000000..8cff080ab4 --- /dev/null +++ b/research/singular-product-threshold/README.md @@ -0,0 +1,152 @@ +# Sharp threshold for singular right-vector products + +Scoped algebraic proof with a finite certificate. No new kappa. + +Let K=F_q and R=K^k. Use two roles, paid factors I+u y^T with u in R^2 +and y in K^2, and common GL_2(K) maps free anywhere. Suppose every component +of a target M=(M_1,...,M_k) is a nonzero rank-one matrix. Then + +```text +k < 2(q+1): every target costs at most two paid factors. +k >= 2(q+1): some target costs exactly three. +Every target costs at most three. +``` + +This answers a singular-target part of the open direction in ToikY's #4334 +and Nick Petalas's #4601. Their invertible-component threshold is q+1. +The changed singular contract permits a zero pivot when the entire row +vanishes, so the invertible common-unit-pivot test does not apply. + +The new exact criterion is particularly simple. For each input line T, +collect the image lines of components having kernel T. Two paid factors +suffice exactly when at least one T has at most one distinct collected +image line. An obstruction therefore needs two different image lines for +EVERY kernel line. An explicit family with two components per kernel +attains the threshold. Over an infinite field every finite such tuple +costs at most two. The [proof](PROOF.md) cites #4276's low-factor criterion +and supplies a common-right-vector e1,e2,e1 word for the three-factor bound. +No predecessor code or verifier is imported or replayed. + +## Exact finite evidence + +The standalone standard-library verifier constructs literal binary one- and +two-factor images with every paid left vector, common right-vector line and +common free endpoint. It includes singular paid factors. The complete +rank-one alphabet has nine matrices, so all 512 support sets suffice to +compare literal membership with the new criterion for tuples of any length. +There are 64 obstructed supports, all with at least six distinct matrices. +A finite support recurrence counts ordered tuples through six components. +It is an exact multiplicity enumeration, not a raw scan of every tuple. + +```text +components tuples cost 1 cost 2 cost 3 +1 9 9 0 0 +2 81 27 54 0 +3 729 63 666 0 +4 6561 135 6426 0 +5 59049 279 58770 0 +6 531441 567 511434 19440 +``` + +All these targets have cost greater than zero because every component is +singular. The six-component count 19,440 is also derived directly in the +proof. The code checks that count against the literal-chart enumeration. + +Over F2,F3,F4,F5,F7 the verifier checks the three-factor word on every +2-by-2 matrix, including singular and zero matrices. This covers 3,379 +matrices and 138,163 arbitrary-input evaluations. F4 is implemented as +F2[t]/(t^2+t+1). It also checks the sharp threshold witnesses at component +counts 6,8,10,12,16 and all 52 single-component deletions. Field-table +associativity, distributivity and inverses are checked before using them. + +Controls discriminate separate component charts, repeated equal image +lines, reversing the word, omitting its final factor, odd-field sign errors +and using the composite modulus six as a field. The deletion controls show +that every component of the explicit threshold witness matters. Checks use +explicit exceptions and remain active under Python optimization. + +Every run emits a generated JSON receipt binding all six package files by +SHA256, followed only by stdout data. No receipt is hand-written or saved +in the checkout. + +## Reproduction + +From the repository root, using the Python 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/singular-product-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/singular-product-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/singular-product-threshold +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/singular-product-threshold --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter above. +Expected verifier marker is +`PASS_SINGULAR_PRODUCT_THRESHOLD binary_cost3=19440 threshold=6 no_new_kappa`. +Both normal and optimized checks are registered with 120-second limits. +SOURCES.json binds the predecessor statements and task catalogue as historical +provenance at base 624de9dc66858af0945e5f8a0942488d62280d43. There are no live +external inputs and no dependence on an unmerged Git object. + +The original formal-interface-lemma card is explicitly changed to this +algebraic side question in TASK.json. Its historical first command, +`scripts/research_baseline.py`, fails with `KeyError: 'bit_lower'` on the +changed selected schema. After materializing the selected source closure, +`scripts/research_selected_baseline.py` passes with selected 60403/20000000. +That orientation check authenticates metadata only. No shared helper is changed. + +## Limits and verification design + +The universal claim is the written scoped proof. The exhaustive support +certificate is binary; other fields have the finite word and sharp-witness +checks stated above. Local radical lifts, non-field factors, mixed-rank +thresholds and more than two roles remain outside the main theorem. The +three-factor construction alone covers arbitrary matrices over K^k. + +Native coefficient preparation, access, routing, control, restoration, +precision, stock and complete supplier costs are unknown. No supplier, +selected frontier or complete multiplication theorem changes. Independent +human and formal proof-kernel review are unclaimed. No Lean, Docker or +selected operator replay is needed for or included in this isolated package. + +The code has no recursion, child process, network access, solver or CLI input. +The field orders are restricted to five fixed cases with q<=7. Field-table +loops use at most 7^3 triples; matrix loops use at most 7^4 targets; vector +loops use at most 7^2 inputs. Binary image construction uses 3*6*3*4^2=864 +two-factor cases. Each support table and recurrence dictionary has at most +512 entries; there are exactly six recurrence rounds. The sharp families +have at most 16 components. Receipt reads are limited to six fixed files +of at most 1 MiB each. The program writes only to stdout. + +Power of Ten rule 3 has a managed-runtime deviation. Python allocates +integers, tuples and finite sets during enumeration. The explicit fixed +domains bound live state to the 512-entry support/counter tables, tiny field +and literal-image tables, and one matrix/word at a time. A fixed-buffer +implementation would be the follow-up if the domains expand. Functions +remain below the 60-line review ceiling. Warning-strict normal and optimized +runs are registered in CI; no separate type checker or linter is required. + +## Open next questions + +1. What replaces the kernel/image criterion for rank-one residue targets + over products of local algebras? Start with two specified dual-number + components and enumerate their right-ideal constraints. Nilpotent + off-pivot entries can invalidate a zero residue pivot, so the field + threshold does not settle that question. +2. Can one literal native producer/consumer realize the common-right-vector + alphabet at a favorable complete cost? First specify its coefficients, + access, restoration and precision contracts and full bill. Those physical + obligations are unknown; the formal word supplies none of them. + +TASK.json records why each question matters and its first bounded step. + +## Credit + +This package was produced by Nick Petalas. ToikY's #4334 supplies the +invertible field-product predecessor and its singular-target gap. Nick +Petalas's #4601 supplies the local-product follow-up, #4276 supplies the +exact low-factor criterion, and #4243 supplies the common-free normal form. +Wentao Li's #4099 supplies the alphabet and column bound, building on #2513. +Projective-line counting and elementary matrix algebra are classical. +The new contribution is the singular kernel/image criterion, its sharp +threshold and the stated finite certificate. Apache-2.0. diff --git a/research/singular-product-threshold/SOURCES.json b/research/singular-product-threshold/SOURCES.json new file mode 100644 index 0000000000..7327608425 --- /dev/null +++ b/research/singular-product-threshold/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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-two-factor-criterion/PROOF.md", + "usage": "provenance", + "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c", + "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895" + }, + { + "path": "research/right-vector-commutative-products/README.md", + "usage": "provenance", + "git_blob": "fc9889d41621b596209c707b6057517744b4642f", + "sha256": "6222431360182204f502334d1c707eefc39a174d06578ef75c52f37b5873055f" + }, + { + "path": "research/right-vector-local-products/README.md", + "usage": "provenance", + "git_blob": "e7886eba302aecd0f0111e76d9908ce8809f3262", + "sha256": "815089fc8c4ac15cffc20b3b529e232840bf675627e8a91cc01590e0f593b65f" + } + ] +} diff --git a/research/singular-product-threshold/TASK.json b/research/singular-product-threshold/TASK.json new file mode 100644 index 0000000000..035cfb0205 --- /dev/null +++ b/research/singular-product-threshold/TASK.json @@ -0,0 +1,122 @@ +{ + "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": "Sharp all-field component threshold and exact two-factor criterion for tuples of nonzero rank-one targets over K^k in the two-role right-vector alphabet.", + "scope_change_reason": "This is a scoped algebraic side result answering the singular-target gap in #4334/#4601, rather than a selected-caller formalization or audit.", + "bottleneck_link": "The result identifies exactly when singular product targets need a third formal paid call. Native preparation, access, restoration, precision and complete supplier cost remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified sharp threshold; do not extend to local radical lifts or mixed-rank components.", + "outcome": "completed", + "evidence": "PROOF.md proves the threshold 2(q+1). verify.py compares literal two-factor charts with all 512 binary support sets, enumerates exact tuple multiplicities through six components, and evaluates explicit words over five fields.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What replaces the kernel/image-line criterion for rank-one residue targets over products of local algebras?", + "why_it_matters": "Nilpotent off-pivot entries can make a zero residue pivot fail right-ideal containment, so the pure-field threshold need not persist.", + "first_step": "Specify two dual-number components with a fixed rank-one residue and enumerate the new right-ideal constraints.", + "blocked_by": "The proof uses a field zero pivot being the only nonunit and does not price or classify radical lifts." + }, + { + "question": "Can a literal native producer/consumer realize the common-right-vector alphabet at a favorable complete cost?", + "why_it_matters": "Formal factor savings do not by themselves improve a recursive supplier.", + "first_step": "Specify one source, target, coefficient-access, restoration and precision contract and its full bill.", + "blocked_by": "Native preparation, routing, restoration, precision and stock costs are unknown." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131551", + "orientation": { + "current_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY after materializing the selected source closure", + "card_first_step": "scripts/research_baseline.py fails with KeyError: bit_lower on the selected productive-helper schema, as current-priorities.md already documents. No shared helper is changed." + }, + "overlap_coverage": { + "open_pr_records": 299, + "open_pr_snapshot": "2026-10-22T19:45:13.565143+00:00", + "discussion_records": 3712, + "discussion_snapshot": "2026-10-22T19:46:08.245656+00:00", + "complete_remote_pagination": true, + "local_notes_complete": false, + "additional_checks": "Live recent claims, account PRs, distinctive main README terms and merged/all-state searches. #4334/#4601/#4770 source bodies read. This is not a novelty certificate.", + "precommit_refresh": "Recent claims and this account's open PR bodies were rechecked; open #4776 concerns a different zero-residue radical-pencil domain. Other same-alphabet claims concern nonlocal polynomial costs, higher-role invertible targets, proper extension residues, and matrix-algebra rank-two targets. No same-question result was found; historical coverage remains incomplete." + }, + "upstream_refresh": { + "commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "checked_at": "2026-10-22T19:52:09.585374+00:00", + "guidance_changed": false, + "predecessor_inputs_changed": false + } +} diff --git a/research/singular-product-threshold/VERIFY.json b/research/singular-product-threshold/VERIFY.json new file mode 100644 index 0000000000..43ac3649bf --- /dev/null +++ b/research/singular-product-threshold/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 binary zero/one/two-factor images, all 512 rank-one support sets and exact tuple counts through six components; all-field sharp witnesses and three-factor words over F2,F3,F4,F5,F7, with semantic controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal binary zero/one/two-factor images, all 512 rank-one support sets and exact tuple counts through six components; all-field sharp witnesses and three-factor words over F2,F3,F4,F5,F7, with semantic controls." + } + ] +} diff --git a/research/singular-product-threshold/verify.py b/research/singular-product-threshold/verify.py new file mode 100644 index 0000000000..ebde25db3f --- /dev/null +++ b/research/singular-product-threshold/verify.py @@ -0,0 +1,248 @@ +#!/usr/bin/env python3 +"""Exact singular-product checks. Produced by Nick Petalas. Apache-2.0.""" + +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Field: + def __init__(self, q): + require(q in (2, 3, 4, 5, 7), "unsupported field order") + self.q = q + self.add = tuple(tuple(a ^ b if q == 4 else (a + b) % q + for b in range(q)) for a in range(q)) + self.mul = tuple(tuple(self.polynomial(a, b) if q == 4 else a * b % q + for b in range(q)) for a in range(q)) + self.neg = tuple(next(b for b in range(q) if self.add[a][b] == 0) + for a in range(q)) + self.inv = (0,) + tuple(next(b for b in range(1, q) + if self.mul[a][b] == 1) + for a in range(1, q)) + self.lines = ((0, 1),) + tuple((1, a) for a in range(q)) + self.vectors = tuple(product(range(q), repeat=2)) + + @staticmethod + def polynomial(a, b): + value = 0 + for bit in range(2): + if b >> bit & 1: + value ^= a << bit + if value & 4: + value ^= 7 + return value + + def sub(self, a, b): + return self.add[a][self.neg[b]] + + def dot(self, u, v): + return self.add[self.mul[u[0]][v[0]]][self.mul[u[1]][v[1]]] + + def act(self, a, v): + return self.dot(a[:2], v), self.dot(a[2:], v) + + def mm(self, a, b): + return tuple(self.dot(a[2*i:2*i+2], (b[j], b[2+j])) + for i in range(2) for j in range(2)) + + def det(self, a): + return self.sub(self.mul[a[0]][a[3]], self.mul[a[1]][a[2]]) + + def paid(self, u, y): + identity = (1, 0, 0, 1) + return tuple(self.add[identity[2*i+j]][self.mul[u[i]][y[j]]] + for i in range(2) for j in range(2)) + + def line(self, v): + require(v != (0, 0), "zero has no projective line") + return (1, self.mul[v[1]][self.inv[v[0]]]) if v[0] else (0, 1) + + +def upper_word(f, matrix, wrong_sign=False): + a, b, c, d = matrix + if b == 0: + return (a, 0, c, 1), (1, 0, 0, d), (1, 0, 0, 1) + lower = f.mul[f.sub(d, 1)][f.inv[b]] + correction = f.mul[lower][a] + bottom = f.add[c][correction] if wrong_sign else f.sub(c, correction) + first = f.sub(a, f.mul[b][bottom]) + return (1, 0, lower, 1), (1, b, 0, 1), (first, 0, bottom, 1) + + +def full_pivot(f, matrices): + """Raw product-of-fields ideal test, without kernel/image grouping.""" + for t, phi in product(f.lines, repeat=2): + valid = True + for matrix in matrices: + row = (f.dot(phi, (matrix[0], matrix[2])), + f.dot(phi, (matrix[1], matrix[3]))) + if f.dot(row, t) == 0 and row != (0, 0): + valid = False + break + if valid: + return t, phi + return None + + +def grouped_pivot(f, matrices): + """The new kernel/image criterion, using distinct image lines.""" + for t in f.lines: + images = set() + for matrix in matrices: + if f.act(matrix, t) == (0, 0): + column = (matrix[0], matrix[2]) + if column == (0, 0): + column = (matrix[1], matrix[3]) + images.add(f.line(column)) + if len(images) <= 1: + return True + return False + + +def binary_literal_images(f, rankones): + matrices = tuple(product(range(2), repeat=4)) + free = tuple(a for a in matrices if f.det(a)) + require(all(a not in free for a in rankones), "zero-paid image excludes singular targets") + one_masks, two_masks = set(), set() + for y, scalar in product(f.lines, free): + image = {f.mm(f.paid(u, y), scalar) for u in f.vectors} + one_masks.add(sum(1 << i for i, a in enumerate(rankones) if a in image)) + for z in f.lines: + image = {f.mm(f.mm(f.paid(u, y), f.paid(v, z)), scalar) + for u, v in product(f.vectors, repeat=2)} + two_masks.add(sum(1 << i for i, a in enumerate(rankones) if a in image)) + return one_masks, two_masks + + +def binary_census(): + f = Field(2) + rankones = tuple(a for a in product(range(2), repeat=4) + if a != (0, 0, 0, 0) and f.det(a) == 0) + require(len(rankones) == 9, "binary rank-one coverage") + one_masks, two_masks = binary_literal_images(f, rankones) + costs = [] + for mask in range(1 << len(rankones)): + selected = tuple(a for i, a in enumerate(rankones) if mask >> i & 1) + literal = any(mask & image == mask for image in two_masks) + require(literal == grouped_pivot(f, selected), "literal/grouped mismatch") + require(literal == (full_pivot(f, selected) is not None), "raw mismatch") + one = any(mask & image == mask for image in one_masks) + costs.append(1 if one else 2 if literal else 3) + counts = {0: 1} + rows = [] + for k in range(1, 7): + next_counts = Counter() + for mask, multiplicity in counts.items(): + for i in range(len(rankones)): + next_counts[mask | 1 << i] += multiplicity + counts = next_counts + histogram = [0, 0, 0, 0] + for mask, multiplicity in counts.items(): + histogram[costs[mask]] += multiplicity + require(sum(histogram) == 9 ** k, "tuple multiplicity coverage") + require(histogram[3] == (19440 if k == 6 else 0), "threshold census") + rows.append({"components": k, "targets": 9 ** k, "costs": histogram}) + require(rows[-1]["costs"] == [0, 567, 511434, 19440], "six-component census") + bad = [mask for mask, cost in enumerate(costs) if cost == 3] + require(len(bad) == 64 and min(m.bit_count() for m in bad) == 6, + "obstructed support coverage") + return rows, {"support_sets": 512, "bad_supports": 64, + "one_chart_masks": len(one_masks), "two_chart_masks": len(two_masks)} + + +def field_check(f): + for a, b, c in product(range(f.q), repeat=3): + require(f.add[f.add[a][b]][c] == f.add[a][f.add[b][c]], "add associativity") + require(f.mul[f.mul[a][b]][c] == f.mul[a][f.mul[b][c]], "mul associativity") + require(f.mul[a][f.add[b][c]] == f.add[f.mul[a][b]][f.mul[a][c]], + "distributivity") + for a in range(1, f.q): + require(f.mul[a][f.inv[a]] == 1, "field inverse") + target_count, input_count, reversals, omissions, sign_errors = 0, 0, 0, 0, 0 + for matrix in product(range(f.q), repeat=4): + word = upper_word(f, matrix) + require(f.mm(f.mm(word[0], word[1]), word[2]) == matrix, "upper word") + rights = ((1, 0), (0, 1), (1, 0)) + for factor, right in zip(word, rights, strict=True): + left = (f.sub(factor[0], 1), factor[2]) if right == (1, 0) else ( + factor[1], f.sub(factor[3], 1)) + require(f.paid(left, right) == factor, "common paid right vector") + for v in f.vectors: + actual = v + for factor in reversed(word): + actual = f.act(factor, actual) + require(actual == f.act(matrix, v), "literal arbitrary-input action") + input_count += 1 + reversals += f.mm(f.mm(word[2], word[1]), word[0]) != matrix + omissions += f.mm(word[0], word[1]) != matrix + mutant = upper_word(f, matrix, wrong_sign=True) + sign_errors += f.mm(f.mm(mutant[0], mutant[1]), mutant[2]) != matrix + target_count += 1 + require(reversals > 0 and omissions > 0, "word mutation controls") + if f.q in (3, 5, 7): + require(sign_errors > 0, "odd-field sign control") + return {"q": f.q, "matrices": target_count, "inputs": input_count, + "reversed_rejected": reversals, "omitted_rejected": omissions, + "wrong_sign_rejected": sign_errors} + + +def sharp_check(f): + matrices = [] + for t in f.lines: + annihilator = (f.neg[t[1]], t[0]) + for image in ((1, 0), (0, 1)): + matrices.append(tuple(f.mul[image[i]][annihilator[j]] + for i in range(2) for j in range(2))) + require(len(matrices) == 2 * (f.q + 1), "sharp family size") + require(not grouped_pivot(f, matrices) and full_pivot(f, matrices) is None, + "sharp lower bound") + for i in range(len(matrices)): + reduced = matrices[:i] + matrices[i+1:] + require(grouped_pivot(f, reduced) and full_pivot(f, reduced) is not None, + "deleting any component removes the obstruction") + repeated = [matrices[2*i] for i in range(f.q + 1) for _ in range(2)] + require(grouped_pivot(f, repeated) and full_pivot(f, repeated) is not None, + "multiplicity is not image diversity") + require(all(full_pivot(f, [a]) is not None for a in matrices), + "common-chart control") + return {"q": f.q, "threshold": len(matrices), "deletions": len(matrices)} + + +def receipt(payload): + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + raw = (root / name).read_bytes() + require(len(raw) <= 1024 * 1024, "receipt source size bound") + hashes[name] = sha256(raw).hexdigest() + print(json.dumps({"schema": "singular-product-threshold/v1", + "sources": hashes, "result": payload}, sort_keys=True)) + + +def main(): + rows, supports = binary_census() + fields, sharp = [], [] + for q in (2, 3, 4, 5, 7): + f = Field(q) + fields.append(field_check(f)) + sharp.append(sharp_check(f)) + rejected = False + try: + Field(6) + except ValueError: + rejected = True + require(rejected, "composite modulus control") + print("PASS_SINGULAR_PRODUCT_THRESHOLD binary_cost3=19440 threshold=6 no_new_kappa") + receipt({"binary": rows, "supports": supports, "fields": fields, "sharp": sharp}) + + +if __name__ == "__main__": + main()