From 4268eab9d5bc1293a006d27abf9164d125ff094d Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 10:04:35 +0000 Subject: [PATCH] feat(research): classify polynomial two-gap insertion pairs --- .../polynomial-two-gap-insertions/README.md | 185 +++++++++++++ .../SOURCES.json | 26 ++ .../polynomial-two-gap-insertions/TASK.json | 109 ++++++++ .../polynomial-two-gap-insertions/VERIFY.json | 33 +++ .../polynomial-two-gap-insertions/verify.py | 248 ++++++++++++++++++ 5 files changed, 601 insertions(+) create mode 100644 research/polynomial-two-gap-insertions/README.md create mode 100644 research/polynomial-two-gap-insertions/SOURCES.json create mode 100644 research/polynomial-two-gap-insertions/TASK.json create mode 100644 research/polynomial-two-gap-insertions/VERIFY.json create mode 100644 research/polynomial-two-gap-insertions/verify.py diff --git a/research/polynomial-two-gap-insertions/README.md b/research/polynomial-two-gap-insertions/README.md new file mode 100644 index 0000000000..d3169b4845 --- /dev/null +++ b/research/polynomial-two-gap-insertions/README.md @@ -0,0 +1,185 @@ +# Exact polynomial pairs across two stage-0 gaps + +**Claim type: scoped written proof with exact finite corroboration.** +For the two literal gaps in unpaidmoon's [PR #7103][7103], replacing constant +insertion matrices by matrices over `K[x]` permits previously excluded +off-diagonal couplings through coordinate 1. Over every field `K`, all pairs +of entry degree at most `d >= 0` form an affine space of dimension +**`64d + 50`**. In particular, the degree-one dimension is **114**. The proof +gives an explicit bijection, hence exactly `q^(64d+50)` pairs over `F_q`. +The checker enumerates small entrywise factors of that count; it does not +enumerate the entire degree-one space. + +This answers Open next question 2 of #7103. Its constant-entry classification +is a cited predecessor, not the deliverable. No new kappa, paid-rank gain, +native caller, supplier admission or complete multiplication theorem is claimed. + +## Literal word and target + +Use zero-based matrix indices `0,...,7` and ordinary written matrix-product +order, exactly as in #7103. Work in `K[x,y,z][e]/(e^2)`, with `e` central. +For stage `s=0,1,2`, write `x_s=x,y,z`, respectively. Its three diagonal gates, +in order, are + +```text +I + x_s E00, I + x_s E11, +I + x_s (E_(2+2s,2+2s) + E_(3+2s,3+2s)). +``` + +Concatenate the stages to obtain `G0,...,G8`, and let `P=G0...G8`. +Insert `I+eR` just after `G0` and `I+eS` just after `G1`. The question is + +```text +G0 (I+eR) G1 (I+eS) G2 ... G8 = (1+e) P. (1) +``` + +Here `R,S` have entries in `K[x]`. Their pure term always remains `P`. +Equation (1) requires the coefficient of `e` to equal **`P`**, rather than +the identity. Matrix equality means the endpoint holds on every initial +input vector; it does not establish a physical workspace contract. + +## Classification and proof + +Put `t=1+x`, `B=G1=diag(1,t,1,1,1,1,1,1)` and `H=G2...G8`. +Expanding the left side of (1), using centrality and `e^2=0`, gives + +```text +P + e G0 (R B + B S) H. +``` + +Every diagonal entry of `G0` and `H` is a nonzero polynomial. Since +`K[x,y,z]` is an integral domain, entrywise cancellation is valid even +though these matrices are not invertible over the polynomial ring. +Thus (1) is equivalent to + +```text +R B + B S = B. (2) +``` + +Write `b_1=t` and `b_i=1` for `i != 1`. Equation (2) at `(i,j)` is +`b_j R_ij + b_i S_ij = b_i delta_ij`. Solving each independent entry gives +the complete list: + +| Position | All solutions | +|---|---| +| `i=j` | `R_ii=a_i`, `S_ii=1-a_i` | +| `i!=j`, both different from 1 | `R_ij=a_ij`, `S_ij=-a_ij` | +| `i=1`, `j!=1` | `R_1j=-t p_j`, `S_1j=p_j` | +| `j=1`, `i!=1` | `R_i1=p_i`, `S_i1=-t p_i` | + +All parameters are arbitrary polynomials. Necessity follows directly from +the entry equation; substitution proves sufficiency. Each parameter can be +recovered from the displayed pair, so the parametrization is injective as +well as surjective. In characteristic two the displayed minus signs become +plus signs. + +Now impose entry degree at most `d`. Each of the eight diagonal parameters +and the `7*6=42` off-diagonal parameters missing coordinate 1 has degree at +most `d`. Each of the fourteen crossing parameters has degree at most `d-1`: +for nonzero `p`, the monic polynomial `t` satisfies `deg(tp)=deg(p)+1`. +When `d=0`, those fourteen parameters must be zero. The solution space is +therefore explicitly affine-isomorphic to + +```text +(K[x]_(<=d))^50 x (K[x]_(<=d-1))^14, +``` + +where `K[x]_(<=-1)={0}`. Its dimension is +`50(d+1)+14d=64d+50`. Over a field with `q` elements the bijection gives +the stated exact count. This is a parameter count, not a claim that the +checker visited each full pair. + +The simplest new crossing solution, valid even over the integers, is + +```text +R = I - (1+x) E10, S = E10. +``` + +Indeed, `E10 B=E10` and `B E10=t E10`, so `RB+BS=B`. +It has degree one. Degree zero cannot realize any nonzero crossing entry, +by the degree restriction just proved. This settles the minimum degree for +opening such a coupling. Reversing the two occurrences of `t` does not work; +the written product order matters. + +## Evidence and reproduction + +The proof above supplies the quantifiers over every field and every `d`. +The standalone [verifier](verify.py) uses only the Python 3.12 standard library. +It derives both entry scales from the literal nine gates, then: + +- computes coefficient-system ranks for `d=1,2,3,4` over `F2,F3,F5,F7`; + the resulting affine dimensions are `114,178,242,306`, respectively; +- exhausts **56,960 entry pairs** in the four domains `(q,d)=(2,1),(2,2), + (3,1),(3,2)`, compares the solved criterion with the literal scales, and + multiplies the entrywise counts using their Cartesian independence; +- multiplies the full eleven-factor operator for **56 integer crossing + witnesses**, covering both crossing directions, all seven other coordinates + and parameters `1,x,x^2,x^3`, plus the affine origin `(I,0)`; +- rejects four false witnesses: reversed crossing orientation, a missing + `x` term, an omitted second insertion, and `(I,I)`. + +It prints `PASS_POLYNOMIAL_TWO_GAP_INSERTIONS` and a generated JSON receipt +binding its results to SHA256 hashes of all five package files. The receipt +is emitted to stdout, never maintained by hand. + +From the repository root, the exact local interpreter is +`~/git/integer-mult-bounds/.venv/bin/python3.12` (CPython 3.12.15): + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/polynomial-two-gap-insertions/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/polynomial-two-gap-insertions/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/polynomial-two-gap-insertions +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/polynomial-two-gap-insertions --check-source-history +``` + +Both registered checks have 30-second limits. Explicit exceptions keep the +checks active under `-O`. [TASK.json](TASK.json) records the changed card +scope and open question. [SOURCES.json](SOURCES.json) pins the historical +catalogue and selected record, and separately lists the immutable external +citation. No external file or predecessor verifier is loaded at runtime; +the word and convention used here are fully specified above. + +The verifier has no recursive calls or unbounded searches. Width is fixed +at eight, degree at four, field samples at seven, the largest enumeration +at 729 polynomial pairs per entry, and the longest word at eleven factors. +Python requires dynamic allocation; bounded finite collections replace the +fixed-allocation rule. Warning-strict normal and optimized checks provide +runtime diagnostics. No additional static type checker is required by this +package. These checks corroborate a written proof, not a formal-kernel proof. + +## Limitations + +The allowed insertion entries change from constants to `K[x]`. Their +implementation, interaction with the native stage operator, physical +restoration, precision, hosting and complete signed invoice are unproved. +The displayed witness has no established cost advantage over `(I,0)`. +Other gap pairs, non-idempotent stage factors and the larger paired-star +callers are outside scope. No predecessor scientific replay, Lean, Docker, +selected-frontier replay or complete multiplication implementation was run. +The selected result is unchanged. + +## Open next questions + +Can a polynomial crossing pair reduce a complete legal invoice after every +`x`-dependent entry is implemented and restoration is charged? Start with +`R=I-(1+x)E10, S=E10` and compare its physical realization with `(I,0)`. +The blocker is a legal, fully priced implementation of those entries. This +is necessary before the new algebraic freedom can advance a supplier. +The structured question is also in [TASK.json](TASK.json). + +## Credit + +This result was produced by Nick Petalas. New work is Apache-2.0. + +Credit **unpaidmoon** for #7103, exact head +`f3af1384aeda8c75be58f09cb07da3941ba7aba3`, which poses the polynomial-entry +question and fixes the gap convention; #7027, head +`1ba2ac5adfe58fbe9dba34d50d4e5d30633ce3d0`, supplies the diagonal word; +#7039, head `e4ddcd2fde8c46b7e528e8806ab72d9bf7690978`, distinguishes the +one-gap coefficient targets. Credit **Ali Romman** for the paired-star +contract in #5747 and its retained #5673, #5631 and #5617 lineage. Their +source attributions remain in their original packages. The new step here +is the polynomial classification, its exact degree filtration and its +explicit crossing witnesses. + +[7103]: https://github.com/CrocSwap/integer-mult-bounds/pull/7103 diff --git a/research/polynomial-two-gap-insertions/SOURCES.json b/research/polynomial-two-gap-insertions/SOURCES.json new file mode 100644 index 0000000000..8186f0e446 --- /dev/null +++ b/research/polynomial-two-gap-insertions/SOURCES.json @@ -0,0 +1,26 @@ +{ + "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" + } + ], + "external_citations": [ + { + "pr": 7103, + "commit": "f3af1384aeda8c75be58f09cb07da3941ba7aba3", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f3af1384aeda8c75be58f09cb07da3941ba7aba3/research/two-gap-constant-insertion/PROOF.md", + "role": "Cited mathematical predecessor, not loaded by the verifier. The literal word and gap order are stated completely in README.md." + } + ] +} diff --git a/research/polynomial-two-gap-insertions/TASK.json b/research/polynomial-two-gap-insertions/TASK.json new file mode 100644 index 0000000000..0e34e40fe6 --- /dev/null +++ b/research/polynomial-two-gap-insertions/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify every R,S in M8(K[x]) of entry degree at most d in the two adjacent stage-0 gaps of PR7103, over every field K, with central e^2=0 and coefficient of e equal to the literal pure product.", + "scope_change_reason": "The card asks for a changed query-demand construction. This package takes the explicit polynomial-entry question in PR7103 and proves a local algebraic interface classification; it supplies no complete caller or invoice gain.", + "bottleneck_link": "Polynomial insertion freedom changes which off-diagonal couplings are algebraically possible across a native-call boundary. Physical realization, native legality and a favorable complete signed bill remain open; this is a scoped interface result.", + "budget_minutes": 60, + "stop_rule": "Stop at the first original proved classification and its exact finite corroboration; do not extend to new gaps, words or paid-rank optimization.", + "outcome": "completed", + "evidence": "Scoped written proof in README.md: explicit bijection with K[x] degree-bounded parameter spaces. Exact independent coefficient elimination, exhaustive entry-pair checks and full integer polynomial operator witnesses in verify.py corroborate the proof. Not a formal-kernel proof or a complete multiplication theorem.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a polynomial crossing pair reduce a complete legal paid invoice after its x-dependent entries are implemented and all restoration costs are charged?", + "why_it_matters": "The new coefficient freedom alone does not save recursive work or improve kappa.", + "first_step": "Implement the explicit R=I-(1+x)E10, S=E10 pair in the actual native interface and compare its full bill with R=I, S=0.", + "blocked_by": "No paid implementation or native legality for the polynomial insertions is provided." + } + ], + "predecessors": [ + { + "pr": 7103, + "author": "unpaidmoon", + "head": "f3af1384aeda8c75be58f09cb07da3941ba7aba3", + "role": "Question source, literal two-gap convention and constant-entry predecessor; cited, not audited." + }, + { + "pr": 7027, + "author": "unpaidmoon", + "head": "1ba2ac5adfe58fbe9dba34d50d4e5d30633ce3d0", + "role": "Literal diagonal nine-gate word." + }, + { + "pr": 7039, + "author": "unpaidmoon", + "head": "e4ddcd2fde8c46b7e528e8806ab72d9bf7690978", + "role": "One-gap predecessor and distinction between coefficient targets I and P." + }, + { + "pr": 5747, + "author": "aliromman", + "role": "Paired-star contract and retained PR5673, PR5631 and PR5617 lineage." + } + ] +} diff --git a/research/polynomial-two-gap-insertions/VERIFY.json b/research/polynomial-two-gap-insertions/VERIFY.json new file mode 100644 index 0000000000..a15e10badd --- /dev/null +++ b/research/polynomial-two-gap-insertions/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact finite polynomial coefficient systems, exhaustive entry-pair checks, complete integer operator witnesses and four false witnesses." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Repeat the same real verifier with isolation and assertions disabled; proof-relevant checks use explicit exceptions." + } + ] +} diff --git a/research/polynomial-two-gap-insertions/verify.py b/research/polynomial-two-gap-insertions/verify.py new file mode 100644 index 0000000000..0831174e61 --- /dev/null +++ b/research/polynomial-two-gap-insertions/verify.py @@ -0,0 +1,248 @@ +#!/usr/bin/env python3 +"""Exact corroboration for polynomial two-gap insertions. Apache-2.0.""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +type Monomial = tuple[int, int, int, int] +type Poly = dict[Monomial, int] +type Matrix = list[list[Poly]] + +ONE: Monomial = (0, 0, 0, 0) +X: Monomial = (1, 0, 0, 0) +EPS: Monomial = (0, 0, 0, 1) +WIDTH = 8 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def add(a: Poly, b: Poly) -> Poly: + result = a.copy() + for monomial, value in b.items(): + result[monomial] = result.get(monomial, 0) + value + if result[monomial] == 0: + del result[monomial] + return result + + +def scale(a: Poly, coefficient: int) -> Poly: + return {m: coefficient * value for m, value in a.items() + if coefficient * value != 0} + + +def mul(a: Poly, b: Poly) -> Poly: + result: Poly = {} + for left, u in a.items(): + for right, v in b.items(): + monomial = tuple(left[i] + right[i] for i in range(4)) + if monomial[3] <= 1: + result[monomial] = result.get(monomial, 0) + u * v + return {m: value for m, value in result.items() if value} + + +def identity() -> Matrix: + return [[{ONE: 1} if i == j else {} for j in range(WIDTH)] + for i in range(WIDTH)] + + +def matrix_mul(a: Matrix, b: Matrix) -> Matrix: + result = [[{} for _ in range(WIDTH)] for _ in range(WIDTH)] + for i in range(WIDTH): + for k in range(WIDTH): + if a[i][k]: + for j in range(WIDTH): + result[i][j] = add(result[i][j], mul(a[i][k], b[k][j])) + return result + + +def gates() -> list[Matrix]: + result = [] + for stage in range(3): + variable = tuple(int(i == stage) for i in range(4)) + for support in ((0,), (1,), (2 + 2 * stage, 3 + 2 * stage)): + gate = identity() + for i in support: + gate[i][i] = {ONE: 1, variable: 1} + result.append(gate) + require(len(result) == 9, "nine literal gates required") + return result + + +def insertion(matrix: Matrix) -> Matrix: + result = identity() + for i in range(WIDTH): + for j in range(WIDTH): + result[i][j] = add(result[i][j], mul({EPS: 1}, matrix[i][j])) + return result + + +def run_word(r: Matrix, s: Matrix) -> Matrix: + word = gates() + factors = [word[0], insertion(r), word[1], insertion(s), *word[2:]] + result = identity() + for factor in factors: + result = matrix_mul(result, factor) + return result + + +def target() -> Matrix: + result = identity() + for factor in gates(): + result = matrix_mul(result, factor) + for i in range(WIDTH): + result[i][i] = mul(result[i][i], {ONE: 1, EPS: 1}) + return result + + +def gap_scales() -> tuple[Matrix, Matrix]: + """Derive each entry's two scales from the literal prefix/suffix.""" + word = gates() + suffix = identity() + for factor in word[2:]: + suffix = matrix_mul(suffix, factor) + first_right = matrix_mul(word[1], suffix) + second_left = matrix_mul(word[0], word[1]) + a = [[mul(word[0][i][i], first_right[j][j]) + for j in range(WIDTH)] for i in range(WIDTH)] + b = [[mul(second_left[i][i], suffix[j][j]) + for j in range(WIDTH)] for i in range(WIDTH)] + return a, b + + +def reduce_mod(poly: Poly, prime: int) -> Poly: + return {m: c % prime for m, c in poly.items() if c % prime} + + +def column_rank(columns: list[Poly], prime: int) -> int: + basis: dict[Monomial, Poly] = {} + for column in columns: + remaining = reduce_mod(column, prime) + for _ in range(len(columns) + 1): + if not remaining: + break + pivot = min(remaining) + if pivot not in basis: + inverse = pow(remaining[pivot], -1, prime) + basis[pivot] = reduce_mod(scale(remaining, inverse), prime) + break + multiple = scale(basis[pivot], -remaining[pivot]) + remaining = reduce_mod(add(remaining, multiple), prime) + else: + raise ValueError("column elimination exceeded its finite bound") + return len(basis) + + +def check_dimensions(a: Matrix, b: Matrix) -> list[dict[str, int]]: + records = [] + for prime, degree in product((2, 3, 5, 7), range(1, 5)): + rank = 0 + for i, j in product(range(WIDTH), repeat=2): + columns = [mul(factor, {(power, 0, 0, 0): 1}) + for factor in (a[i][j], b[i][j]) + for power in range(degree + 1)] + rank += column_rank(columns, prime) + dimension = 128 * (degree + 1) - rank + require(dimension == 64 * degree + 50, "wrong affine dimension") + records.append({"prime": prime, "degree": degree, + "rank": rank, "dimension": dimension}) + return records + + +def all_polynomials(prime: int, degree: int) -> list[Poly]: + return [{(power, 0, 0, 0): value + for power, value in enumerate(coefficients) if value} + for coefficients in product(range(prime), repeat=degree + 1)] + + +def predicted_pair(r: Poly, s: Poly, i: int, j: int, prime: int) -> bool: + t = {ONE: 1, X: 1} + if i == j: + difference = add(add(r, s), {ONE: -1}) + elif i == 1: + difference = add(r, mul(t, s)) + elif j == 1: + difference = add(mul(t, r), s) + else: + difference = add(r, s) + return not reduce_mod(difference, prime) + + +def check_entry_pairs(a: Matrix, b: Matrix) -> int: + examined = 0 + for prime, degree in ((2, 1), (2, 2), (3, 1), (3, 2)): + polynomials = all_polynomials(prime, degree) + total_solutions = 1 + for i, j in product(range(WIDTH), repeat=2): + hits = 0 + for r, s in product(polynomials, repeat=2): + lhs = add(mul(a[i][j], r), mul(b[i][j], s)) + rhs = a[i][i] if i == j else {} + actual = not reduce_mod(add(lhs, scale(rhs, -1)), prime) + require(actual == predicted_pair(r, s, i, j, prime), + "entry criterion disagrees with literal gap scales") + hits += int(actual) + examined += 1 + total_solutions *= hits + require(total_solutions == prime ** (64 * degree + 50), + "Cartesian product of enumerated entry solutions disagrees") + return examined + + +def zero_matrix() -> Matrix: + return [[{} for _ in range(WIDTH)] for _ in range(WIDTH)] + + +def check_witnesses() -> tuple[int, int]: + expected = target() + require(run_word(identity(), zero_matrix()) == expected, + "affine origin is not a solution") + successes = 0 + for other in (0, 2, 3, 4, 5, 6, 7): + for power in range(4): + p = {(power, 0, 0, 0): 1} + t_p = mul({ONE: 1, X: 1}, p) + for row_crossing in (False, True): + r, s = identity(), zero_matrix() + if row_crossing: + r[1][other], s[1][other] = scale(t_p, -1), p + else: + r[other][1], s[other][1] = p, scale(t_p, -1) + require(run_word(r, s) == expected, + "polynomial crossing witness fails over the integers") + successes += 1 + r, s = identity(), zero_matrix() + controls = [] + r[1][0], s[1][0] = {ONE: -1}, {ONE: 1, X: 1} + controls.append(run_word(r, s) != expected) + s[1][0] = {ONE: 1} + controls.append(run_word(r, s) != expected) + r[1][0], s[1][0] = {ONE: -1, X: -1}, {} + controls.append(run_word(r, s) != expected) + controls.append(run_word(identity(), identity()) != expected) + require(all(controls), "a false witness passed") + return successes, len(controls) + + +def main() -> None: + a, b = gap_scales() + dimensions = check_dimensions(a, b) + examined = check_entry_pairs(a, b) + witnesses, controls = check_witnesses() + package = Path(__file__).resolve().parent + files = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + receipt = {"dimensions": dimensions, "entry_pairs_examined": examined, + "integer_crossing_witnesses": witnesses, + "false_witnesses_rejected": controls, + "sha256": {name: sha256((package / name).read_bytes()).hexdigest() + for name in files}} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_POLYNOMIAL_TWO_GAP_INSERTIONS") + + +if __name__ == "__main__": + main()