diff --git a/research/coupled-resonant-jordan-pair/PROOF.md b/research/coupled-resonant-jordan-pair/PROOF.md new file mode 100644 index 0000000000..8767c35a60 --- /dev/null +++ b/research/coupled-resonant-jordan-pair/PROOF.md @@ -0,0 +1,143 @@ +# Coupling two individually rigid resonant Jordan blocks + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped mathematical proof. The finite verifier corroborates the +argument; independent human and formal proof-kernel review are unclaimed. + +## Statement + +Let F_q be any finite field. Choose nonzero lambda_1, lambda_2 with +lambda_i^2=1, and put + + P = diag(J_2(lambda_1), J_2(lambda_2)), + J_2(lambda) = [[lambda,1],[0,lambda]]. + +Use precisely the ordinary wrapper of Nicholas Stone's #5556, on arbitrary +H,D in F_q^4, with chronological operations + + D -= H; F_P; D += H; F_Q; D = -D; D += H, + F_T(H,D) = (T D, T^-1 H). + +Require Q invertible. Optimality means least rank of the difference between +this wrapper and the interchange (H,D) -> (D,H), with this P fixed. + +**Theorem.** In characteristic two the unique optimum is Q=P. In odd +characteristic there are exactly q^2 optimal Q, all with determinant one. +Exactly q^2-1 have rank(Q-P)=1. In coordinates 0,1,2,3, the complete list is + + Q = P + U D S V, S^2=0, + U = [e_0 e_2], V = [e_1^T; e_3^T], + D = diag(2 lambda_1, 2 lambda_2). + +Here S is an arbitrary two-by-two matrix over F_q. The parameterization is +injective in odd characteristic. The minimum wrapper error rank is two in +odd characteristic and zero in characteristic two. Thus odd-characteristic +optimal wrappers agree with interchange on exactly q^6 of the q^8 input pairs. + +Each individual J_2(lambda_i) has a unique optimum by #5556. Their direct +sum has q^2 optima in odd characteristic. Multiplying individual counts +would give one and misses all q^2-1 new coupled maps. + +## Credited starting point + +Nicholas Stone's [#5556](https://github.com/CrocSwap/integer-mult-bounds/pull/5556), +`research/jordan-second-callee-count/PROOF.md`, gives the fixed-wrapper +error reduction. Write A=P^2-I and R=Q-P. For invertible P and Q, the +wrapper error rank is + + rank M, M = [[A,R],[R,0]]. (1) + +The minimum is rank A, attained by R=0. The error identity and optimum are +used as inherited statements, not re-audited here. They originate in Jerry +Chen / CubeJerry's #2950 and Nick Petalas's #5228. The latter gives a general +equality characterization for arbitrary P. The argument below specializes +(1) directly to the new coupled pair and counts its complete solution set. +It does not claim the general characterization as new. + +Nick Petalas's #6406 counts regular J_3(lambda), where P^2-I is invertible. +Our P has singular P^2-I. The block-coupling question appears in #5556's +Open next questions. No predecessor executable is used. + +## The support forced by equality + +In odd characteristic, each block of P has square +I+2 lambda_i N, where N=[[0,1],[0,0]]. Therefore + + A=U D V, rank A=2, V U=0, + im A=span(e_0,e_2), ker A=span(e_0,e_2). + +If rank M=rank A, its top block row [A R] cannot have rank greater than A. +Thus im R is contained in im A. The first block column [A; R] likewise +forces ker A contained in ker R. These two containments say exactly that + + R=U T V (2) + +for a unique two-by-two T. In particular the only possible nonzero entries +of R are at (0,1),(0,3),(2,1),(2,3). No candidate is discarded on a clean-input +assumption. These are consequences of equality for the entire error map. + +Substitute (2) into M and delete its identically zero rows and columns. +Permuting the remaining rows and columns yields + + [[D,T],[T,0]]. + +Since D is invertible, block elimination gives + + rank M = 2 + rank(T D^-1 T). + +Put T=D S. Then T D^-1 T=D S^2, so equality is equivalent to S^2=0. +Since U has independent columns, V has independent rows and D is invertible, +different S yield different R and hence different Q. + +## The invertibility filter accepts every parameter + +Order the coordinates as (0,2,1,3). In this order P+U D S V is + + [[Lambda, I_2+D S], [0,Lambda]], + Lambda=diag(lambda_1,lambda_2). + +It is invertible for every S, with determinant +(lambda_1 lambda_2)^2=1. Invertibility is proved before counting; no singular +second maps are counted as optima. This remains true when the two signs differ. + +## Count and perturbation ranks + +The square-zero two-by-two matrices over any field are exactly + + S=[[a,b],[c,-a]], a^2+bc=0. (3) + +This elementary parameterization, including characteristic two, is recorded +in #5556. For c=0, the equation forces a=0 and permits any b, giving q choices. +For each of the q-1 nonzero c, any a determines the unique b=-a^2/c, +again giving q choices. Thus (3) gives q+(q-1)q=q^2 parameters. +One is zero; every other one has rank one because im S is contained in ker S. +The injective left/right maps in U D S V preserve that rank. This proves +the count and the stated rank distribution. + +For a concrete coupled optimum take S=E_01. Then R has the single nonzero +entry R_03=2 lambda_1. Both diagonal two-by-two blocks of Q remain unchanged, +yet Q differs from the independent-block optimum P. + +Finally, a rank-two linear error map on the eight-dimensional input space +has a six-dimensional kernel, hence q^6 agreeing inputs. + +## Characteristic two + +The equation lambda_i^2=1 over a field of characteristic two implies +lambda_i=1. Each J_2(1) squares to I, so A=0. Equation (1) then has rank +2 rank R. Its minimum zero is attained exactly when R=0. Consequently Q=P +is the unique optimum. The odd-characteristic count cannot be transferred +to this case because D is zero. + +## Scope and open next questions + +This settles one coupled finite-field equality/counting problem. The first +verified pair ended the investigation. No larger block family, selected +assumption, physical implementation or cost advantage is proved. Native +coefficients, movement, restoration, precision, stock, compiler and outer +costs remain unpriced. No new kappa, selected frontier, exact interchange in +odd characteristic, or complete multiplication theorem is claimed. + +Further questions and their first steps are in TASK.json. Classical block +elimination, rank-nullity and finite-field counting are not claimed as new. diff --git a/research/coupled-resonant-jordan-pair/README.md b/research/coupled-resonant-jordan-pair/README.md new file mode 100644 index 0000000000..f3693965f4 --- /dev/null +++ b/research/coupled-resonant-jordan-pair/README.md @@ -0,0 +1,127 @@ +# Two rigid Jordan blocks have q squared coupled optima + +This contribution was produced by Nick Petalas. Apache-2.0. + +For the unchanged ordinary wrapper, fix + + P=diag(J_2(lambda_1),J_2(lambda_2)), lambda_i^2=1. + +Over any odd finite field F_q, there are exactly **q^2** optimal invertible +second maps Q. In characteristic two, Q=P is the unique optimum. This is a +scoped written proof with exact finite corroboration, with no new kappa. + +Nicholas Stone's [#5556](https://github.com/CrocSwap/integer-mult-bounds/pull/5556) +proves that either block alone has only one optimum and leaves coupled +blocks open. The new count shows why multiplying individual counts fails. +Its fixed-wrapper error reduction and two-dimensional square-zero count +are cited inputs. No predecessor scientific verifier is replayed. + +## Complete parameterization + +In odd characteristic, all optima are exactly + + Q=P+U D S V, S^2=0, + U=[e_0 e_2], V=[e_1^T; e_3^T], + D=diag(2 lambda_1,2 lambda_2). + +The q^2 square-zero matrices S give distinct Q. Every such Q has determinant +one; q^2-1 have rank(Q-P)=1. For example S=E_01 adds the single cross-block +entry Q_03=2 lambda_1 without changing either diagonal Jordan block. + +[PROOF.md](PROOF.md) proves completeness by forcing the perturbation into +the rank-two image/kernel support, then reducing the remaining equality to +S^2=0. The determinant filter accepts every parameter, including mixed signs. +The minimum error rank is two in odd characteristic. Agreement with exact +interchange therefore holds on q^6 of q^8 inputs, rather than on every input. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/coupled-resonant-jordan-pair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/coupled-resonant-jordan-pair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/coupled-resonant-jordan-pair +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/coupled-resonant-jordan-pair --check-source-history +``` + +Another CPython 3.12 path may replace the prefix. The direct marker is +`PASS_COUPLED_RESONANT_JORDAN_PAIR no_new_kappa`. Each run prints a generated +JSON receipt bound to SHA256 hashes of all six package files and writes no +files. There is no handwritten receipt or predecessor executable dependency. +[VERIFY.json](VERIFY.json) registers normal and optimized commands. Explicit +exceptions keep every acceptance check active with Python -O. + +The verifier builds exact fields of orders 2,3,4,5,7,8,9,11,13 and checks +their field laws. It enumerates every four-entry perturbation in the forced +support for every resonant sign pair, compares the complete accepted set +with a separately enumerated square-zero catalogue, and runs all eight +original input basis columns of every accepted wrapper. It also enumerates +all 65,536 binary four-by-four second maps and executes the literal wrapper +on every invertible one. Rejection controls cover off-support entries, +non-square-zero couplings and misuse of the odd-characteristic count. +The extension fields use polynomial coordinates, not composite-modulus +integer arithmetic. + +The finite totals are 27 field/sign contexts, 215,848 supported perturbations +and 1,819 accepted wrappers. The full binary census has 20,160 invertible +second maps and exactly one optimum. Together the literal replays check +175,832 original input basis columns. Fifteen rejection controls and one +coupled positive control pass. Normal and optimized local runs on CPython +3.12.15 produce identical receipts. + +## Scope and credit + +The `formal-interface-lemma` card has changed scope to this algebraic side +result. No selected assumption is discharged. Native implementation, +restoration, movement, precision, stock, compiler, complete supplier costs +and outer use remain unpriced. The selected #7000 frontier is unchanged. +No larger block family, complete multiplication theorem, independent human +review or formal proof-kernel acceptance is claimed. Lean, Docker, predecessor +scientific suites and the selected cold replay are unrun. + +Credit Nicholas Stone / #5556 for the multiblock question, Jordan method, +wrapper reduction and two-dimensional square-zero count; Nick Petalas / +#5228 for the general equality characterization and #6406 for the distinct +regular J3 count; Jerry Chen / CubeJerry / #2950 for the wrapper optimum; +and the retained ordinary/native lineage. Classical block elimination and +finite-field counting are not claimed as new. [SOURCES.json](SOURCES.json) +pins predecessor prose, catalogue and selected record as historical provenance. +The direct verifier imports none of them. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539400) +records the question. Base is canonical main +`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8. Entry checks +covered live open PRs, this account's recent work, recent handoffs and local +reservations, all 10,178 current note records, cached snapshots of 488 open +PRs and 7,148 Discussion records, and targeted main/merged searches. No +matching coupled resonant-pair count surfaced. Unpublished work and arbitrary +historical diffs remain coverage limits. + +## Open next questions + +- Count one pair with at least one eigenvalue squared different from one. + First fix distinct regular eigenvalues over F5 and derive the new quotient + and determinant filter. The present singular-support reduction does not + classify that problem. +- Price one explicit coupled map in a physically specified ordinary caller. + Its correctness domain, native coefficients and restoration costs must be + supplied before optimal agreement can imply a useful implementation. + +The structured questions are in [TASK.json](TASK.json). The first proved pair +ended the investigation. + +## Verification constraints + +The standalone verifier has no recursion, subprocesses, network calls or +external scientific imports. Its domains are fixed at q<=13 and matrix sizes +two, four or eight. Candidate scans stream at most 13^4 tuples per context; +accepted sets contain at most 169 tuples. The binary scan visits 2^16 matrices. +Every function is shorter than 60 physical lines. Exceptions enforce matrix, +field, rank and endpoint invariants in both interpreter modes. + +Managed CPython allocation is a Power of Ten rule 3 deviation. Fixed domains +bound live collections; no fixed-allocation runtime is claimed. Rule 10 uses +warning-strict execution and AST compilation, plus the registered replay; +no separate static analyzer is configured. Revisit these bounds before +accepting variable fields or dimensions. No shared implementation is changed. diff --git a/research/coupled-resonant-jordan-pair/SOURCES.json b/research/coupled-resonant-jordan-pair/SOURCES.json new file mode 100644 index 0000000000..78322f75cf --- /dev/null +++ b/research/coupled-resonant-jordan-pair/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/jordan-second-callee-count/PROOF.md", + "usage": "provenance", + "git_blob": "9686b917aa7bfd9a3b59672bec414d68cfae6aad", + "sha256": "e267e006f420563548bc5b36817691e3772c8237552f266382b0974f10b2abe5" + }, + { + "path": "research/jordan-second-callee-count/README.md", + "usage": "provenance", + "git_blob": "da13fd8c532ac2494aa5f0b6e959f4fa971a2290", + "sha256": "d5370bdc01a7aa8bc8b1b039548ecb8fce09dfa633cf72ca77bc59b780461611" + }, + { + "path": "research/jordan-three-callee-count/README.md", + "usage": "provenance", + "git_blob": "8c5bf956d34ba972a89afd46851e2f942c536a1e", + "sha256": "5f37421eeca0a1dc6ffc277ca50a07736b1b32919913a3e4b3d13237042447ae" + }, + { + "path": "research/optimal-second-callees/README.md", + "usage": "provenance", + "git_blob": "01bf464c2cfbf576a089f1cdc5e71b367d7fcf85", + "sha256": "99c816abf0a7f0ef25843a7adb3b29b4ab983d108c04506827a622f696a5f33e" + } + ] +} diff --git a/research/coupled-resonant-jordan-pair/TASK.json b/research/coupled-resonant-jordan-pair/TASK.json new file mode 100644 index 0000000000..72014ad296 --- /dev/null +++ b/research/coupled-resonant-jordan-pair/TASK.json @@ -0,0 +1,137 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify and count optimal second callees for exactly two resonant length-two Jordan blocks over every finite field.", + "scope_change_reason": "Nicholas Stone's PR5556 explicitly leaves coupling between several Jordan blocks open. This is a written finite-field equality/counting theorem, not a proof-assistant caller binding or audit of that predecessor.", + "bottleneck_link": "Algebraic interface side result: independent-block rigidity does not determine the coupled optimal-callee set. No native cost advantage or selected assumption is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop after the first coupled-pair theorem, exact bounded corroboration and one focused PR. Do not extend to larger block families.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-field theorem. verify.py checks 27 field/sign contexts, 215848 supported perturbations, 1819 accepted wrappers, all 65536 binary second maps including 20160 invertible ones, 175832 literal input basis columns, and 15 rejection controls. It emits a package-hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "How many optimal second callees survive for two length-two blocks with at least one eigenvalue squared different from one?", + "why_it_matters": "The singular resonant case has no determinant rejections; other blocks may couple through a nontrivial filter.", + "first_step": "Fix one concrete pair of distinct regular eigenvalues over F5 and write its complete square-zero quotient and determinant filter.", + "blocked_by": "The rank-two support reduction here uses both eigenvalues squared equal to one; the other quotient and its filter are not classified." + }, + { + "question": "Does one physically specified ordinary caller benefit from a coupled optimal map in this family?", + "why_it_matters": "Optimal agreement alone supplies no implementation saving.", + "first_step": "Choose one of the explicit single-entry coupled maps and price both callees with the actual correctness domain and restoration requirements.", + "blocked_by": "No native or physical cost model is supplied by this algebraic result." + } + ], + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit" + }, + "claim_type": "scoped written proof with exact finite corroboration", + "predecessors": [ + { + "pr": 5556, + "author": "Nicholas Stone / NicholasStone", + "usage": "Primary source of the several-block question, fixed-wrapper error matrix and square-zero two-dimensional count." + }, + { + "pr": 5228, + "author": "Nick Petalas", + "usage": "Credited general equality characterization; not re-audited or used as a new result." + }, + { + "pr": 6406, + "author": "Nick Petalas", + "usage": "Comparison with the already solved regular J3 count; a different first map." + }, + { + "pr": 2950, + "author": "Jerry Chen / CubeJerry", + "usage": "Inherited ordinary-wrapper optimum and attainer." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539400", + "overlap": { + "checked_utc": "2026-11-11T10:02:00Z", + "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57", + "local_notes": 10178, + "cached_open_prs": 488, + "cached_discussions": 7148, + "coverage": "Complete cached local note inventory, complete cached open-PR and Discussion snapshots, live current open-PR and recent-account lists, last 30 handoff comments, main README and merged keyword searches. No unpublished work or exhaustive historical diffs." + } +} diff --git a/research/coupled-resonant-jordan-pair/VERIFY.json b/research/coupled-resonant-jordan-pair/VERIFY.json new file mode 100644 index 0000000000..d36455d9fc --- /dev/null +++ b/research/coupled-resonant-jordan-pair/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": 240, + "checks": "Exact fields, complete supported coupling catalogues, full binary second-map domain, literal wrapper basis columns, rank/determinant distribution and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact fields, complete supported coupling catalogues, full binary second-map domain, literal wrapper basis columns, rank/determinant distribution and semantic rejection controls." + } + ] +} diff --git a/research/coupled-resonant-jordan-pair/verify.py b/research/coupled-resonant-jordan-pair/verify.py new file mode 100644 index 0000000000..b44f12966f --- /dev/null +++ b/research/coupled-resonant-jordan-pair/verify.py @@ -0,0 +1,273 @@ +#!/usr/bin/env python3 +"""Finite corroboration of the coupled resonant Jordan-pair theorem. + +Produced by Nick Petalas. Apache-2.0. No predecessor code is imported. +""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def field(p, degree, modulus): + require((p, degree, modulus) in ( + (2, 1, (0,)), (3, 1, (0,)), (5, 1, (0,)), + (7, 1, (0,)), (11, 1, (0,)), (13, 1, (0,)), + (2, 2, (1, 1)), (2, 3, (1, 1, 0)), (3, 2, (1, 0))), + "unsupported field") + q = p**degree + digits = [tuple(x // p**i % p for i in range(degree)) for x in range(q)] + plus, times = [[0]*q for _ in range(q)], [[0]*q for _ in range(q)] + for x, y in product(range(q), repeat=2): + a, b = digits[x], digits[y] + plus[x][y] = sum((a[i]+b[i]) % p * p**i for i in range(degree)) + c = [0]*(2*degree-1) + for i, j in product(range(degree), repeat=2): + c[i+j] = (c[i+j]+a[i]*b[j]) % p + for i in range(2*degree-2, degree-1, -1): + for j in range(degree): + c[i-degree+j] = (c[i-degree+j]-c[i]*modulus[j]) % p + times[x][y] = sum(c[i]*p**i for i in range(degree)) + negative = [next(y for y in range(q) if plus[x][y] == 0) for x in range(q)] + inverse = [0]+[next(y for y in range(1, q) if times[x][y] == 1) + for x in range(1, q)] + return (p, q, plus, times, negative, inverse) + + +def check_field(f): + _, q, add, mul, neg, inv = f + for x in range(q): + require(add[x][0] == x and mul[x][1] == x, "field units") + require(add[x][neg[x]] == 0, "additive inverse") + require(x == 0 or mul[x][inv[x]] == 1, "multiplicative inverse") + for x, y, z in product(range(q), repeat=3): + require(add[x][y] == add[y][x] and mul[x][y] == mul[y][x], "commutativity") + require(add[add[x][y]][z] == add[x][add[y][z]], "addition associativity") + require(mul[mul[x][y]][z] == mul[x][mul[y][z]], "product associativity") + require(mul[x][add[y][z]] == add[mul[x][y]][mul[x][z]], "distributivity") + + +def zero(n): + require(n in (2, 4, 8), "matrix dimension") + return [[0]*n for _ in range(n)] + + +def eye(n): + a = zero(n) + for i in range(n): + a[i][i] = 1 + return a + + +def add_matrix(f, a, b, subtract=False): + n = len(a) + require(n in (2, 4, 8) and len(b) == n, "sum dimension") + op, neg = f[2], f[4] + return [[op[a[i][j]][neg[b[i][j]] if subtract else b[i][j]] + for j in range(n)] for i in range(n)] + + +def mm(f, a, b): + n = len(a) + require(n in (2, 4, 8) and len(b) == n, "product dimension") + out, add, mul = zero(n), f[2], f[3] + for i, j, k in product(range(n), repeat=3): + out[i][j] = add[out[i][j]][mul[a[i][k]][b[k][j]]] + return out + + +def eliminate(f, matrix, invert=False): + n = len(matrix) + require(n in (2, 4, 8) and all(len(row) == n for row in matrix), "square matrix") + require(all(type(x) is int and 0 <= x < f[1] for row in matrix for x in row), + "field coordinates") + a = [row[:] for row in matrix] + if invert: + for i in range(n): + a[i] += [int(i == j) for j in range(n)] + pivot, determinant = 0, 1 + add, mul, neg, inv = f[2:] + for col in range(n): + row = next((i for i in range(pivot, n) if a[i][col]), None) + if row is None: + determinant = 0 + continue + if row != pivot: + determinant = neg[determinant] + a[pivot], a[row] = a[row], a[pivot] + scale = a[pivot][col] + determinant = mul[determinant][scale] + a[pivot] = [mul[inv[scale]][x] for x in a[pivot]] + for i in range(n): + if i == pivot: + continue + scale = a[i][col] + a[i] = [add[x][neg[mul[scale][y]]] for x, y in zip(a[i], a[pivot])] + pivot += 1 + require(not invert or pivot == n, "singular inverse") + return pivot, determinant, [row[n:] for row in a] if invert else None + + +def jordan_pair(f, signs): + require(len(signs) == 2 and all(f[3][x][x] == 1 for x in signs), "resonant signs") + p = zero(4) + for j, lam in enumerate(signs): + p[2*j][2*j] = p[2*j+1][2*j+1] = lam + p[2*j][2*j+1] = 1 + return p + + +def perturbation(values): + require(len(values) == 4, "four entries") + r = zero(4) + for (i, j), x in zip(((0, 1), (0, 3), (2, 1), (2, 3)), values): + r[i][j] = x + return r + + +def error_block(f, p, q): + a = add_matrix(f, mm(f, p, p), eye(4), True) + r = add_matrix(f, q, p, True) + return [a[i]+r[i] for i in range(4)]+[r[i]+[0]*4 for i in range(4)] + + +def mv(f, a, v): + n = len(a) + require(n == len(v) == 4, "vector dimension") + out = [0]*n + for i, j in product(range(n), repeat=2): + out[i] = f[2][out[i]][f[3][a[i][j]][v[j]]] + return out + + +def wrapper_rank(f, p, pinv, q, qinv): + """Execute all six wrapper operations on every original input basis column.""" + columns, add, neg = [], f[2], f[4] + for column in range(8): + h0 = [int(column == i) for i in range(4)] + d0 = [int(column == i+4) for i in range(4)] + h, d = h0[:], d0[:] + d = [add[x][neg[y]] for x, y in zip(d, h)] + h, d = mv(f, p, d), mv(f, pinv, h) + d = [add[x][y] for x, y in zip(d, h)] + h, d = mv(f, q, d), mv(f, qinv, h) + d = [neg[x] for x in d] + d = [add[x][y] for x, y in zip(d, h)] + columns.append([add[x][neg[y]] for x, y in zip(h+d, d0+h0)]) + matrix = [[columns[j][i] for j in range(8)] for i in range(8)] + return eliminate(f, matrix)[0] + + +def parameter(f, signs, values): + two = f[2][1][1] + scaled = [f[3][f[3][two][signs[i//2]]][x] for i, x in enumerate(values)] + return perturbation(scaled) + + +def context(f, signs): + pchar, qsize = f[:2] + p = jordan_pair(f, signs) + pinv = eliminate(f, p, True)[2] + expected_rank = 0 if pchar == 2 else 2 + accepted, literal, rank_one = set(), 0, 0 + for values in product(range(qsize), repeat=4): + q = add_matrix(f, p, perturbation(values)) + actual = eliminate(f, error_block(f, p, q))[0] == expected_rank + if actual: + accepted.add(values) + expected = set() + for values in product(range(qsize), repeat=4): + s = [list(values[:2]), list(values[2:])] + if mm(f, s, s) != zero(2): + continue + r = parameter(f, signs, values) + expected.add(tuple(r[i][j] for i, j in ((0, 1), (0, 3), (2, 1), (2, 3)))) + require(accepted == expected, "complete coupling catalogue") + require(len(accepted) == (1 if pchar == 2 else qsize*qsize), "all-field count") + for values in sorted(accepted): + q = add_matrix(f, p, perturbation(values)) + _, determinant, qinv = eliminate(f, q, True) + require(determinant == 1, "determinant filter") + require(wrapper_rank(f, p, pinv, q, qinv) == expected_rank, "literal wrapper") + rank_one += eliminate(f, perturbation(values))[0] == 1 + literal += 1 + require(rank_one == len(accepted)-1, "perturbation rank distribution") + return {"q": qsize, "signs": signs, "candidates": qsize**4, + "optimal": len(accepted), "literal": literal, "rank_one": rank_one} + + +def binary_full_census(): + """Every binary second map, without the forced-support restriction.""" + f = field(2, 1, (0,)) + p = jordan_pair(f, (1, 1)) + optimal, invertible = 0, 0 + for bits in range(1 << 16): + q = [[(bits >> (4*i+j)) & 1 for j in range(4)] for i in range(4)] + if eliminate(f, q)[0] != 4: + continue + invertible += 1 + qinv = eliminate(f, q, True)[2] + actual = wrapper_rank(f, p, p, q, qinv) + require((actual == 0) == (q == p), "full-domain wrapper optimum") + optimal += actual == 0 + require(invertible == 20160 and optimal == 1, "full binary census") + return {"all_matrices": 65536, "invertible": invertible, "optimal": optimal} + + +def controls(): + f = field(3, 1, (0,)) + p = jordan_pair(f, (1, 1)) + pinv = eliminate(f, p, True)[2] + q = add_matrix(f, p, parameter(f, (1, 1), (0, 1, 0, 0))) + require(q != p, "coupling exists") + require(wrapper_rank(f, p, pinv, q, eliminate(f, q, True)[2]) == 2, "coupling optimum") + for values in ((1, 0, 0, 0), (0, 1, 1, 0)): + bad = add_matrix(f, p, parameter(f, (1, 1), values)) + require(wrapper_rank(f, p, pinv, bad, eliminate(f, bad, True)[2]) > 2, + "non-square-zero coupling rejection") + off_support = 0 + for i, j in product(range(4), repeat=2): + if i in (0, 2) and j in (1, 3): + continue + r = zero(4) + r[i][j] = 1 + bad = add_matrix(f, p, r) + require(eliminate(f, error_block(f, p, bad))[0] > 2, "support rejection") + off_support += 1 + f2 = field(2, 1, (0,)) + p2 = jordan_pair(f2, (1, 1)) + bad2 = add_matrix(f2, p2, perturbation((0, 1, 0, 0))) + require(wrapper_rank(f2, p2, p2, bad2, eliminate(f2, bad2, True)[2]) > 0, + "odd formula cannot transfer to characteristic two") + return {"non_square_zero": 2, "off_support": off_support, + "coupling_positive": 1, "characteristic_two_rejection": 1} + + +def main(): + presentations = ((2, 1, (0,)), (3, 1, (0,)), (2, 2, (1, 1)), + (5, 1, (0,)), (7, 1, (0,)), (2, 3, (1, 1, 0)), + (3, 2, (1, 0)), (11, 1, (0,)), (13, 1, (0,))) + cases = [] + for args in presentations: + f = field(*args) + check_field(f) + signs = sorted(set((1, f[4][1]))) + for pair in product(signs, repeat=2): + cases.append(context(f, pair)) + report = {"claim_type": "scoped proof with finite corroboration", "contexts": cases, + "binary_census": binary_full_census(), "controls": controls()} + package = Path(__file__).resolve().parent + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + report["package_sha256"] = {name: sha256((package/name).read_bytes()).hexdigest() for name in names} + print(json.dumps(report, sort_keys=True)) + print("PASS_COUPLED_RESONANT_JORDAN_PAIR no_new_kappa") + + +if __name__ == "__main__": + main()