diff --git a/research/paired-prefix-cut-capacity/PROOF.md b/research/paired-prefix-cut-capacity/PROOF.md new file mode 100644 index 0000000000..f1de1fef75 --- /dev/null +++ b/research/paired-prefix-cut-capacity/PROOF.md @@ -0,0 +1,198 @@ +# Sharp capacity change for a paired scalar ADD at a cut + +This proof was produced by Nick Petalas. New work is Apache-2.0. + +## Contract and statement + +Let D=Z[1/2]. Use the saturated helper-cut interface of Ali Romman's +PR5615. There are finitely many independent dirty scalar fields. A and B +are invertible matrices over D. Their complete endpoint BA is identity +on the helper support G and is an invertible map on its complement. +Keep the eligible coordinate support F, helper support G, and endpoint +BA fixed. There is no live owned field at the cut. + +The eligible row and column modules are + +```text +L(A) = {v supported in F : v A is supported in G}, +R(B) = {u supported in F : B u is supported in G}. +``` + +Pair full D-module bases by ordinary row-column multiplication. Let +c(A,B;F,G) be the largest size of a dyadic identity block obtainable by +left and right combinations of that pairing. The credited PR5615 +Smith theorem gives + +```text +c(K) = min_(odd primes p) rank_(F_p)(K mod p). +``` + +The minimum is attained. This includes a full-unit or empty pairing. +No predecessor capacity computation is needed for the result below. + +An elementary update x_i += a x_j, i != j and nonzero a in D, has matrix +T=I+a e_i e_j^t and inverse T^-1=I-a e_i e_j^t. Change the prefix and +suffix to + +```text +A' = T A, B' = B T^-1. +``` + +The inserted update is immediately before the nominated cut and its +inverse immediately after it, in these physical coordinates. The entire +dirty endpoint stays B'A'=BA. Then + +```text +|c(A',B';F,G) - c(A,B;F,G)| <= 1 if exactly one of i,j belongs to F, +c(A',B';F,G) = c(A,B;F,G) otherwise. +``` + +Both signs of the one-channel difference occur. For any finite sequence +of such paired edits, its total capacity change in absolute value is at +most the number of crossing updates in the prefix-side edit sequence. +That sequence bound is attained for every nonnegative integer count. + +The result concerns scalar elementary updates adjacent to a fixed cut. +An update inserted earlier inside a prefix becomes a generally dense +conjugate at the cut and is outside this elementary-update statement. + +## A one-row or one-column comparison + +Suppose a full pairing C gains at most one row to form K. Every old unit +block remains available by extending its row coefficients by zero, so +c(C)<=c(K). Choose an odd prime p attaining c(C). Adding a row raises +rank modulo p by at most one. Hence + +```text +c(C) <= c(K) <= c(C)+1. +``` + +The same argument applies to a column. This is a use of the credited +Smith criterion and ordinary rank subadditivity, not a new Smith theorem. + +## An update crossing out of the cut + +First suppose i belongs to F and j does not. For every column u supported +in F, u_j=0, so T^-1 u=u. Consequently R(B')=R(B). + +For a row v supported in F, v T=v+a v_i e_j^t. In particular v T=v +whenever v_i=0. Therefore the two left modules have exactly the same +coordinate-zero submodule + +```text +L0 = L(A) intersect {v_i=0} = L(A') intersect {v_i=0}. +``` + +The coordinate map v -> v_i identifies each quotient L(A)/L0 and +L(A')/L0 with a submodule of D. Such a submodule is free of rank at most +one, since D is a PID. The quotients are finitely generated, and their +short exact sequences split. A full basis of L0 therefore extends to a +full basis of either left module by at most one row. + +Pair these bases with one fixed full basis of R(B). The two pairing +matrices extend a common matrix C by at most one row each. By the +preceding comparison, both capacities belong to {c(C),c(C)+1}. Their +difference has absolute value at most one. This uses full saturated +modules; merely counting rational kernel dimensions would not suffice. + +## An update crossing into the cut + +Suppose i is outside F and j belongs to F. Every supported row v has +v_i=0, so v T=v and L(A')=L(A). On supported columns satisfying u_j=0, +T^-1 u=u. The common right submodule is thus + +```text +R0 = R(B) intersect {u_j=0} = R(B') intersect {u_j=0}. +``` + +Both right modules extend R0 by at most one basis column. The identical +one-column comparison proves the result in this orientation. + +## Updates within one side + +If i and j both belong to F, multiplication by T and T^-1 preserves the +row and column coordinate modules supported in F. Exactly + +```text +L(A') = L(A) T^-1, R(B') = T R(B). +``` + +Transport any two full bases accordingly. Their pairing is unchanged, +because (v T^-1)(T u)=v u. If both indices are outside F, T acts as the +identity on every supported row and column, so both modules themselves +are unchanged. These two cases prove invariance. Summing the per-edit +absolute differences proves the finite-sequence bound. + +## Sharpness with every dirty field restored + +Take two arbitrary fields x,z and F=G={x}. Use prefix x += z and its +inverse suffix x -= z. Thus + +```text +A = [[1,1],[0,1]], B = [[1,-1],[0,1]]. +``` + +The left eligibility equation is v_x=0, so L=0 and the old capacity is +zero. Insert x -= z immediately before the cut and x += z immediately +after it. Now A'=B'=I_2. Both eligible modules have basis e_x and pair +to [1], so the new capacity is one. The complete chronological word is + +```text +x += z; x -= z; CUT; x += z; x -= z. +``` + +It restores both arbitrary dirty inputs, and the x value at the new cut +is exactly its independent input value. Reversing the edit gives the +negative difference. For d disjoint pairs, take F=G to consist of every +x field. The original left constraint matrix is I_d, giving capacity +zero. All d paired edits give A'=B'=I_(2d), hence capacity d. There are +d crossing prefix-side updates, d matched suffix updates, 2d original +scalar updates and 4d total scalar updates in the edited identity word. +No extra storage is allocated. This proves sharpness for every d; it is +not a source-bound native construction or productive Gaussian invoice. + +## Exact finite corroboration + +The new verifier constructs fresh small prefixes and computes their full +eligible modules. It imports no predecessor executable. For at most three +coordinates, row reduction determines rational constraint rank. A rank-one +kernel is its primitive integral cross product or perpendicular vector. +For a single primitive constraint (a,b,c), write sa+tb=g=gcd(a,b) and +h=gcd(g,c). When g is nonzero the complete integer kernel has basis + +```text +(b/g,-a/g,0), (-sc/h,-tc/h,g/h). +``` + +Indeed the constraint forces z to be a multiple of g/h. Subtract the +corresponding multiple of the second vector; every remaining solution +has z=0 and is an integer multiple of the first vector. The g=0 case +has basis e_0,e_1. Localizing these full integer kernels at two gives +the full D-kernels, since a dyadic solution can have its denominator +cleared by a power of two. Thus no nonsaturated rational basis is +substituted for a module basis. + +The capacity oracle enumerates all minors and their integer gcds after +clearing dyadic denominators. A k-minor ideal is the whole dyadic ring +exactly when its nonzero integer gcd is a power of two. This is the +determinantal-divisor form of the cited criterion. Literal scalar +updates separately check the sharp family on arbitrary signed small +dirty states. The finite checks corroborate the universal written +argument; they do not prove it by extrapolation. + +## Scope and credit + +zxv's PR6064 posed the changed-prefix opening after proving the sharp +two-per-added-coordinate bound for fixed prefixes. Here the supports +are fixed and the program changes by paired elementary updates. Ali +Romman's PR5615 supplies saturated module capacity, with PR5602/5611/5599 +and the retained P104/native/controller lineage. Coordinate kernels, +module splitting over a PID, rank bounds and Bezout identities are +classical. No claim of general literature priority is made for them. + +No physical chart, timing, native-map, delivery, productive-target, +precision, storage, ownership, compiler or complete supplier cost is +established. A scalar ADD is not a recursive paid child. This theorem +does not imply a kappa ceiling or improve kappa. All five selected +framework assumptions retain their status. Independent human and +formal proof-kernel review are unclaimed. diff --git a/research/paired-prefix-cut-capacity/README.md b/research/paired-prefix-cut-capacity/README.md new file mode 100644 index 0000000000..d96b979b05 --- /dev/null +++ b/research/paired-prefix-cut-capacity/README.md @@ -0,0 +1,136 @@ +# One crossing paired scalar ADD changes cut capacity by at most one + +This contribution was produced by Nick Petalas. + +At a fixed dyadic helper cut, insert an elementary update immediately +before the cut and its inverse immediately after it. Keep both supports +and the complete dirty endpoint fixed. The exact unit-channel capacity +changes by at most one if the update crosses the cut's eligible coordinate +support. An update within either side preserves capacity exactly. + +```text +T = I + a e_i e_j^t, i != j, nonzero a in Z[1/2] +A' = T A, B' = B T^-1, B'A' = BA + +exactly one of i,j in F: |capacity' - capacity| <= 1 +both or neither in F: capacity' = capacity +``` + +The bound is sharp. For every d, an explicit 2d-field identity word gains +exactly d unit channels using d crossing prefix-side edits and their d +matched suffix edits. The original word uses 2d scalar ADDs; the edited +word uses 4d and restores every arbitrary dirty field. No extra storage +is allocated. Reversing an edit attains a decrease of one as well. + +Claim type: scoped written mathematical proof with exact finite +corroboration. No new kappa or selected-frontier change is claimed. +[PROOF.md](PROOF.md) proves the result over arbitrary finite dimensions. +It takes the changed-prefix opening in zxv's +[PR6064](https://github.com/CrocSwap/integer-mult-bounds/pull/6064). +That predecessor enlarges the cut support while keeping the program fixed; +this result keeps the supports fixed and changes the program. + +## Evidence and reproduction + +The new standalone checker imports no predecessor executable. It solves +full integer kernels in dimension at most three, localizes them at two, +and computes dyadic unit capacity by enumerating every minor gcd. +Normal and optimized warning-strict modes check: + +- 12,928 paired edits on 80 prefix instances, with every nonempty proper + cut/helper support in their two- and three-dimensional fixtures. + There are 4,032 same-side and 8,896 crossing edits. The capacity deltas + are -1 in 1,276 cases, zero in 11,625 and +1 in 27. +- All 52 determinant-one two-by-two matrices with entries in -2..2, + plus the 28 explicitly generated three-coordinate prefix instances + listed by `prefixes(3)`. Each edit uses coefficient -1/2 or +1/2. +- The sharp d=1,2,3,4 family, full module equations and unit witnesses, + with literal scalar execution on all 7,380 declared signed dirty states. +- Six invalid ADD rejections and six algebraic controls, including odd + nonunits, joint unit extraction, full kernel generation, a falsely + zero-change bound and the wrong inverse sign. + +From the worktree root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/paired-prefix-cut-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/paired-prefix-cut-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/paired-prefix-cut-capacity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/paired-prefix-cut-capacity --check-source-history +``` + +Substitute another CPython 3.12 interpreter path elsewhere. Direct checks +write nothing and emit `PASS_PAIRED_PREFIX_CUT_CAPACITY` in a generated +JSON receipt bound to all six package files and both declared source files. +There is no hand-written receipt. The registered hook runs both direct +commands separately with 60-second limits. + +## Scope and limitations + +The update must be elementary in the physical coordinates of the nominated +cut. An update inserted earlier inside the prefix generally becomes a dense +conjugate there; the one-channel statement does not cover that case. +Matched inverse suffix edits, fixed helper/cut supports and the full dirty +endpoint are essential hypotheses. Capacity is the algebraic unit-block +capacity of the full saturated modules, not rational rank alone. + +This changes `coverage-law-change` to a scalar algebraic side result. No +selected-word edit, common native chart, delivery, independent productive +Gaussian target, precision/growth, storage, ownership, compiler or complete +paid/target invoice is supplied. A scalar ADD is not a paid recursive child, +so this result supplies no kappa ceiling or supplier admission. All five +selected framework assumptions remain. Selected cold replay, Lean and Docker +were not run. Independent human and formal proof-kernel review are unclaimed. + +The selected binding orientation passed at conditional kappa .003125804. +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority +revision 8. [SOURCES.json](SOURCES.json) pins the two mathematical sources +and records selected/catalogue provenance. Existing source notices and bytes +are unchanged. Live PRs, latest handoffs, local reservations, current-main +object/formula searches, merged searches and recent account bodies were +checked. The initial cached local corpus was sparse; Git-tree searches and +materialized relevant sources supplemented it. Unpublished work and arbitrary +historical diffs remain outside coverage. The advance +[CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362888) +precedes the mathematical checks. + +## Open next questions + +1. What is the sharp capacity change for a dense conjugate of one earlier + prefix update? First pin the transport to the cut and compute both full + modules. The present elementary-update proof does not cover that change. +2. Can an actual native helper use a crossing paired update at a profitable + complete signed invoice? First extract one legal cut and prove its charts, + timing, dirty endpoints and delivery costs. Algebraic capacity supplies + none of those missing productive-target obligations. + +## Credit + +Credit zxv / PR6064 for the changed-prefix question and support-enlargement +predecessor, and Ali Romman / PR5615 for saturated cut-pairing capacity, +PR5602/5611/5599 and their retained P104/helper/native/controller lineage. +The related PR6054 pure-product result and Nick Petalas's earlier tensor, +parallel-bank and fixed-reader results leave this paired-edit contract open. +PR6308 changes only the predecessor determinant evaluator's runtime. +No predecessor theorem or numerical result is an audit deliverable here. +Module splitting, coordinate kernels, minor ideals and Bezout identities +are classical; no literature-wide priority is claimed for them. New work +is Apache-2.0. + +## Verifier constraints + +All functions are shorter than sixty physical lines. There is no recursion, +dynamic code loading, subprocess or network call. Matrices have order at +most eight, full kernel/minor calculations have order at most three, +prefix constructor words have at most four updates, sharp identity words +have at most sixteen, and source/package reads have a one-MiB cap. +Euclid has a 64-bit input cap and 192-iteration budget. +Every loop ranges over these fixed finite domains. Explicit exceptions +keep acceptance checks enabled under optimization. + +Power-of-ten rule 3 deviation: CPython allocates integers, Fractions and +containers during checking. The fixed fixture sizes bound live collections; +no static-allocation claim is made. Rule 9 uses ordinary fixed standard-library +iteration and local direct function calls. Warning-strict normal/optimized +replay and in-memory syntax compilation provide the local diagnostics; +no additional static analyzer or formal proof kernel is claimed. diff --git a/research/paired-prefix-cut-capacity/SOURCES.json b/research/paired-prefix-cut-capacity/SOURCES.json new file mode 100644 index 0000000000..ddd43596cd --- /dev/null +++ b/research/paired-prefix-cut-capacity/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/dyadic-cut-enlargement/README.md", + "usage": "input", + "git_blob": "312b56bc97647075f11e222d66705936279b6521", + "sha256": "0cb8510368768ba3428d41ed5133e03a29901d065f1b0da9000c032e610a0ad5" + }, + { + "path": "research/dyadic-helper-channel-capacity/PROOF.md", + "usage": "input", + "git_blob": "c97a6edce3070414c81f0ef6e6c099ebb17f3a90", + "sha256": "b258a217f2cd0fc48461285fe8ae24de26b0c5963668d9d8f0955fc6e759e929" + } + ] +} diff --git a/research/paired-prefix-cut-capacity/TASK.json b/research/paired-prefix-cut-capacity/TASK.json new file mode 100644 index 0000000000..53690662fd --- /dev/null +++ b/research/paired-prefix-cut-capacity/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "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": "Sharp unit-channel capacity change under elementary scalar prefix edits adjacent to a fixed cut, paired with inverse suffix edits; supports and complete dirty endpoint fixed.", + "scope_change_reason": "Takes the changed-prefix opening of zxv PR6064 rather than enlarging its support. This scalar algebraic side result does not establish the original card complete native invoice.", + "bottleneck_link": "Bounds the channels a local paired scalar edit can unlock before pricing native delivery and productive target credit; no scalar-to-recursive-cost conversion is asserted.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified sharp one-channel theorem and dirty-input attainer; no selected-word search or supplier expansion.", + "outcome": "completed", + "evidence": "PROOF.md universal argument; verify.py new full-module/minor checks and literal dirty sharpness states.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the sharp capacity change for a dense conjugate of one earlier prefix update?", + "why_it_matters": "An interior scalar update need not be elementary in the cut coordinates, so the present bound cannot price arbitrary prefix changes.", + "first_step": "Pin the transport from the update to the cut and compute the full eligible modules before and after one dense conjugate.", + "blocked_by": "No universal dense-edit capacity bound or physical source contract is supplied." + }, + { + "question": "Can an actual helper exploit a crossing paired update at a profitable complete signed invoice?", + "why_it_matters": "Algebraic unit capacity is not independent productive Gaussian target credit.", + "first_step": "Extract one legal native cut, its two scalar updates, full dirty endpoints, charts and delivery costs.", + "blocked_by": "Native realization, chronology, helper restoration and complete caller charges remain unproved." + } + ], + "claim_type": "scoped written mathematical proof with exact finite corroboration", + "question_source": { + "pr": 6064, + "author": "zxv", + "head": "5fd1fdedddf32307db31416958a1f03a8a67aa16", + "question": "Can changed prefixes or helper endpoints beat the fixed-program bound at a favorable complete invoice?" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362888", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library" + }, + "overlap": { + "open_prs": 406, + "discussion_records": 6353, + "local_notes_searched": 122, + "head_note_inventory": 8917, + "limits": "Initial local corpus was sparse. Main README Git-tree searches, relevant materialized packages, live PR titles/bodies and last-hour claims supplemented it; arbitrary historical diffs and unpublished work are outside coverage.", + "source6064_in_latest200_account_pr_bodies": 0, + "main_search_terms": [ + "capacity Lipschitz", + "transvection capacity", + "paired ADD", + "cross-cut", + "changed prefix", + "prefix edit" + ] + } +} diff --git a/research/paired-prefix-cut-capacity/VERIFY.json b/research/paired-prefix-cut-capacity/VERIFY.json new file mode 100644 index 0000000000..7c9f949fec --- /dev/null +++ b/research/paired-prefix-cut-capacity/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dyadic-cut-enlargement/README.md", + "research/dyadic-helper-channel-capacity/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New exact full-module paired-edit screen, same-side invariance, crossing bound, sharp dirty identity words, minor-gcd capacity and invalid-input controls; hash-bound stdout receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New exact full-module paired-edit screen, same-side invariance, crossing bound, sharp dirty identity words, minor-gcd capacity and invalid-input controls; hash-bound stdout receipt." + } + ] +} diff --git a/research/paired-prefix-cut-capacity/verify.py b/research/paired-prefix-cut-capacity/verify.py new file mode 100644 index 0000000000..0f11a14131 --- /dev/null +++ b/research/paired-prefix-cut-capacity/verify.py @@ -0,0 +1,303 @@ +"""Exact paired-prefix cut checks. Nick Petalas. Apache-2.0.""" +from fractions import Fraction as Q +from itertools import combinations, permutations, product +from math import gcd, lcm +from pathlib import Path +import hashlib +import json + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def eye(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def mm(a, b): + return [[sum(x * y for x, y in zip(row, col)) + for col in zip(*b)] for row in a] + + +def add_matrix(n, dst, src, coefficient): + need(type(n) is int and 2 <= n <= 8, "matrix dimension") + need(type(dst) is int and type(src) is int and + 0 <= dst < n and 0 <= src < n and dst != src, "distinct roles") + c = Q(coefficient) + need(c and c.denominator & (c.denominator - 1) == 0 and + max(abs(c.numerator).bit_length(), c.denominator.bit_length()) <= 16, + "bounded nonzero dyadic coefficient") + a = eye(n) + a[dst][src] = c + return a + + +def rref(a, width): + need(0 <= width <= 3 and len(a) <= 3, "kernel dimension") + need(all(len(row) == width for row in a), "constraint shape") + a = [[Q(x) for x in row] for row in a] + pivots = [] + for col in range(width): + row = next((i for i in range(len(pivots), len(a)) if a[i][col]), None) + if row is None: + continue + k = len(pivots) + a[k], a[row] = a[row], a[k] + scale = a[k][col] + a[k] = [x / scale for x in a[k]] + for i in range(len(a)): + if i != k: + scale = a[i][col] + a[i] = [x - scale * y for x, y in zip(a[i], a[k])] + pivots.append(col) + return a, pivots + + +def primitive(row): + scale = lcm(*(Q(x).denominator for x in row)) + values = [int(scale * x) for x in row] + divisor = gcd(*values) + need(divisor != 0, "nonzero primitive row") + return [x // divisor for x in values] + + +def bezout(a, b): + need(max(abs(a).bit_length(), abs(b).bit_length()) <= 64, "Bezout size") + old_r, r, old_s, s, old_t, t = abs(a), abs(b), 1, 0, 0, 1 + for _ in range(192): + if not r: + u = old_s if a >= 0 else -old_s + v = old_t if b >= 0 else -old_t + need(u * a + v * b == old_r, "Bezout identity") + return old_r, u, v + q = old_r // r + old_r, r = r, old_r - q * r + old_s, s = s, old_s - q * s + old_t, t = t, old_t - q * t + raise ValueError("Bezout iteration budget exhausted") + + +def cross(a, b): + return [a[1] * b[2] - a[2] * b[1], + a[2] * b[0] - a[0] * b[2], + a[0] * b[1] - a[1] * b[0]] + + +def kernel(a, width): + """Rows forming the full integer kernel, hence its full dyadic localization.""" + reduced, pivots = rref(a, width) + rank = len(pivots) + if not rank: + return eye(width) + if rank == width: + return [] + first = primitive(reduced[0]) + if width == 2: + result = [[-first[1], first[0]]] + elif rank == 2: + result = [primitive(cross(first, primitive(reduced[1])))] + else: + a0, b0, c0 = first + g, s, t = bezout(a0, b0) + if not g: + result = [[1, 0, 0], [0, 1, 0]] + else: + h = gcd(g, c0) + result = [[b0 // g, -a0 // g, 0], + [-s * (c0 // h), -t * (c0 // h), g // h]] + need(all(not any(sum(x * y for x, y in zip(row, v)) for row in a) + for v in result), "kernel equations") + need(len(rref(result, width)[1]) == width - rank, "kernel rank") + return result + + +def determinant(a): + n = len(a) + need(n <= 3 and all(len(row) == n for row in a), "minor dimension") + total = Q(0) + for p in permutations(range(n)): + inversions = sum(p[i] > p[j] for i in range(n) for j in range(i + 1, n)) + term = Q((-1) ** inversions) + for i in range(n): + term *= a[i][p[i]] + total += term + return total + + +def capacity(a): + """Determinantal-divisor oracle, without predecessor executable imports.""" + m, n = len(a), len(a[0]) if a else 0 + need(m <= 3 and n <= 3 and all(len(row) == n for row in a), "pairing size") + scale = max((Q(x).denominator for row in a for x in row), default=1) + need(all(Q(x).denominator & (Q(x).denominator - 1) == 0 + for row in a for x in row), "dyadic pairing") + integer = [[int(scale * x) for x in row] for row in a] + count = 0 + for k in range(1, min(m, n) + 1): + divisor = 0 + for rows in combinations(range(m), k): + for cols in combinations(range(n), k): + value = determinant([[integer[i][j] for j in cols] for i in rows]) + need(value.denominator == 1, "integer minor") + divisor = gcd(divisor, int(value)) + if not divisor or divisor & (divisor - 1): + break + count = k + return count + + +def cut_data(a, b, f, g): + n = len(a) + outside = [j for j in range(n) if j not in g] + left = kernel([[a[i][j] for i in f] for j in outside], len(f)) + right = kernel([[b[j][i] for i in f] for j in outside], len(f)) + pairing = [[sum(x * y for x, y in zip(v, u)) for u in right] for v in left] + return capacity(pairing) + + +def word(n, operations): + a = b = eye(n) + for dst, src, c in operations: + a = mm(add_matrix(n, dst, src, c), a) + b = mm(b, add_matrix(n, dst, src, -c)) + need(mm(a, b) == mm(b, a) == eye(n), "complete dirty endpoint") + return a, b + + +def prefixes(n): + if n == 2: + result = [] + for values in product(range(-2, 3), repeat=4): + a, b, c, d = values + if a * d - b * c == 1: + result.append(([[a, b], [c, d]], [[d, -b], [-c, a]])) + return result + operations = [(i, j, c) for i in range(3) for j in range(3) + if i != j for c in (-1, 1)] + result = [word(3, [])] + result.extend(word(3, [op]) for op in operations) + result.extend(word(3, [op, operations[(i + 3) % 12]]) + for i, op in enumerate(operations)) + for c in (2, 3, 5): + result.append(word(3, [(0, 2, 1), (1, 2, c), (2, 0, 1), (2, 1, c)])) + return result + + +def screen(): + counts = {"prefix_instances": 0, "edits": 0, "same_side": 0, + "crossing": 0, "delta_minus_one": 0, "delta_zero": 0, + "delta_plus_one": 0} + delta_keys = {-1: "delta_minus_one", 0: "delta_zero", 1: "delta_plus_one"} + for n in (2, 3): + cases = prefixes(n) + counts["prefix_instances"] += len(cases) + for a, b in cases: + need(mm(a, b) == mm(b, a) == eye(n), "prefix inverse") + for fm in range(1, (1 << n) - 1): + f = [i for i in range(n) if fm >> i & 1] + for gm in range(1, (1 << n) - 1): + g = [i for i in range(n) if gm >> i & 1] + old = cut_data(a, b, f, g) + for dst in range(n): + for src in range(n): + if dst == src: + continue + for c in (Q(-1, 2), Q(1, 2)): + aa = mm(add_matrix(n, dst, src, c), a) + bb = mm(b, add_matrix(n, dst, src, -c)) + need(mm(bb, aa) == eye(n), "paired edit endpoint") + delta = cut_data(aa, bb, f, g) - old + crossing = (dst in f) != (src in f) + need(abs(delta) <= int(crossing), "paired ADD bound") + counts["edits"] += 1 + counts["crossing" if crossing else "same_side"] += 1 + counts[delta_keys[delta]] += 1 + need(counts["edits"] == counts["crossing"] + counts["same_side"], "coverage") + return counts + + +def sharpness(): + cases = 0 + for d in range(1, 5): + n = 2 * d + operations = [(2 * i, 2 * i + 1, 1) for i in range(d)] + a, b = word(n, operations) + f = list(range(0, n, 2)) + z = list(range(1, n, 2)) + # Old left constraints are I_d, so L=0. New constraints vanish. + need([[a[i][j] for i in f] for j in z] == eye(d), "old zero module") + need(all(not b[j][i] for j in z for i in f), "old full right module") + t, ti = word(n, [(dst, src, -c) for dst, src, c in operations]) + aa, bb = mm(t, a), mm(b, ti) + need(aa == bb == eye(n), "attaining paired edits") + need([[sum(aa[i][k] * bb[k][j] for k in range(n)) + for j in f] for i in f] == eye(d), "attaining full unit block") + for values in product((-1, 0, 1), repeat=n): + state = list(values) + inverse = [(dst, src, -c) for dst, src, c in reversed(operations)] + for dst, src, c in operations + inverse: + state[dst] += c * state[src] + need(state == list(values), "attaining cut value") + for dst, src, c in operations + inverse: + state[dst] += c * state[src] + need(state == list(values), "four-pass dirty restoration") + cases += 1 + return cases + + +def controls(): + bad = [(1, 0, 0, 1), (2, 0, 0, 1), (2, -1, 1, 1), + (2, 0, 1, 0), (2, 0, 1, Q(1, 3)), (9, 0, 1, 1)] + for args in bad: + try: + add_matrix(*args) + except ValueError: + continue + raise ValueError("invalid ADD accepted") + need(capacity([[21]]) == 0 and capacity([[Q(1, 4)]]) == 1, "unit status") + need(capacity([[3, 0], [0, 5]]) == 1, "joint unit without unit entry") + need(kernel([[6, 10, 15]], 3) == [[5, -3, 0], [-30, 15, 2]], + "full rank-two integer kernel") + a, b = word(2, [(0, 1, 1)]) + need(cut_data(a, b, [0], [0]) == 0, "old sharpness capacity") + need(cut_data(eye(2), eye(2), [0], [0]) == 1, "zero-change mutant rejects") + t = add_matrix(2, 0, 1, -1) + need(mm(mm(b, t), mm(t, a)) != eye(2), "wrong inverse sign rejects") + return len(bad) + 6 + + +def source_hashes(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + hashes = {} + for row in pins["files"]: + if row["usage"] == "input": + path = ROOT / row["path"] + need(path.stat().st_size <= 1024 * 1024, "source size") + digest = hashlib.sha256(path.read_bytes()).hexdigest() + need(digest == row["sha256"], "source hash: " + row["path"]) + hashes[row["path"]] = digest + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + path = HERE / name + need(path.stat().st_size <= 1024 * 1024, "package file size") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def main(): + hashes = source_hashes() + result = screen() + result["dirty_states"] = sharpness() + result["controls"] = controls() + result["status"] = "PASS_PAIRED_PREFIX_CUT_CAPACITY" + result["file_sha256"] = hashes + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()