From ea5a00d0e3a706eef4a07788f8fe68e1c92c7334 Mon Sep 17 00:00:00 2001 From: ywz65 <154373401+ywz65@users.noreply.github.com> Date: Thu, 15 Oct 2026 08:31:03 -0700 Subject: [PATCH] Prove the signed integer-address SWAP tariff --- .../PREDECESSORS.json | 14 + research/integer-address-signed-swap/PROOF.md | 166 ++++++++++ .../integer-address-signed-swap/README.md | 87 ++++++ .../integer-address-signed-swap/RESULT.json | 22 ++ .../integer-address-signed-swap/SOURCES.json | 31 ++ .../integer-address-signed-swap/TASK.json | 95 ++++++ .../integer-address-signed-swap/VERIFY.json | 34 +++ .../predecessor-2544.md | 181 +++++++++++ .../test_boundary.py | 81 +++++ .../integer-address-signed-swap/verify.py | 287 ++++++++++++++++++ 10 files changed, 998 insertions(+) create mode 100644 research/integer-address-signed-swap/PREDECESSORS.json create mode 100644 research/integer-address-signed-swap/PROOF.md create mode 100644 research/integer-address-signed-swap/README.md create mode 100644 research/integer-address-signed-swap/RESULT.json create mode 100644 research/integer-address-signed-swap/SOURCES.json create mode 100644 research/integer-address-signed-swap/TASK.json create mode 100644 research/integer-address-signed-swap/VERIFY.json create mode 100644 research/integer-address-signed-swap/predecessor-2544.md create mode 100644 research/integer-address-signed-swap/test_boundary.py create mode 100644 research/integer-address-signed-swap/verify.py diff --git a/research/integer-address-signed-swap/PREDECESSORS.json b/research/integer-address-signed-swap/PREDECESSORS.json new file mode 100644 index 0000000000..ad536e7746 --- /dev/null +++ b/research/integer-address-signed-swap/PREDECESSORS.json @@ -0,0 +1,14 @@ +{ + "schema_version": 1, + "files": [ + { + "path": "research/integer-address-signed-swap/predecessor-2544.md", + "usage": "input", + "git_blob": "e4647abcd7056dd205252f8d1e4d20368df66c9d", + "sha256": "bd9e1a3346adbb8b99a30eaa2819006760adff5258f629b2ffc628cc397e93c4", + "source_commit": "9fb1552f12ca4777ca660461a8b602e709285f99", + "source_path": "research/gl2-swap-weighted-tariff/README.md", + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2544" + } + ] +} diff --git a/research/integer-address-signed-swap/PROOF.md b/research/integer-address-signed-swap/PROOF.md new file mode 100644 index 0000000000..131921a8ec --- /dev/null +++ b/research/integer-address-signed-swap/PROOF.md @@ -0,0 +1,166 @@ +# Integer address SWAPs need a separately charged sign + +## Exact model + +Work in `M_R(F2[GL2(Z)])`. Each of the R scalar roles is an arbitrary dirty +binary stream. Address matrices act on its two integer coordinates; a NEG +below negates one **address coordinate**, not a binary payload value. +The paid labels are + +``` +a+ = [1 1;0 1], a- = [1 -1;0 1], +b+ = [1 0;1 1], b- = [1 0;-1 1], +nx = [-1 0;0 1], ny = [1 0;0 -1]. +``` + +For any binary rank-one idempotent `N=uv^T`, with `v^T u=1`, a call is +`D_N(g)=I_R+([g]+1)N`. The prices of a+/a- are A, those of b+/b- are B, +and those of nx/ny are C. A,B,C are fixed nonnegative real numbers, +independent of role count, projector, state and word position. Arbitrary +scalar GL_R(F2) operations may be interleaved for free. No other address +map, clean input, reset, erasure, higher-rank paid unit or free restoration +is provided. Every actual inverse call is charged. + +Let r roles have any mixture of the four signed anti-diagonal targets + +``` + S=[0 1;1 0], -S=[0 -1;-1 0], + J=[0 1;-1 0], -J=[0 -1;1 0]. +``` + +Let t of them be S or -S (determinant -1). The other r-t targets are J or +-J (determinant +1). The complete endpoint is their diagonal direct sum, +with identity on all R-r spectators and every off-diagonal coupling zero. +Assume finite R>=r>=0. Equality is coefficientwise in the full formal group +algebra, not equality only after applying a nonfaithful representation. + +**Theorem.** The exact minimum price is + +``` + r*(2*min(A,B)+max(A,B)) + t*C. +``` + +At unit prices, this is 4t+3(r-t). The zero-target case is the empty word. +This is a sharp tariff in this specified relaxation, not a physical tape +invoice, primitive elapsed time, recursive supplier or new exponent. + +## The credited ADD bounds survive the integer extension + +Reduction modulo2 is a group homomorphism `GL2(Z) -> GL2(F2)`. Both signs of +a shear have the same image; nx and ny have identity image. All four targets +map to coordinate SWAP. The induced group-algebra map preserves a formal +identity and the scalar projectors, while deleting every address NEG call. + +Thus PR2544's credited individual crossing bounds and PR2415/PR1989's total +bound apply to the remaining word, with the same arbitrary scalar mixing +and restored dirty spectators: + +``` + n_a >= r, n_b >= r, n_a+n_b >= 3r. (1) +``` + +For clarity, each individual bound uses the upper/lower crossing block of +the natural two-dimensional representation. In address-major order, a paid +a has image `[I N;0 I]`, a paid b has `[I 0;N I]`, scalar mixing is block +diagonal, and each target has both crossing ranks one per target role. + +The total bound acts on the three nonzero binary vectors, ordered +`(1,0),(1,1),(0,1)`. a and b are the two adjacent transpositions. Their +action on ordered distinct pairs splits increasing and decreasing pairs: +each paid shear has crossing rank one; SWAP has crossing rank three. +This is the predecessor's ordered-pair argument, not a new proof principle. + +All these crossing ranks are subadditive because for a fixed decomposition +`(UV)_12=U_11 V_12+U_12 V_22`, hence `rank((UV)_12)` is at most the sum of +the two crossing ranks. No intermediate triangularity or commuting +projectors are assumed. + +## A disjoint determinant-character charge + +Take the homomorphism `det:GL2(Z)->{+1,-1}`, then its two-point permutation +representation over F2. The +1 element acts as I2, while -1 swaps the two +sheets. Extend it linearly to the full group algebra and tensor with roles. + +Every ADD has identity image, hence crossing rank zero. Every paid address +NEG has image `[I+N N;N I+N]`, whose crossing block N has rank one. Free +scalar mixing is `[Q 0;0 Q]` and crosses zero. At the endpoint, exactly the +t negative-determinant targets exchange sheets, with crossing rank t. +The same subadditivity therefore proves + +``` + n_NEG >= t. (2) +``` + +This is a separate necessary inequality. The ADD cuts charge no NEGs, and +the determinant cut charges no ADDs. Summing their weighted consequences +does not charge one instruction twice. In particular, even when an even +number of target swaps has overall determinant +1, its block crossing rank +is t rather than merely the parity of t. Scalar role mixing cannot hide it. + +For A<=B, (1) gives +`A*n_a+B*n_b=A*(n_a+n_b)+(B-A)*n_b >= r*(2A+B)`. +The other ordering is symmetric. Adding C times (2) proves the lower bound, +including zero prices. Negative prices are excluded substantively: for R>=1, +a paid label followed by its charged inverse is a formal identity loop; +if its price is negative, arbitrary repetitions make the cost unbounded below. + +## Literal integer attaining words + +Use left-to-right matrix multiplication in the displayed words. Direct +integer multiplication gives + +``` +J = a+ b- a+ = b- a+ b-, +-J = a- b+ a- = b+ a- b+, +S = J nx, -S = J ny. +``` + +Choose the cheaper three-shear orientation for each target and append the +one indicated NEG exactly for negative-determinant targets. On role j use +N=E_jj. Each factor changes only that role, so the full formal product has +exactly the prescribed monomial there and identity elsewhere. Concatenating +over r roles attains (1) and (2) jointly. It needs no extra role, scalar +preparation, inter-role copying or uncharged restoration. This verifies the +entire dirty endpoint, not only a natural-representation image. + +## Uniform address realization and its boundary + +Each attaining integer matrix word reduces to the same signed permutation +on `(Z/MZ)^2` for every M>=2. Every label is a unit coordinate ADD or address +NEG; neither whole-SWAP nor free coordinate relabeling is an extra paid label. +This supplies literal uniform upper identities, not their physical compiler, +prefix/suffix layout, word representation or recursively weighted cost. + +The lower bound is for formal GL2(Z) identities, equivalently for a fixed +finite word that realizes the complete stream endpoint on integer addresses. +To see faithfulness of the latter implication, for any finite set of distinct +integer matrices choose v=(1,z) outside the finitely many collision values +of z. Each nonzero matrix difference kills at most one such v. The distinct +images then separate all coefficients of every finite group-algebra entry. +The same separation survives reduction modulo any sufficiently large M, +since a fixed finite list of nonzero integer differences cannot all vanish +modulo arbitrarily large M. Thus a fixed finite word valid at every modulus +in an unbounded family also satisfies the formal identity. + +This is **not** a lower bound for every separately optimized word at one +finite modulus. At M=2, both address NEG labels become identity and J=S, +so three shears already swap coordinates. Nor does the theorem establish +admission for width-dependent alphabets, varying coefficient labels, changing +role counts, restricted input subspaces or incomplete spectator restoration. + +The quotient images are lower-bound witnesses only. For example a+ squared +is a nonidentity integer matrix with identity image in both the mod2 and +determinant quotients. Adding `[I]+[(a+)^2]` to an endpoint entry is therefore +invisible to all four cuts but changes the full formal map. The verifier +uses exact formal coefficients for endpoints and checks this control. + +## Credit + +PR2544 at `9fb1552f12ca4777ca660461a8b602e709285f99` supplies the asymmetric +GL2(F2) tariff and its individual label counts, crediting Aaron Wang's +PR2444 handoff and Ross Richardson's PR1989/PR2415 total crossing bound. +Those bounds and standard rank subadditivity are reused, not claimed new. +The contribution is their source-bound integer-address extension with a +separately paid determinant-sign requirement, mixed signed endpoints and +the explicit finite-modulus boundary. Prepared for ywz65 with substantial +OpenAI Codex assistance, Apache-2.0. No human or formal-kernel review claimed. diff --git a/research/integer-address-signed-swap/README.md b/research/integer-address-signed-swap/README.md new file mode 100644 index 0000000000..2ca4939c17 --- /dev/null +++ b/research/integer-address-signed-swap/README.md @@ -0,0 +1,87 @@ +# Price address signs in uniform integer SWAP words + +For any mixture of `r` signed anti-diagonal targets in formal +`F2[GL2(Z)]`, with `t` of determinant -1, the exact minimum price is + +``` +r*(2*min(A,B)+max(A,B)) + t*C. +``` + +Here the two unit shear orientations, with either sign, cost A and B; +negating either **address coordinate** costs C. Prices are nonnegative. +All R>=r roles begin arbitrarily, scalar `GL_R(F2)` mixing is free, and all +spectators and off-diagonal couplings must be restored. A paid unit acts on +one binary rank-one scalar idempotent, not an arbitrary-rank block. +At unit prices, SWAP and minus-SWAP cost four each; the two determinant-positive +quarter turns cost three each. A binary payload sign is not an address NEG. + +[PROOF.md](PROOF.md) gives the all-R, all-target, all-nonnegative-price theorem. +The inherited mod2 ADD cuts give `n_a>=r`, `n_b>=r`, `n_a+n_b>=3r`. +A separate two-sheet determinant representation gives `n_NEG>=t`: even when +t is even, the crossing rank sees t, not just its parity. The charges are +disjoint. Literal signed three-shear words, with one NEG where needed, attain +all inequalities together on complete formal endpoints. + +This extends [PR2544](https://github.com/CrocSwap/integer-mult-bounds/pull/2544) +at `9fb1552f12ca4777ca660461a8b602e709285f99`; its asymmetric mod2 tariff is +credited, not rediscovered. That predecessor credits Aaron Wang's PR2444 +handoff and Ross Richardson's PR1989 general ordered-pair cut and PR2415 +coordinate-SWAP bridge. Its unchanged README is retained as +[predecessor-2544.md](predecessor-2544.md) for source-bound review; no source +implementation is imported. [PREDECESSORS.json](PREDECESSORS.json) pins it; +[SOURCES.json](SOURCES.json) pins the unchanged main ordered-pair proof, +with SHA-256 and Git blob IDs. + +## Domain boundary + +Formal equality is also forced by a **fixed finite word** valid on full integer +streams, or at every modulus in an unbounded family; the proof supplies the +finite-support separation argument. The attaining identities work modulo +every M>=2. The lower bound does **not** apply to every word optimized +separately at a fixed finite M. At M=2 address NEG is identity and three shears +already implement SWAP. Restricted clean inputs, width-dependent alphabets, +higher-rank units, free address maps and incomplete restoration are outside +the model. No physical tape compiler, completed recursive supplier, selected +frontier change or integer-multiplication theorem follows. + +## Reproduce and evidence + +Python 3.12+, standard library, from the repository root: + +```sh +python3 -I -O -B research/integer-address-signed-swap/verify.py +python3 -I -O -B research/integer-address-signed-swap/test_boundary.py +python3 scripts/research_package.py --package research/integer-address-signed-swap +``` + +The fixed [RESULT.json](RESULT.json) records 930 rank-one paid-factor cut checks +(all binary projectors for R=1..4), 20 free scalar factors, 1,364 complete formal +endpoints (every mixture of up to four targets, two orientations and zero/one +spectator), 42,625 exact rational price checks and 720 deterministic mixed +paid/free prefixes. These bounded checks support the written proof; they are +not an exhaustive word search or a proof assistant formalization. + +Controls detect an omitted NEG invisible to mod2 cuts, a nonzero formal +perturbation invisible to **all** quotient representations, fourteen deleted +attaining calls and a nonidempotent projector. Separate controls exhibit the +M=2 exception, negative-price identity loops and the changed higher-rank-unit +premise. Six subprocess tests check unchanged Git-free exports, source drift, +missing sources/receipt, typed receipt drift and exclusive regeneration. + +Verification is read-only. `--write-result NEW_PATH` regenerates a complete +receipt and refuses an existing path. Explicit failures remain active under +`-O`. Runtime provenance and independent AI review are recorded with delivery; +hosted CI and independent human review are not asserted. + +## Open next questions + +1. Establish a lower bound for one named physical finite-modulus family at its + actual widths. Start by pinning the native alphabet and proving its action + faithful on the allowed word supports; M=2 blocks an unconditional transfer. +2. Price the literal signed words in a legal tape representation. Start with + all ADD/NEG calls, temporary roles and restoration; native compilation, + all-size layout and recursive eligibility remain blockers. + +The structured obligations and original picker scope change are in +[TASK.json](TASK.json). Contributor: ywz65 with substantial OpenAI Codex +assistance. Apache-2.0; predecessor attribution is retained. diff --git a/research/integer-address-signed-swap/RESULT.json b/research/integer-address-signed-swap/RESULT.json new file mode 100644 index 0000000000..9258b6d6af --- /dev/null +++ b/research/integer-address-signed-swap/RESULT.json @@ -0,0 +1,22 @@ +{ + "all_register_proof": "PROOF.md", + "claim_kind": "finite_checks_for_scoped_proof", + "controls": { + "all_quotients_miss_nonzero_formal_perturbation": true, + "finite_modulus_two_breaks_formal_lower_bound": true, + "fourteen_deleted_attainer_calls_rejected": true, + "higher_rank_unit_would_change_model": true, + "nonidempotent_projector_rejected": true, + "omitted_neg_detected_only_by_sign_cut": true, + "six_negative_price_identity_loops": true + }, + "exact_rational_price_cases": 42625, + "formula": "r*(2*min(A,B)+max(A,B))+t*C", + "free_scalar_factor_cases": 20, + "full_formal_endpoint_cases": 1364, + "mixed_word_prefix_cases": 720, + "new_selected_exponent": false, + "rank_one_paid_factor_cases": 930, + "schema_version": 1, + "source_files": 3 +} diff --git a/research/integer-address-signed-swap/SOURCES.json b/research/integer-address-signed-swap/SOURCES.json new file mode 100644 index 0000000000..51118b0d01 --- /dev/null +++ b/research/integer-address-signed-swap/SOURCES.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/symmetric-adjacent-cut-bound/README.md", + "usage": "input", + "git_blob": "cdb3f431acc07b4a75abdd3998093fd68d9a498f", + "sha256": "4fb453c83d7cd15a93fc7c65b82f2f67cb609a31285ac9ebd1f44b675777d154" + }, + { + "path": "research/symmetric-adjacent-cut-bound/PROOF.md", + "usage": "input", + "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d", + "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50" + } + ], + "retained_source_note": "Only the cited predecessor README is retained for Git-free review, unchanged with its credit and Apache-2.0 notice; no predecessor implementation is imported." +} diff --git a/research/integer-address-signed-swap/TASK.json b/research/integer-address-signed-swap/TASK.json new file mode 100644 index 0000000000..c0a5766699 --- /dev/null +++ b/research/integer-address-signed-swap/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp mixed signed anti-diagonal tariff in formal F2[GL2(Z)] with separately paid address NEGs, arbitrary free scalar GL_R mixing and restored dirty spectators.", + "scope_change_reason": "The first working example was read and baseline bindings passed. Changing the address group from finite binary matrices to integer matrices and adding charged address sign changes exposes a sign obligation invisible in the existing mod2 SWAP cuts; this is not another register-count census.", + "bottleneck_link": "A complete primitive needs its address signs and restoration charged. This closes that obligation in the specified relaxation only; native suppliers and the selected exponent are unchanged.", + "budget_minutes": 60, + "stop_rule": "One scoped proof, full formal attaining endpoints and negative controls; stop rather than claim arbitrary finite-modulus or physical eligibility.", + "outcome": "completed", + "evidence": "PROOF.md, verify.py, RESULT.json, test_boundary.py and retained source pins.", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate AI review; no human or proof-assistant review claimed.", + "selector_seed": "0f0808b71b0d13f33a0de3e1e61c03b1", + "open_questions": [ + { + "question": "Can a named finite-modulus physical address implementation admit the same lower bound at its actual widths?", + "why_it_matters": "The formal integer lower bound cannot be silently transferred to separately optimized finite-width words.", + "first_step": "Pin one modulus family and prove a faithful action for the actual allowed label-word support before claiming a tariff.", + "blocked_by": "A source-specific finite-address faithfulness or separate lower-bound witness; M=2 is a counterexample to unrestricted transfer." + }, + { + "question": "What is the full physical invoice for the literal signed three-shear words and their address NEG?", + "why_it_matters": "An exact relaxed tariff alone supplies no recursive BIT supplier improvement.", + "first_step": "Select one legal tape/address representation and charge every ADD, NEG, temporary and restored role.", + "blocked_by": "A native compiler, all-size layout and completed recursive eligibility proof." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2544#issuecomment-6195288484", + "overlap": "Task helper plus complete cached 679-PR and 1197 Discussion/comment/reply metadata snapshot; fresh recent PR bodies and source2544 comments checked before claiming. Discussion coverage remains stale after 2026-10-15T12:29:05Z and is not a novelty guarantee.", + "upstream_refresh": { + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "selected_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "time_utc": "2026-10-15T15:04:00Z" + }, + "nearest_predecessors": [ + "PR2544 9fb1552f12ca4777ca660461a8b602e709285f99 ywz65, sharp asymmetric mod2 tariff; reused and credited", + "PR1989 Ross Richardson, symmetric adjacent ordered-pair cut on canonical main", + "PR2415 Ross Richardson, coordinate-SWAP specialization credited through2544", + "PR2444 Aaron Wang, weighted tariff handoff credited through2544" + ], + "limits": [ + "Formal/uniform integer stream identities; no per-modulus optimized-word lower bound", + "No physical compiler, supplier, recursive invoice or new exponent" + ], + "submission_refresh": { + "time_utc": "2026-10-15T15:29:19.595750+00:00", + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "source_head": "9fb1552f12ca4777ca660461a8b602e709285f99", + "priority_revision": 4, + "compatibility": "Canonical main unchanged from original base; scientific source pins unchanged." + } +} diff --git a/research/integer-address-signed-swap/VERIFY.json b/research/integer-address-signed-swap/VERIFY.json new file mode 100644 index 0000000000..d467879ce5 --- /dev/null +++ b/research/integer-address-signed-swap/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/symmetric-adjacent-cut-bound/README.md", + "research/symmetric-adjacent-cut-bound/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Full formal integer group-algebra endpoints, four cut charges, sampled mixed prefixes, rational tariffs and model-boundary controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_boundary.py" + ], + "timeout_seconds": 120, + "checks": "Git-free read-only replay, exact source and typed receipt corruption, exclusive regeneration" + } + ] +} diff --git a/research/integer-address-signed-swap/predecessor-2544.md b/research/integer-address-signed-swap/predecessor-2544.md new file mode 100644 index 0000000000..e4647abcd7 --- /dev/null +++ b/research/integer-address-signed-swap/predecessor-2544.md @@ -0,0 +1,181 @@ +# Sharp asymmetric label tariffs for coordinate SWAP + +In the formal coordinate-SWAP model, assign fixed nonnegative real prices A and B +to the two paid labels a and b. For t target roles and any finite `R >= t` +arbitrary-input roles, the exact minimum is + +```text + t * (2 min(A,B) + max(A,B)). +``` + +This closes Open next questions item 2 of Aaron Wang's +[PR2444](https://github.com/CrocSwap/integer-mult-bounds/pull/2444), which proposed +weighted BFS for t=2,3. No further search is required for that tariff change: +even arbitrary noncommuting projectors and restored dirty spectators cannot +beat the cheaper of independent `aba` and `bab` words. + +The total-call bound `3t` and its general cut argument are **inherited**, credited +to Ross Richardson's [PR1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989) +and its explicit coordinate-SWAP corollary +[PR2415](https://github.com/CrocSwap/integer-mult-bounds/pull/2415). +The additional result here is the two individual label counts and their sharp +weighted combination, with exact zero-price and changed-premise boundaries. +This is a scoped formal-model theorem, not a new native supplier or exponent. + +## Model + +Work in `F2[G]` for `G=GL_2(F2)`, with + +```text +a = [1 1] b = [1 0] s = aba = bab = [0 1]. + [0 1] [1 1] [1 0] +``` + +Every paid factor is `D_N(g) = I_R + ([g]+1) N`, where g is exactly a or b +and `N=uv^T` is a binary rank-one idempotent (`v^T u=1`). Its price is A or B, +independently of N, position, R and the surrounding word. Arbitrary scalar +`GL_R(F2)` maps may be interleaved for free. There are no additional free address +maps, clean allocations, resets, erasures or copies. Every role begins arbitrarily. +The endpoint is coefficientwise equality with +`diag([s] I_t, I_(R-t))`; every spectator is individually restored, with no +off-diagonal residual. Spectators may be reused arbitrarily during the word. +These are exactly PR2415's model hypotheses; only the two label prices change. +For t=0 the empty word attains zero; all statements allow A=0 and/or B=0. + +## The two per-label bounds + +Apply the natural two-dimensional representation linearly to the group algebra. +It need not be injective: a necessary consequence of a formal identity suffices +for a lower bound. Order the resulting `2R` coordinates by address coordinate, +so each operator has four `R by R` blocks. For an operator M define + +```text +q_a(M) = rank_F2 M_12, q_b(M) = rank_F2 M_21. +``` + +For arbitrary compatible U,V, block multiplication gives + +```text +(UV)_12 = U_11 V_12 + U_12 V_22, +(UV)_21 = U_21 V_11 + U_22 V_21. +``` + +Rank subadditivity and `rank(XY) <= min(rank X, rank Y)` imply +`q_a(UV) <= q_a(U)+q_a(V)` and the same for q_b. This holds regardless of +commutation, invertibility or intermediate dirty couplings, so it applies to +arbitrarily long prefixes with any surrounding paid and free factors. + +The natural images of paid factors and free scalar maps are + +```text +D_N(a) -> [I N] D_N(b) -> [I 0] S -> [S 0]. + [0 I] [N I] [0 S] +``` + +Their `(q_a,q_b)` charges are `(1,0)`, `(0,1)` and `(0,0)`, respectively. +The target is `[[I-P,P],[P,I-P]]`, where `P=diag(I_t,0)`, hence its two crossing +ranks are both t. Applying subadditivity to the actual entire word proves + +```text + n_a >= t, n_b >= t. +``` + +No normalization of scalar mixing is needed, and no clean-state restriction is +introduced. All R roles are included in every block rank. + +## Combining with the credited total bound + +PR2415's source-bound specialization of PR1989 gives `n_a+n_b >= 3t` under the +same hypotheses. Briefly, the natural action of `GL_2(F2)` on its three nonzero +vectors identifies a,b with adjacent transpositions in S3. Its action on six +ordered distinct pairs splits into increasing and decreasing pairs. Each paid +label crosses exactly one independent direction in this cut; free scalar maps +cross none; SWAP crosses three per target. The same block-rank subadditivity +therefore gives `3t`. This paragraph restates the predecessor's proof; it is not +new work here. Exact source heads and the unchanged main proof hash are in +SOURCES.json. + +If `A <= B`, then + +```text +A*n_a + B*n_b = A*(n_a+n_b) + (B-A)*n_b + >= 3A*t + (B-A)*t = (2A+B)*t. +``` + +Every coefficient used to multiply an inequality is nonnegative. Interchanging +a and b proves the other case. On each target role j, the coordinate projector +`E_jj` and word `aba` give exactly `[s]` on j and identity everywhere else; +`bab` does the same. Choose `aba` when A<=B and `bab` otherwise, and concatenate +over all t target roles. These full formal words attain the stated price and +leave every arbitrary spectator untouched. Thus the lower bound is sharp. + +For example, `(t,A,B)=(5,1,2)` costs 20 exactly, and `(5,0,2)` costs 10 exactly. +Zero-price calls may be used freely often, but the number of positive-price +calls is still bounded as above. If both prices vanish, the minimum is zero. +The theorem is about minimum value, not uniqueness of optimal words. + +## Checks and limitations + +`verify.py` independently builds the six binary matrices, full group-algebra +convolution, full register matrices, their natural images and binary block ranks. +It imports no predecessor implementation. Its complete receipt records: + +- 54 exact formal attaining endpoints, both orientations, t=0..8 and + R=t,t+1,t+2; these include arbitrary dirty spectators by coefficient equality. +- All 1,302 paid factors for R=1..5 with their separate `(1,0)/(0,1)` charges; + every two-role free scalar map on both sides of all 12 two-role paid factors + (144 compositions). +- 2,160 mixed paid/free prefixes for R=1..6, checking the natural homomorphism, + both rank inequalities and accumulated label bounds. These are deterministic + sample words, not a complete search over words. +- All 25 pairs from prices `{0,1/3,1,2,7/2}`, t=0..8, against every count pair + `t<=n_a,n_b<=4t` satisfying the three inequalities; both attaining prices. +- Controls demonstrating why each count inequality is needed, detecting a + full-formal corruption invisible in the natural representation, rejecting an + omitted attaining call, and verifying the direct-SWAP changed-alphabet case. +- A negative-price boundary: `D_N(a)^2=I` coefficientwise, so if A<0, appending + arbitrarily many `aa` loops makes the cost unbounded below. Likewise for B<0. + Nonnegative prices are therefore a substantive hypothesis. + +These finite checks support the written all-parameter proof; they do not replace +it. The natural representation is used only as a lower-bound image; complete +formal coefficients verify every claimed endpoint. The inherited `3t` theorem +is not independently formalized in a proof assistant here. + +The result does not cover role-dependent or state-dependent prices, different +paid labels, higher-rank calls charged as one, partial spectator restoration, +restricted clean input states, nonlinear operations, or the abelian rational +frame model. Nor does it supply native address conversion, hosting, precision, +tape bounds, a recursive child invoice or an integer-multiplication theorem. + +## Reproduce + +Python 3.12+, standard library, from repository root: + +```sh +python3 -I -O -B research/gl2-swap-weighted-tariff/verify.py +python3 -I -O -B research/gl2-swap-weighted-tariff/test_boundary.py +python3 scripts/research_package.py --package research/gl2-swap-weighted-tariff +``` + +Default verification is read-only. `--out NEW_FILE` regenerates the complete +receipt and refuses overwrite. Checks use explicit failures, including under +`-O`. The boundary test verifies unchanged Git-free replay, corrupt/missing +receipt rejection and exclusive regeneration. + +## Open next questions + +1. Can a physically legal changed address label cross multiple directions for + less than the corresponding invoice? This matters because fixed a/b tariff + asymmetry is now closed. Start with one named native implementation and its + full recursive charge; arbitrary formal labels have no such implementation. +2. What is sharp when label prices depend on the projector support? The weighted + combination above uses a single price per label. First classify attainable + projector-specific crossing charges; support-changing free scalar maps make + the price convention itself part of the contract. + +Contributor: ywz65 with substantial OpenAI Codex assistance. Credit remains with +Ross Richardson's general cut theorem and coordinate-SWAP bridge, Aaron Wang's +explicit asymmetric-tariff handoff, and their cited model predecessors. TASK.json +records the original picker, scope change, exact freshness and separate AI review. +No independent human review, new selected frontier or frozen-source edit is claimed. diff --git a/research/integer-address-signed-swap/test_boundary.py b/research/integer-address-signed-swap/test_boundary.py new file mode 100644 index 0000000000..671f640458 --- /dev/null +++ b/research/integer-address-signed-swap/test_boundary.py @@ -0,0 +1,81 @@ +"""Failure-sensitive export and evidence checks, including optimized execution.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +class Boundary(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory(prefix="integer-signed-swap-") + self.root = Path(self.temp.name) + self.pkg = self.root / "research/integer-address-signed-swap" + shutil.copytree(HERE, self.pkg, ignore=shutil.ignore_patterns("__pycache__")) + manifest = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + for item in manifest["files"]: + if item["usage"] != "input" or item["path"].startswith("research/integer-address-signed-swap/"): + continue + dest = self.root / item["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / item["path"], dest) + + def tearDown(self): + self.temp.cleanup() + + def invoke(self, *args): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(self.pkg / "verify.py"), *args], + cwd=self.root, capture_output=True, text=True, encoding="utf-8", timeout=60) + + def hashes(self): + return {str(p.relative_to(self.root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.root.rglob("*") if p.is_file()} + + def test_git_free_readonly_replay(self): + before = self.hashes() + result = self.invoke() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(before, self.hashes()) + + def test_source_drift_rejected(self): + source = self.pkg / "predecessor-2544.md" + source.write_bytes(source.read_bytes()+b"\nChanged premise\n") + result = self.invoke() + self.assertNotEqual(result.returncode, 0) + self.assertIn("source SHA mismatch", result.stderr) + + def test_missing_source_rejected(self): + (self.root / "research/symmetric-adjacent-cut-bound/PROOF.md").unlink() + self.assertNotEqual(self.invoke().returncode, 0) + + def test_typed_receipt_drift_rejected(self): + path = self.pkg / "RESULT.json" + receipt = json.loads(path.read_text(encoding="utf-8")) + receipt["new_selected_exponent"] = 0 # Python equality alone would accept False == 0. + path.write_text(json.dumps(receipt), encoding="utf-8") + result = self.invoke() + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt mismatch", result.stderr) + + def test_missing_receipt_rejected(self): + (self.pkg / "RESULT.json").unlink() + self.assertNotEqual(self.invoke().returncode, 0) + + def test_exclusive_regeneration(self): + destination = self.root / "fresh-result.json" + result = self.invoke("--write-result", str(destination)) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(json.loads(destination.read_text()), json.loads((self.pkg / "RESULT.json").read_text())) + old = destination.read_bytes() + self.assertNotEqual(self.invoke("--write-result", str(destination)).returncode, 0) + self.assertEqual(destination.read_bytes(), old) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/integer-address-signed-swap/verify.py b/research/integer-address-signed-swap/verify.py new file mode 100644 index 0000000000..67a5b424bf --- /dev/null +++ b/research/integer-address-signed-swap/verify.py @@ -0,0 +1,287 @@ +#!/usr/bin/env python3 +"""Exact finite checks accompanying PROOF.md; standard library, no source imports.""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import random +from fractions import Fraction + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +I = (1, 0, 0, 1) +LABELS = {"a+": (1, 1, 0, 1), "a-": (1, -1, 0, 1), + "b+": (1, 0, 1, 1), "b-": (1, 0, -1, 1), + "nx": (-1, 0, 0, 1), "ny": (1, 0, 0, -1)} +TARGETS = {"S": (0, 1, 1, 0), "-S": (0, -1, -1, 0), + "J": (0, 1, -1, 0), "-J": (0, -1, 1, 0)} +VECTORS = ((1, 0), (1, 1), (0, 1)) +PAIRS = ((0, 1), (0, 2), (1, 2), (1, 0), (2, 0), (2, 1)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def mul(x, y): + a, b, c, d = x + e, f, g, h = y + return a*e+b*g, a*f+b*h, c*e+d*g, c*f+d*h + + +def det(g): + a, b, c, d = g + return a*d-b*c + + +def identity(r): + return [[{I} if i == j else set() for j in range(r)] for i in range(r)] + + +def paid(matrix, name, u, v): + """Right multiply by I+([g]+1)uv^T, with exact F2 group supports.""" + r = len(matrix) + require(0 < u < 1 << r and 0 < v < 1 << r and (u & v).bit_count() % 2 == 1, + "not a rank-one idempotent") + g = LABELS[name] + result = [[set(entry) for entry in row] for row in matrix] + for i in range(r): + p = set() + for k in range(r): + if u >> k & 1: + p ^= matrix[i][k] + change = p ^ {mul(h, g) for h in p} + for j in range(r): + if v >> j & 1: + result[i][j] ^= change + return result + + +def scalar_cnot(matrix, source, target): + require(source != target, "noninvertible scalar operation") + result = [[set(entry) for entry in row] for row in matrix] + for row in result: + row[target] ^= row[source] + return result + + +def rank(rows): + pivots = {} + for row in rows: + while row: + p = row.bit_length()-1 + if p in pivots: + row ^= pivots[p] + else: + pivots[p] = row + break + return len(pivots) + + +def rep(g, kind): + a, b, c, d = g + if kind == "natural": + return ((a & 1) | ((b & 1) << 1), (c & 1) | ((d & 1) << 1)) + if kind == "sign": + return (1, 2) if det(g) == 1 else (2, 1) + permutation = [VECTORS.index(((a*x+b*y) % 2, (c*x+d*y) % 2)) + for x, y in VECTORS] + rows = [0]*6 + for j, (x, y) in enumerate(PAIRS): + i = PAIRS.index((permutation[x], permutation[y])) + rows[i] ^= 1 << j + return tuple(rows) + + +def lift(matrix, kind): + r = len(matrix) + dim = 6 if kind == "pairs" else 2 + rows = [0]*(r*dim) + for i in range(r): + for j in range(r): + for g in matrix[i][j]: + for a, bits in enumerate(rep(g, kind)): + for b in range(dim): + if bits >> b & 1: + rows[a*r+i] ^= 1 << (b*r+j) + return rows + + +def cuts(matrix): + r = len(matrix) + natural = lift(matrix, "natural") + pairs = lift(matrix, "pairs") + sign = lift(matrix, "sign") + return (rank([row >> r for row in natural[:r]]), + rank([row & ((1 << r)-1) for row in natural[r:]]), + rank([row >> (3*r) for row in pairs[:3*r]]), + rank([row >> r for row in sign[:r]])) + + +def expected(names, r): + matrix = identity(r) + for j, name in enumerate(names): + matrix[j][j] = {TARGETS[name]} + return matrix + + +def words(target, orientation): + if target == "-J": + word = ["a-", "b+", "a-"] if orientation == "aba" else ["b+", "a-", "b+"] + else: + word = ["a+", "b-", "a+"] if orientation == "aba" else ["b-", "a+", "b-"] + if target == "S": + word.append("nx") + elif target == "-S": + word.append("ny") + return word + + +def counts(word): + return tuple(sum(name.startswith(prefix) for name in word) for prefix in ("a", "b", "n")) + + +def sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + retained = json.loads((HERE / "PREDECESSORS.json").read_text(encoding="utf-8")) + checked = 0 + for item in manifest["files"] + retained["files"]: + if item["usage"] == "provenance": + continue + path = ROOT / item["path"] + raw = path.read_bytes() + # Git checkout LF/CRLF conversion is not scientific content drift. + raw = raw.replace(b"\r\n", b"\n") + require(hashlib.sha256(raw).hexdigest() == item["sha256"], "source SHA mismatch: " + item["path"]) + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(blob == item["git_blob"], "source blob mismatch: " + item["path"]) + checked += 1 + return checked + + +def run(): + source_count = sources() + projector_cases = 0 + free_cases = 0 + for r in range(1, 5): + for u in range(1, 1 << r): + for v in range(1, 1 << r): + if (u & v).bit_count() % 2 != 1: + continue + for name in LABELS: + want = (1, 0, 1, 0) if name[0] == "a" else ((0, 1, 1, 0) if name[0] == "b" else (0, 0, 0, 1)) + require(cuts(paid(identity(r), name, u, v)) == want, "projector cut") + projector_cases += 1 + for i in range(r): + for j in range(r): + if i != j: + require(cuts(scalar_cnot(identity(r), i, j)) == (0, 0, 0, 0), "free cut") + free_cases += 1 + + endpoint_cases = 0 + price_cases = 0 + prices = [Fraction(0), Fraction(1, 3), Fraction(1), Fraction(2), Fraction(7, 2)] + for n in range(5): + for names in itertools.product(TARGETS, repeat=n): + t = sum(det(TARGETS[name]) == -1 for name in names) + for r in (n, n+1): + for orientation in ("aba", "bab"): + matrix = identity(r) + all_words = [] + for j, target in enumerate(names): + for name in words(target, orientation): + matrix = paid(matrix, name, 1 << j, 1 << j) + all_words.append(name) + require(matrix == expected(names, r), "formal endpoint") + require(cuts(matrix) == (n, n, 3*n, t), "target cuts") + require(counts(all_words) == ((2*n, n, t) if orientation == "aba" else (n, 2*n, t)), "attainer count") + endpoint_cases += 1 + for a, b, c in itertools.product(prices, repeat=3): + count = (2*n, n, t) if a <= b else (n, 2*n, t) + require(a*count[0]+b*count[1]+c*count[2] == n*(2*min(a,b)+max(a,b))+t*c, "price attainer") + price_cases += 1 + + rng = random.Random(82026) + prefix_cases = 0 + for r in range(1, 6): + for _ in range(16): + matrix = identity(r) + budget = [0, 0, 0, 0] + for _ in range(9): + if r > 1 and rng.randrange(3) == 0: + i, j = rng.sample(range(r), 2) + matrix = scalar_cnot(matrix, i, j) + else: + while True: + u, v = rng.randrange(1, 1 << r), rng.randrange(1, 1 << r) + if (u & v).bit_count() % 2: + break + name = rng.choice(tuple(LABELS)) + matrix = paid(matrix, name, u, v) + charge = (1, 0, 1, 0) if name[0] == "a" else ((0, 1, 1, 0) if name[0] == "b" else (0, 0, 0, 1)) + budget = [x+y for x,y in zip(budget, charge)] + require(all(x <= y for x,y in zip(cuts(matrix), budget)), "mixed-prefix rank bound") + prefix_cases += 1 + + controls = {} + j_matrix = expected(("J",), 2) + s_matrix = expected(("S",), 2) + require(j_matrix != s_matrix and cuts(j_matrix)[:3] == cuts(s_matrix)[:3] and cuts(j_matrix)[3] == 0 and cuts(s_matrix)[3] == 1, + "omitted sign control") + controls["omitted_neg_detected_only_by_sign_cut"] = True + perturbed = expected(("S",), 2) + perturbed[1][0] ^= {I, mul(LABELS["a+"], LABELS["a+"])} + require(perturbed != s_matrix and all(lift(perturbed, k) == lift(s_matrix, k) for k in ("natural", "pairs", "sign")), "quotient blind spot") + controls["all_quotients_miss_nonzero_formal_perturbation"] = True + require(tuple(x % 2 for x in TARGETS["J"]) == tuple(x % 2 for x in TARGETS["S"]), "mod2 control") + require(all(tuple(x % m for x in TARGETS["J"]) != tuple(x % m for x in TARGETS["S"]) for m in (3,5,7)), "odd moduli control") + controls["finite_modulus_two_breaks_formal_lower_bound"] = True + inverses = {"a+":"a-", "a-":"a+", "b+":"b-", "b-":"b+", "nx":"nx", "ny":"ny"} + for name, inverse in inverses.items(): + require(paid(paid(identity(2), name, 3, 1), inverse, 3, 1) == identity(2), "negative-price identity loop") + controls["six_negative_price_identity_loops"] = True + for target in TARGETS: + word = words(target, "aba") + for omitted in range(len(word)): + matrix = identity(1) + for i, name in enumerate(word): + if i != omitted: + matrix = paid(matrix, name, 1, 1) + require(matrix != expected((target,), 1), "deleted call") + controls["fourteen_deleted_attainer_calls_rejected"] = True + try: + paid(identity(2), "a+", 1, 2) + except ValueError: + controls["nonidempotent_projector_rejected"] = True + else: + raise ValueError("accepted nonidempotent") + rank_two = expected(("S", "S"), 2) + require(cuts(rank_two)[0] == 2, "higher rank label control") + controls["higher_rank_unit_would_change_model"] = True + return {"schema_version": 1, "claim_kind": "finite_checks_for_scoped_proof", + "source_files": source_count, "rank_one_paid_factor_cases": projector_cases, + "free_scalar_factor_cases": free_cases, "full_formal_endpoint_cases": endpoint_cases, + "exact_rational_price_cases": price_cases, "mixed_word_prefix_cases": prefix_cases, + "controls": controls, "formula": "r*(2*min(A,B)+max(A,B))+t*C", + "all_register_proof": "PROOF.md", "new_selected_exponent": False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path, help="write a NEW receipt path; never replace committed evidence") + args = parser.parse_args() + result = run() + rendered = json.dumps(result, indent=2, sort_keys=True)+"\n" + if args.write_result: + with args.write_result.open("x", encoding="utf-8", newline="\n") as handle: + handle.write(rendered) + else: + recorded = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + require(json.dumps(recorded, sort_keys=True) == json.dumps(result, sort_keys=True), "receipt mismatch") + print(rendered, end="") + + +if __name__ == "__main__": + main()