From b065a51249198a23e24195023f4b2e83eda1dd9c Mon Sep 17 00:00:00 2001 From: Gareth Davidson Date: Thu, 15 Oct 2026 06:15:22 +0100 Subject: [PATCH] Prove pairing-rank dirty workspace compression for rank-one words --- .../register-pairing-compression/PROOF.md | 236 ++++++++++ .../register-pairing-compression/README.md | 109 +++++ .../register-pairing-compression/RESULT.json | 367 +++++++++++++++ .../register-pairing-compression/SOURCES.json | 58 +++ .../register-pairing-compression/TASK.json | 301 +++++++++++++ .../register-pairing-compression/VERIFY.json | 36 ++ .../compression.py | 216 +++++++++ .../sources/mixed-middle.md | 231 ++++++++++ .../sources/weighted-boundary.md | 194 ++++++++ .../register-pairing-compression/verify.py | 423 ++++++++++++++++++ 10 files changed, 2171 insertions(+) create mode 100644 research/register-pairing-compression/PROOF.md create mode 100644 research/register-pairing-compression/README.md create mode 100644 research/register-pairing-compression/RESULT.json create mode 100644 research/register-pairing-compression/SOURCES.json create mode 100644 research/register-pairing-compression/TASK.json create mode 100644 research/register-pairing-compression/VERIFY.json create mode 100644 research/register-pairing-compression/compression.py create mode 100644 research/register-pairing-compression/sources/mixed-middle.md create mode 100644 research/register-pairing-compression/sources/weighted-boundary.md create mode 100644 research/register-pairing-compression/verify.py diff --git a/research/register-pairing-compression/PROOF.md b/research/register-pairing-compression/PROOF.md new file mode 100644 index 0000000000..f91d23a430 --- /dev/null +++ b/research/register-pairing-compression/PROOF.md @@ -0,0 +1,236 @@ +# Retain the dirty pairing, not the entire dirty span + +A rank-one word with a fully restored dirty complement can be compressed to +its active roles plus the rank of the pairing between its dirty column and row +spans. The construction preserves every ordered contraction over an arbitrary +unital F2-algebra. The proof is uniform in word length and finite role count; +the finite tests corroborate the implementation, not those quantifiers. + +For the formal UT4 endpoint `diag([z],[uz],I_rest)`, the credited span bounds +then give at most `2+floor((L-13)/2)` roles for a word of length L. In particular, +the possible cost-25 improvement at prices `(a,b,c)=(1,3,1)` reduces to three +roles. This is a workspace reduction; existence of that improvement is open. + +## General compression theorem + +Let `E=H direct-sum K` be a finite-dimensional binary role space, with `dim H=h`. +Let R be any unital F2-algebra, possibly noncommutative. Consider an ordered word + +``` +W = product_(j=1..L) (I + lambda_j x_j y_j^T), +x_j,y_j in F2^r, lambda_j in R. +``` + +Binary scalars commute with R. Every original outer product is nonzero. Let +`u_j` be the K component of `x_j`, and let `v_j` be the restriction of `y_j^T` +to K. Put + +``` +U = span{u_j} <= K, V = span{v_j} <= K*, +t = rank(V x U -> F2), (v,u) |-> v(u). +``` + +Equivalently, t is the rank of the L-by-L dirty contraction matrix +`M_ij = v_i(u_j)`. Spanning lists or bases give the same rank. + +**Theorem.** There is a word W' on `H direct-sum F2^t`, using the same ordered +coefficient list and rank-at-most-one binary couplings, such that + +``` +W' = Fhat W Ghat, +Fhat = diag(I_H,F), Ghat = diag(I_H,G), FG=I_t. +``` + +Every scalar contraction `y_i^T x_j` is preserved, including `i=j`. If +`W=diag(T_H,I_K)` as a full matrix over R, then +`W'=diag(T_H,I_t)`. Delete zero outer products: every remaining factor belongs +to the arbitrary nonzero rank-one alphabet, in the original order, and every +label count weakly decreases. A label-dependent nonnegative price cannot rise. +No clean initial state, physical projection, COPY, ERASE, or executed F/G map +is used. The construction defines a different legal word. + +**Construction.** Let `U_rad=U intersect ann(V)`. Choose a complement +`U=U_0 direct-sum U_rad`; `dim U_0=t`. Choose an isomorphism +`G:F2^t -> U_0 <= K`. On U define F to take the U_0 component to its G +coordinates, and extend F linearly to K. This is possible because U is a +subspace of K. Then `FG=I_t`. For every `u in U`, `u-GFu` lies in U_rad, so + +``` +vGFu = vu for every v in V, u in U. (1) +``` + +The implementation chooses independent evaluation images of a basis of U to +obtain U_0, and solves a consistent binary linear system for each row of F. +It does not assume that an ambient coordinate projection has property (1). + +Set `x'_j=Fhat x_j`, `y'_j^T=y_j^T Ghat`. The active components are unchanged, +and (1) gives + +``` +y'_i^T x'_j = y_i^T x_j for all i,j. (2) +``` + +Expand any nonempty ordered subsequence `i_1<...=rank M=t`. The +construction therefore uses the minimum number of dirty roles for this exact +factorwise preservation requirement. This is not a lower bound for all words +with the same endpoint: changing the factor list can use less workspace. + +## Why active-corner projection alone is insufficient + +On one active and one dirty role take + +``` +N_1=e_active e_dirty^T, N_2=e_dirty e_active^T. +``` + +The active corner of `(I+A N_1)(I+B N_2)` contains `I+AB`, whereas both naively +projected couplings vanish. In `F2[UT4(F2)]`, `A=[a]+1`, `B=[b]+1` have nonzero +ordered product AB. Here t=1, which correctly retains the feedback direction. +The finite census detects every such failure among all 2,401 ordered pairs of +nonzero binary rank-one couplings on three roles with one active role. + +Conversely, with two dirty directions, a row supported on the second and a +column supported on the first may both occur, with zero dirty pairing. Their +inverse-paired relator restores all inputs and compresses to no dirty roles. +Neither common block orientation need hold. This separates the new lemma from +the one-orientation hypothesis of PR1680. PR1541 restricts to an image span; +that space may still contain the radical eliminated here. + +## UT4 application and inherited premises + +Use the same formal alphabet as Nick Petalas's +[PR2175](https://github.com/CrocSwap/integer-mult-bounds/pull/2175): +`G=UT4(F2)`, `R=F2[G]`, `a=I+E12`, `b=I+E23`, `c=I+E34`, +`u=I+E13`, `z=I+E14`. A paid call is `I+([g]+1)xy^T` for `g in {a,b,c}` and +any nonzero binary rank-one coupling, including nilpotents. Every occurrence +is charged. Scalar GL mixing is optimistically free and normalized into the +couplings; augmentation makes any final scalar map identity. There are no free +address maps or initialized roles. All extra roles are arbitrary and restored. + +Let H be the two active coordinate roles. For label g let X_g and Y_g denote +the spans of all coupling columns and rows. The PR2027 coefficient-span argument +and PR2175 mixed-middle argument give, uniformly in finite r and L, + +``` +H <= X_g, H* <= Y_g (all six containments), +n_a >= dim X_a + dim Y_a, +n_c >= dim X_c + dim Y_c, +n_b >= dim X_b + dim Y_b + 1. (3) +``` + +These are credited inputs. For clarity, their mechanism is as follows. In the +retained degree-three quotient of the free algebra on A,B,C, the target has +coefficient `P=diag(1,1,0,...)` on ABC, ACB, BAC, CBA, and +`S=diag(0,1,0,...)` on AB, BA, ABA, BAB. First and last letters force the six +containments; first-degree coefficients give zero sums and the outer rank +inequalities. For middle calls, the transported-column/row matrices obey +`XY=0, UY=S, XV=0, UV=P`. Delete S's output coordinate by pi. The rank-one map +`pi P` factors through `ker X / im Y`, giving the extra 1 in (3). The quotient +homomorphism and earlier census are predecessor evidence, not newly replayed +by this package. Exact archived proofs retain their attribution and pins. + +Define `e_g^x=dim X_g-2`, `e_g^y=dim Y_g-2`. They are nonnegative integers, +and (3) gives + +``` +sum_g(e_g^x+e_g^y) <= L-13. (4) +``` + +Because each X_g contains H, its projection onto K has dimension e_g^x; +similarly the dirty row projection has dimension e_g^y. Hence the combined +spaces U,V from the general theorem satisfy + +``` +dim U <= sum_g e_g^x, dim V <= sum_g e_g^y, +t <= min(dim U,dim V) <= floor((L-13)/2). (5) +``` + +The compressed full endpoint therefore uses at most +`2+floor((L-13)/2)` roles, and no larger label counts. This applies to every +length for which a word exists. It recovers two roles at L<=14 and gives three +at L<=16, four at L<=18, and so on. The bound is sufficient, not a claim that +all these role counts are necessary or that a word exists at each length. + +## The precise fifteen-call handoff + +The pinned [PR2314](https://github.com/CrocSwap/integer-mult-bounds/pull/2314) +result excludes fourteen-call five-b words on arbitrary dirty workspace. +Together with (3), it gives + +``` +n_a,n_c >= 4, n_b >= 5, +n_b=5 implies n_a+n_c >= 10. (6) +``` + +Its two exhaustive quotient censuses are inherited computer-assisted premises; +this package does not rerun or claim them as new evidence. Their public head +and exact proof are retained in SOURCES.json and sources/weighted-boundary.md. + +At positive letter prices `(alpha,beta,gamma)=(1,3,1)`, the credited direct +word `abcbabcb` on z and `acbabc` on uz costs 26. Any cheaper word must have +`n_b=5` (six b calls already cost at least 26). By (6), the only cheaper counts +are `(6,5,4)`, `(5,5,5)`, `(4,5,6)`, all of length 15 and cost 25. Equations +(4)-(5) compress any such word to at most three roles. No factor can disappear: +that would create a cost at most 24 word contradicting (6). Thus each count +split is preserved exactly. A word using fewer than three roles can be padded +with an identity dirty spectator. + +Consequently, a cost-25 word exists on any finite dirty workspace if and only +if one exists on exactly three roles in these three count splits. At five b +calls, (3) also forces both b spans to equal H, so every b coupling is supported +on the active 2x2 block. This extra restriction is necessary, not a construction. +A complete three-role exclusion would establish the exact cost 26; a survivor +must pass the full 64-element group-algebra endpoint. A quotient survivor or +finite sampled address test would not establish it. + +## Evidence, credit and remaining scope + +The general theorem above is elementary linear algebra; no literature-priority, +proof-kernel, independent human or independent-agent review is claimed. New +code constructs F,G, tests their full product identity, and separately evaluates +faithful dirty-input columns using literal 4x4 binary group multiplication. +The exact domains, digests, source bindings and deliberate failures are in +RESULT.json. All checks remain active with Python assertions disabled. + +Credit CinnaDavis / 1337isnot1337 PR1541 for image-span restriction; +ToikY PR1662/1680 for UT4 span bounds and common-orientation compression; +Gareth Davidson PR2027 for mixed-root tariffs and PR2314 for the weighted +boundary; Nick Petalas / petalas PR2175 for the mixed-middle inequality; +Aaron Wang / navinor PR1690 for the inherited finite profile-screen method. +The PR2175/2314 proofs retain the earlier steph4n-gh, Arham Tahir and Hanson Sun +lineage. Only two actually used proof documents are archived; no predecessor +implementation or census package is copied. + +The new contribution is the uniform pairing reduction and its missing-workspace +implication for the next weighted question. No fifteen-call census, optimum +outside the previously proved price cone, native/compiler realization, physical +supplier, precision/reserve theorem, all-size transfer, or new kappa is claimed. +Prepared by Gareth Davidson / @bitplane with substantial OpenAI Codex assistance. +Apache-2.0. diff --git a/research/register-pairing-compression/README.md b/research/register-pairing-compression/README.md new file mode 100644 index 0000000000..d80d0cb3a3 --- /dev/null +++ b/research/register-pairing-compression/README.md @@ -0,0 +1,109 @@ +# Dirty-workspace compression by pairing rank + +A full formal rank-one word can retain just the dirty directions that feed +back into its calls. If U is its dirty column span and V its dirty row span, +let `t=rank(V x U -> F2)`. The word compresses from `h+k` roles to `h+t`, +preserving the active endpoint and restoring every retained arbitrary dirty +role. Every ordered contraction is preserved over any unital F2-algebra, +including noncommutative ones. Letter counts never increase. + +The uniform [proof](PROOF.md) constructs binary maps F,G with `FG=I` and +`vGFu=vu`, then expands the ordered rank-one product. These maps describe a +new legal word; they are not additional physical operations. Idempotent factors +remain nonzero idempotents; nilpotent factors may become identity and be removed. +The exact pairing rank is minimal among replacements preserving the active +components and every contraction, not among all words for the same endpoint. + +## Concrete consequence + +For `diag([z],[uz],I_rest)` in the formal F2[UT4(F2)] adjacent-letter alphabet, +the inherited span inequalities give + +``` +roles needed <= 2 + floor((L - 13) / 2). +``` + +In particular, every possible 15- or 16-call word reduces to at most three +roles, uniformly over any original finite dirty workspace. This extends the +prior one-excess/common-orientation reduction. + +At letter prices `(a,b,c)=(1,3,1)`, the direct word costs 26. Building on the +pinned [PR2314](https://github.com/CrocSwap/integer-mult-bounds/pull/2314) +weighted boundary, any cheaper word costs exactly 25 and has counts +`(6,5,4)`, `(5,5,5)` or `(4,5,6)`. The new lemma preserves those counts and +reduces existence to exactly three roles, with all b couplings supported on +the active two-role block. **Whether such a word exists remains open.** + +This is a formal-model reduction and a concrete missing-workspace handoff. +No new native supplier, physical cost saving, weighted optimum or kappa is +claimed. Geometry, support restrictions, compilation, hosting, precision, +reserves and all-size transfer need their own arguments. + +## Evidence and reproduction + +```sh +python3.12 -B scripts/research_package.py --package research/register-pairing-compression +``` + +The registered commands use `-I -O -B`, standard library only. They check: + +- Every ordered pair of binary subspaces of workspace dimensions 0 through 4: + 4,775 pairs, with an independent set-image pairing-rank oracle and complete + noncommutative product comparison for each constructed word. +- All 2,401 ordered rank-one coupling pairs on three roles with one active role; + 384 expose the failure of naive active-corner projection. +- 29 complete dirty-endpoint fixtures on up to eight roles, including changed + dirty bases, idempotents, nilpotents, and bidirectional orthogonal workspace. + A separate literal group-action checker evaluates all 18,176 basis columns. +- All 4,096 literal UT4 group products, fourteen semantic controls, + the integer span budgets and exact cost-25 count splits. +- Four actual source/proof/receipt corruption controls and a Git-free relocated + preflight. Occupied output paths are rejected. + +[RESULT.json](RESULT.json) records exact coverage and transcript digests. The +finite checks corroborate the new construction; [PROOF.md](PROOF.md) establishes +the general quantifiers. The PR2175/2314 quotient homomorphism and exclusion +censuses are credited inherited premises and are **not rerun here**. Their exact +proofs are archived unchanged, with author, public head, Git blob and SHA256 +bindings in [SOURCES.json](SOURCES.json). Three main-branch proof inputs are +also pinned and declared to the replay planner. Historical catalogue and +selected-result pins are provenance, not new results. + +Direct replay from a Git-free export requires this package plus the three +`usage=input` paths in SOURCES.json. It reads its inputs and uses temporary +copies for corruption controls. To regenerate a receipt for review, use +`verify.py --write-result /an/unoccupied/path.json`; normal verification never +rewrites RESULT.json. + +## Open next questions + +Decide the three 15-call count splits on three roles, keeping all b couplings +inside the active block. A complete necessary-quotient exclusion would settle +the formal price at 26; any survivor needs the full group-algebra endpoint. +Start by deriving a complete normal form or coverage certificate for the single +dirty direction. No three-role census or witness is provided here. + +A separate application could replace the whole image-span bound in a different +rank-one alphabet, provided that alphabet is closed under the constructed +couplings. The first step is an explicit closure check; native or geometric +restrictions cannot be assumed preserved. Structured questions and the changed +card scope are in [TASK.json](TASK.json). + +## Attribution and scope change + +Credit CinnaDavis / 1337isnot1337 PR1541 for image-span restriction; ToikY +PR1662/1680 for UT4 spans and common-orientation compression; Nick Petalas / +petalas PR2175 for the mixed-middle inequality; Gareth Davidson PR2027/2314 for +the mixed tariff and weighted boundary; Aaron Wang / navinor PR1690 for the +inherited census method and its predecessor lineage. This package adds the +pairing reduction, not those bounds or the direct word. No literature-priority +claim is made for the underlying linear algebra. + +The single OS draw selected `bit-new-register-model`. Scope is explicitly +changed to the missing workspace implication in this nonabelian formal model; +it does not meet the card's native-construction gate. The baseline and the +specified predecessor boundaries were checked first. Coordination is the +[scoped follow-up in Discussion2019](https://github.com/CrocSwap/integer-mult-bounds/discussions/2019#discussioncomment-18941076). + +Prepared by Gareth Davidson / @bitplane with substantial OpenAI Codex assistance. +No subagents, independent human review or proof-kernel check. Apache-2.0. diff --git a/research/register-pairing-compression/RESULT.json b/research/register-pairing-compression/RESULT.json new file mode 100644 index 0000000000..7f1f660076 --- /dev/null +++ b/research/register-pairing-compression/RESULT.json @@ -0,0 +1,367 @@ +{ + "bindings": { + "PROOF.md": "f9c3c3f1363787ed0c92a65abba065d5debcb1e526a439cd3c82ad48d24f27bd", + "SOURCES.json": "a226038d414feeeb640540a9a53a5939048ebc14b1deab2b2a1e4b33ccccf3fe", + "compression.py": "ba409bd717c74c5af69f92cc96ec2efd4d5898533b5a6e2322b8f44f38d395db", + "verify.py": "c2d6096a89a35d87ba95b94cf96791ae388fcdae18129748995ff0bd15ec9fd6" + }, + "full_endpoint_fixtures": { + "deleted_nilpotent_factors": 4, + "faithful_columns": 18176, + "fixtures": [ + { + "compressed_length": 14, + "length": 14, + "rank": 0, + "roles": 2 + }, + { + "compressed_length": 16, + "length": 16, + "rank": 0, + "roles": 3 + }, + { + "compressed_length": 16, + "length": 16, + "rank": 1, + "roles": 3 + }, + { + "compressed_length": 18, + "length": 18, + "rank": 0, + "roles": 4 + }, + { + "compressed_length": 18, + "length": 18, + "rank": 1, + "roles": 4 + }, + { + "compressed_length": 18, + "length": 18, + "rank": 2, + "roles": 4 + }, + { + "compressed_length": 20, + "length": 20, + "rank": 0, + "roles": 5 + }, + { + "compressed_length": 20, + "length": 20, + "rank": 1, + "roles": 5 + }, + { + "compressed_length": 20, + "length": 20, + "rank": 2, + "roles": 5 + }, + { + "compressed_length": 20, + "length": 20, + "rank": 3, + "roles": 5 + }, + { + "compressed_length": 22, + "length": 22, + "rank": 0, + "roles": 6 + }, + { + "compressed_length": 22, + "length": 22, + "rank": 1, + "roles": 6 + }, + { + "compressed_length": 22, + "length": 22, + "rank": 2, + "roles": 6 + }, + { + "compressed_length": 22, + "length": 22, + "rank": 3, + "roles": 6 + }, + { + "compressed_length": 22, + "length": 22, + "rank": 4, + "roles": 6 + }, + { + "compressed_length": 24, + "length": 24, + "rank": 0, + "roles": 7 + }, + { + "compressed_length": 24, + "length": 24, + "rank": 1, + "roles": 7 + }, + { + "compressed_length": 24, + "length": 24, + "rank": 2, + "roles": 7 + }, + { + "compressed_length": 24, + "length": 24, + "rank": 3, + "roles": 7 + }, + { + "compressed_length": 24, + "length": 24, + "rank": 4, + "roles": 7 + }, + { + "compressed_length": 24, + "length": 24, + "rank": 5, + "roles": 7 + }, + { + "compressed_length": 26, + "length": 26, + "rank": 0, + "roles": 8 + }, + { + "compressed_length": 26, + "length": 26, + "rank": 1, + "roles": 8 + }, + { + "compressed_length": 26, + "length": 26, + "rank": 2, + "roles": 8 + }, + { + "compressed_length": 26, + "length": 26, + "rank": 3, + "roles": 8 + }, + { + "compressed_length": 26, + "length": 26, + "rank": 4, + "roles": 8 + }, + { + "compressed_length": 26, + "length": 26, + "rank": 5, + "roles": 8 + }, + { + "compressed_length": 26, + "length": 26, + "rank": 6, + "roles": 8 + } + ], + "idempotent_occurrences": 504, + "nilpotent_occurrences": 112, + "orthogonal_bidirectional_fixture": true + }, + "literal_group_products": 4096, + "rank_one_pair_census": { + "naive_projection_failures": 384, + "ordered_pairs": 2401, + "pairing_rank_histogram": { + "0": 289, + "1": 1536, + "2": 576 + }, + "transcript_sha256": "48f482316b765943ca2c4b480bdcec4c6129eee684dd7f50b7f0633799305942" + }, + "schema_version": 1, + "scope": "Finite corroboration of PROOF.md; no fifteen-call census, native supplier, or kappa claim.", + "semantic_controls": [ + "naive active-corner projection loses feedback", + "wrong F_rows", + "wrong G_columns", + "incorrect zero pairing rank", + "FG identity without contraction preservation", + "transposed coupling", + "unpriced deletion", + "unrestored dirty role", + "dirty input contaminates target", + "ordered noncommutative coefficients", + "omitted restoration call", + "wrong paid letter", + "zero original factor", + "out-of-domain role" + ], + "source_inputs": [ + "research/three-swap-compression-seed6/PROOF.md", + "research/ut4-mixed-root-tariffs/PROOF.md", + "research/ut4-one-slack-workspace/PROOF.md", + "sources/mixed-middle.md", + "sources/weighted-boundary.md" + ], + "subspace_census": { + "domains": [ + { + "pairing_rank_histogram": { + "0": 1 + }, + "pairs": 1, + "subspaces": 1, + "workspace": 0 + }, + { + "pairing_rank_histogram": { + "0": 3, + "1": 1 + }, + "pairs": 4, + "subspaces": 2, + "workspace": 1 + }, + { + "pairing_rank_histogram": { + "0": 12, + "1": 12, + "2": 1 + }, + "pairs": 25, + "subspaces": 5, + "workspace": 2 + }, + { + "pairing_rank_histogram": { + "0": 66, + "1": 147, + "2": 42, + "3": 1 + }, + "pairs": 256, + "subspaces": 16, + "workspace": 3 + }, + { + "pairing_rank_histogram": { + "0": 513, + "1": 2250, + "2": 1575, + "3": 150, + "4": 1 + }, + "pairs": 4489, + "subspaces": 67, + "workspace": 4 + } + ], + "total_pairs": 4775, + "transcript_sha256": "cb51204edfe62a9fd07fe7389df5c67b9eb35b08d12e65db7641e1980942201b" + }, + "ut4_consequence": { + "cheaper_price": 25, + "direct_price": 26, + "fifteen_call_existence_decided": false, + "maximum_roles_for_cheaper_word": 3, + "only_cheaper_count_splits": [ + [ + 4, + 5, + 6 + ], + [ + 5, + 5, + 5 + ], + [ + 6, + 5, + 4 + ] + ], + "price": [ + 1, + 3, + 1 + ], + "span_relaxations": [ + { + "length": 13, + "role_bound": 2, + "span_profiles": 1 + }, + { + "length": 14, + "role_bound": 2, + "span_profiles": 7 + }, + { + "length": 15, + "role_bound": 3, + "span_profiles": 28 + }, + { + "length": 16, + "role_bound": 3, + "span_profiles": 84 + }, + { + "length": 17, + "role_bound": 4, + "span_profiles": 210 + }, + { + "length": 18, + "role_bound": 4, + "span_profiles": 462 + }, + { + "length": 19, + "role_bound": 5, + "span_profiles": 924 + }, + { + "length": 20, + "role_bound": 5, + "span_profiles": 1716 + }, + { + "length": 21, + "role_bound": 6, + "span_profiles": 3003 + }, + { + "length": 22, + "role_bound": 6, + "span_profiles": 5005 + }, + { + "length": 23, + "role_bound": 7, + "span_profiles": 8008 + }, + { + "length": 24, + "role_bound": 7, + "span_profiles": 12376 + } + ] + } +} diff --git a/research/register-pairing-compression/SOURCES.json b/research/register-pairing-compression/SOURCES.json new file mode 100644 index 0000000000..5c9d0f322a --- /dev/null +++ b/research/register-pairing-compression/SOURCES.json @@ -0,0 +1,58 @@ +{ + "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/three-swap-compression-seed6/PROOF.md", + "usage": "input", + "git_blob": "9a1e4dfc6dcb0632efa24aacc2313ac17b10e5bf", + "sha256": "b60b9abd328ae0c45fcb86af19bb5d339d531d329e5f9886ad7b0c0f8d8b3a1e" + }, + { + "path": "research/ut4-mixed-root-tariffs/PROOF.md", + "usage": "input", + "git_blob": "633a7d5137ad13fafe719cc042099977ad1f96e5", + "sha256": "c0def58338a69a57ac95f1d32a744993aa07656c46eba88a99354b276917bd8e" + }, + { + "path": "research/ut4-one-slack-workspace/PROOF.md", + "usage": "input", + "git_blob": "4ca867ca780aff8bae8ab695959c89f35543586c", + "sha256": "a9e2c7e6f6841b0f9a53c65861c2e212c2bc126923d9e41f5723c530389e96cf" + } + ], + "archived_proofs": [ + { + "path": "sources/mixed-middle.md", + "source_path": "research/ut4-mixed-central-middle/PROOF.md", + "head": "1d943bc9e0718c8a2f15e1d0a22b73ad528ef0ca", + "git_blob": "e6a7c24d20c7718989a2b00e97ef9638f7804226", + "sha256": "34a5dc532b9010b5e8afd67273a9d4b1cf17e1362f5f432c4b433581cc7784d5", + "author": "Nick Petalas / petalas", + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2175", + "use": "Inherited mixed-middle span inequality; thirteen-call census is not replayed here." + }, + { + "path": "sources/weighted-boundary.md", + "source_path": "research/ut4-mixed-weighted-boundary/PROOF.md", + "head": "16319e3f12fc95d5820a3f1802e2976949c92933", + "git_blob": "d5ba9d06c0bb4e8553da56d504eb8d5f2ee0e1bd", + "sha256": "580fce5e5e460fd00afa8fa0231395859fdf5cf0998df9d21471b40a996665ef", + "author": "Gareth Davidson / bitplane, substantial OpenAI Codex assistance", + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2314", + "use": "Inherited five-b outer-count bound for the precise cost25 handoff; fourteen-call census is not replayed here." + } + ] +} diff --git a/research/register-pairing-compression/TASK.json b/research/register-pairing-compression/TASK.json new file mode 100644 index 0000000000..b7236809a7 --- /dev/null +++ b/research/register-pairing-compression/TASK.json @@ -0,0 +1,301 @@ +{ + "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": "Uniform rank-pairing compression for full rank-one words over any unital F2-algebra; all-register UT4 cost25 existence reduces to three roles.", + "scope_change_reason": "The selected changed-alphabet card is narrowed to its missing workspace implication. This extends prior common-orientation compression and leaves native conversion and fifteen-call existence open.", + "bottleneck_link": "Removes an unbounded dirty-workspace dimension from the next specific weighted nonabelian bit-word question. Formal-model partial result; no physical supplier or selected moment improvement.", + "budget_minutes": 60, + "stop_rule": "Bounded pass42: prove or falsify the full-endpoint pairing lemma, test complete small binary domains, publish the three-role handoff; no fifteen-call census.", + "outcome": "completed", + "evidence": "PROOF.md gives the uniform construction and full product identity; RESULT.json corroborates finite domains and binds source proofs and code. Inherited PR2175/2314 exclusion censuses are not rerun.", + "author": "Gareth Davidson / @bitplane", + "ai_assistance": "Substantial OpenAI Codex assistance. No subagents, independent human or kernel review.", + "open_questions": [ + { + "question": "Does any of (6,5,4), (5,5,5), (4,5,6) realize z/uz on three roles?", + "why_it_matters": "The new reduction makes this decisive for cost25 versus26 at prices(1,3,1), for every finite dirty workspace.", + "first_step": "Exploit the active-only b couplings and derive a complete one-dirty-direction normal form before a bounded quotient census; verify any survivor in the full algebra.", + "blocked_by": "No three-role fifteen-call census or witness is supplied." + }, + { + "question": "Does a different rank-one register alphabet remain closed under pairing compression?", + "why_it_matters": "The linear-algebra lemma could remove workspace from other concrete searches, but cannot preserve arbitrary native or geometric restrictions automatically.", + "first_step": "State the actual legal coupling constraints and prove their preservation or give a counterexample.", + "blocked_by": "Only arbitrary nonzero binary rank-one couplings and the idempotent restriction are covered here." + } + ], + "selection": { + "seed": "7a2384591c85979b237ae332e98a912d", + "track": "bit-mechanisms", + "suggestions": [ + { + "task_id": "bit-new-register-model", + "scope_key": "7084092dd726e7ba1f2f", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "method": "Derive a target-specific relaxation bound for that same explicit alphabet.", + "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" + ], + "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_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "bit-helper-contract", + "scope_key": "3475f46c8358c6a9211b", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "method": "Derive a replacement interface lemma and price its implementation.", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "catalog_assessed_on": "2026-10-14", + "priority_revision": 4, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2019#discussioncomment-18941076", + "first_command": { + "argv": [ + "/usr/bin/python3.12", + "-B", + "scripts/research_baseline.py" + ], + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY" + }, + "optimistic_budget": { + "prices": [ + 1, + 3, + 1 + ], + "direct_counts": [ + 4, + 6, + 4 + ], + "direct_cost": 26, + "only_cheaper_counts": [ + [ + 6, + 5, + 4 + ], + [ + 5, + 5, + 5 + ], + [ + 4, + 5, + 6 + ] + ], + "candidate_cost": 25, + "physical_invoice": "unbuilt; formal prices only" + }, + "overlap": { + "entry": { + "open_prs": { + "fetched_at": "2026-10-15T04:55:48.834313+00:00", + "complete_pagination": true, + "records": 535 + }, + "discussions": { + "fetched_at": "2026-10-15T04:57:17.334309+00:00", + "complete_pagination": true, + "records": 1023 + } + }, + "targeted_pairing_check": "No pairing-rank/bilinear-compression/contraction-preserving UT4 or workspace match in the complete cached remote records; closest local proofs read in full relevant sections.", + "nearest": [ + { + "pr": 1541, + "difference": "Image-span restriction does not quotient its invisible dirty radical." + }, + { + "pr": 1680, + "difference": "One-excess/common-orientation projection; current result preserves feedback pairing beyond that domain." + }, + { + "pr": 2175, + "difference": "Supplies the mixed-middle span inequality; no longer-word workspace theorem." + }, + { + "pr": 2314, + "difference": "Supplies cost25 count constraints, explicitly leaves larger-slack compression open." + } + ], + "limits": "PR bodies/discussions and local metadata, plus relevant proof reads; not all code diffs or unpublished work.", + "pre_submit": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "checked_utc": "2026-10-15T05:14:46.100528+00:00", + "priority_revision": 4, + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T05:13:15.813304+00:00", + "complete_pagination": true, + "records": 536 + }, + "discussions": { + "fetched_at": "2026-10-15T05:14:46.033410+00:00", + "complete_pagination": true, + "records": 1035 + } + }, + "warnings": [], + "matches_inspected": 12, + "disposition": "Own claim/package; prior PR1541/1680 compression; pure-central z/z fifteen-call PR1816, distinct from mixed z/uz; five-SWAP commuting-projector PR2317 and predecessor full-occupancy notes, different group/target. No competing pairing compression identified; no novelty guarantee.", + "predecessor_heads_unchanged": { + "2175": "1d943bc9e0718c8a2f15e1d0a22b73ad528ef0ca", + "2314": "16319e3f12fc95d5820a3f1802e2976949c92933" + } + } + }, + "receipt_sha256": "9e35028964ecf9ed69257249e3b2ea3ff73a8a54e6f891c129d24769b43a4c60", + "validation": { + "registered_python": "3.12.3", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE with -I -O -B", + "readonly_export": { + "python": "Python 3.14.4", + "files": 13, + "read_only_probe_rejected": true, + "hashes_unchanged": true, + "commands": [ + { + "argv": [ + "/usr/bin/python3.14", + "-I", + "-O", + "-B", + "/home/gaz/tmp/math/sprint/pass-42/export314/research/register-pairing-compression/verify.py" + ], + "exit_code": 0 + }, + { + "argv": [ + "/usr/bin/python3.14", + "-I", + "-O", + "-B", + "/home/gaz/tmp/math/sprint/pass-42/export314/research/register-pairing-compression/verify.py", + "--controls" + ], + "exit_code": 0 + } + ], + "checked_at": "2026-10-15T05:13:40.963017+00:00" + }, + "occupied_output": { + "occupied_output_rejected": true, + "original_bytes_preserved": true + }, + "inherited_censuses_replayed": false + } +} diff --git a/research/register-pairing-compression/VERIFY.json b/research/register-pairing-compression/VERIFY.json new file mode 100644 index 0000000000..b85470ab9d --- /dev/null +++ b/research/register-pairing-compression/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/three-swap-compression-seed6/PROOF.md", + "research/ut4-mixed-root-tariffs/PROOF.md", + "research/ut4-one-slack-workspace/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete small-subspace/coupling domains, full noncommutative products, literal faithful dirty columns, uniform-bound integer consequences and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py", + "--controls" + ], + "timeout_seconds": 60, + "checks": "Four actual live/archived proof and receipt corruptions rejected, and Git-free relocated preflight accepted." + } + ] +} diff --git a/research/register-pairing-compression/compression.py b/research/register-pairing-compression/compression.py new file mode 100644 index 0000000000..6038a64833 --- /dev/null +++ b/research/register-pairing-compression/compression.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Exact binary pairing compression; Gareth Davidson, Codex assistance, Apache-2.0. + +Vectors and functionals are little-endian bit masks. Maps are mathematical +witnesses for constructing a new word; they are not executed register operations. +""" +from dataclasses import dataclass + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(x, y): + return (x & y).bit_count() & 1 + + +def basis(vectors): + pivots = {} + chosen = [] + for original in vectors: + v = original + for p in sorted(pivots, reverse=True): + if v >> p & 1: + v ^= pivots[p] + if v: + pivots[v.bit_length() - 1] = v + chosen.append(original) + return chosen + + +def coordinates(independent, vector): + pivots = {} + for i, original in enumerate(independent): + v, tag = original, 1 << i + for p in sorted(pivots, reverse=True): + if v >> p & 1: + v ^= pivots[p][0] + tag ^= pivots[p][1] + require(v != 0, "coordinate basis is dependent") + pivots[v.bit_length() - 1] = (v, tag) + out = 0 + for p in sorted(pivots, reverse=True): + if vector >> p & 1: + vector ^= pivots[p][0] + out ^= pivots[p][1] + require(vector == 0, "vector is outside the coordinate span") + return out + + +def solve(equations, width): + """Solve a consistent binary linear system, assigning free coordinates zero.""" + pivots = {} + for mask, rhs in equations: + require(0 <= mask < 1 << width and rhs in (0, 1), "invalid equation") + for p in sorted(pivots, reverse=True): + if mask >> p & 1: + mask ^= pivots[p][0] + rhs ^= pivots[p][1] + if mask: + pivots[mask.bit_length() - 1] = (mask, rhs) + else: + require(rhs == 0, "inconsistent equations") + answer = 0 + for p in sorted(pivots): + mask, rhs = pivots[p] + answer |= (rhs ^ dot(mask, answer)) << p + return answer + + +@dataclass(frozen=True) +class Factor: + label: str + x: int + y: int + + +def evaluate_rows(rows, vector): + return sum(dot(row, vector) << i for i, row in enumerate(rows)) + + +def pairing_maps(word, active, roles): + require(0 <= active <= roles, "invalid active/total dimension") + for f in word: + require(0 < f.x < 1 << roles and 0 < f.y < 1 << roles, + "original factor must be nonzero and within the role space") + width = roles - active + ub = basis(f.x >> active for f in word) + vb = basis(f.y >> active for f in word) + images, columns = [], [] + for u in ub: + image = evaluate_rows(vb, u) + if len(basis([*images, image])) > len(images): + images.append(image) + columns.append(u) + t = len(images) + u_coordinates = [coordinates(images, evaluate_rows(vb, u)) for u in ub] + rows = [solve([(u, c >> j & 1) for u, c in zip(ub, u_coordinates)], width) + for j in range(t)] + return {"active": active, "roles": roles, "rank": t, + "column_span_rank": len(ub), "row_span_rank": len(vb), + "F_rows": rows, "G_columns": columns} + + +def compress(word, active, roles): + maps = pairing_maps(word, active, roles) + rows, columns = maps["F_rows"], maps["G_columns"] + mask = (1 << active) - 1 + reduced, indices = [], [] + for i, f in enumerate(word): + x = (f.x & mask) | (evaluate_rows(rows, f.x >> active) << active) + y = (f.y & mask) | (evaluate_rows(columns, f.y >> active) << active) + if x and y: + reduced.append(Factor(f.label, x, y)) + indices.append(i) + maps["retained_indices"] = indices + check_compression(word, reduced, maps) + return reduced, maps + + +def check_compression(word, reduced, maps): + h, r, t = maps["active"], maps["roles"], maps["rank"] + require(0 <= h <= r and 0 <= t <= r - h, "invalid map dimensions") + rows, columns = maps["F_rows"], maps["G_columns"] + require(len(rows) == len(columns) == t, "map shape mismatch") + require(all(0 <= v < 1 << (r - h) for v in [*rows, *columns]), "map outside workspace") + require(all(dot(row, col) == (i == j) + for i, row in enumerate(rows) for j, col in enumerate(columns)), "FG is not identity") + ub = basis(f.x >> h for f in word) + vb = basis(f.y >> h for f in word) + require(len(basis(evaluate_rows(vb, u) for u in ub)) == t, "incorrect pairing rank") + require(maps["column_span_rank"] == len(ub) and maps["row_span_rank"] == len(vb), + "incorrect span dimensions") + mask = (1 << h) - 1 + all_reduced = [Factor(f.label, (f.x & mask) | (evaluate_rows(rows, f.x >> h) << h), + (f.y & mask) | (evaluate_rows(columns, f.y >> h) << h)) for f in word] + require(all(dot(a.y, b.x) == dot(ap.y, bp.x) + for a, ap in zip(word, all_reduced) for b, bp in zip(word, all_reduced)), + "ordered contraction changed") + indices = [i for i, f in enumerate(all_reduced) if f.x and f.y] + require(indices == maps["retained_indices"], "incorrect deleted-factor indices") + require(reduced == [all_reduced[i] for i in indices], "compressed word mismatch") + for i, f in enumerate(word): + if dot(f.x, f.y): + require(i in indices, "idempotent factor was deleted") + + +def group_multiply(g, h): + # Upper triangular coordinates 12,13,14,23,24,34, identity encoded by 0. + return (g ^ h ^ (((g & 1) * ((h >> 3) & 1)) << 1) + ^ ((((g & 1) * ((h >> 4) & 1)) ^ (((g >> 1) & 1) * ((h >> 5) & 1))) << 2) + ^ ((((g >> 3) & 1) * ((h >> 5) & 1)) << 4)) + + +GROUP = [[group_multiply(g, h) for h in range(64)] for g in range(64)] +COEFFICIENTS = {"a": 1 ^ (1 << 1), "b": 1 ^ (1 << 8), "c": 1 ^ (1 << 32)} + + +def bits(value): + while value: + bit = value & -value + yield bit.bit_length() - 1 + value ^= bit + + +def ring_multiply(a, b): + result = 0 + for g in bits(a): + for h in bits(b): + result ^= 1 << GROUP[g][h] + return result + + +def identity(roles): + return [[int(i == j) for j in range(roles)] for i in range(roles)] + + +def word_matrix(word, roles, coefficients=COEFFICIENTS): + result = identity(roles) + for factor in word: + values = [] + for row in result: + v = 0 + for j in bits(factor.x): + v ^= row[j] + values.append(ring_multiply(v, coefficients[factor.label])) + for i in range(roles): + for j in bits(factor.y): + result[i][j] ^= values[i] + return result + + +def sandwich(matrix, maps): + h, r, t = maps["active"], maps["roles"], maps["rank"] + rows = [1 << i for i in range(h)] + [v << h for v in maps["F_rows"]] + columns = [1 << i for i in range(h)] + [v << h for v in maps["G_columns"]] + require(len(matrix) == r and all(len(row) == r for row in matrix), "matrix shape") + result = [[0] * (h + t) for _ in range(h + t)] + for i, row in enumerate(rows): + for j, col in enumerate(columns): + for a in bits(row): + for b in bits(col): + result[i][j] ^= matrix[a][b] + return result + + +def target(roles): + require(roles >= 2, "two target roles are required") + matrix = identity(roles) + matrix[0][0], matrix[1][1] = 1 << 4, 1 << 6 + return matrix + + +def direct_word(): + return [Factor(g, 1, 1) for g in "abcbabcb"] + [Factor(g, 2, 2) for g in "acbabc"] diff --git a/research/register-pairing-compression/sources/mixed-middle.md b/research/register-pairing-compression/sources/mixed-middle.md new file mode 100644 index 0000000000..e6a7c24d20 --- /dev/null +++ b/research/register-pairing-compression/sources/mixed-middle.md @@ -0,0 +1,231 @@ +# One z target and one uz target cost exactly fourteen calls + +This is a computer-assisted theorem in the formal UT4 model. The written rank +argument quantifies arbitrary finite dirty workspace and word length. The finite +census excludes the one remaining two-role call split. Neither part establishes +a physical supplier, a rational-frame translation, or a multiplication exponent. + +## Model and predecessor boundary + +Let `G=UT4(F2)` and `R=F2[G]`. Write + +``` +a=I+E12, b=I+E23, c=I+E34, +u=I+E13, v=I+E24, z=I+E14. +``` + +Every paid factor is `D_N(g)=I+([g]+1)N`, where `g` is one of `a,b,c` and +`N=xy^T` is a nonzero binary rank-one matrix on the scalar roles. Both +idempotent and nilpotent couplings are allowed. Every occurrence, including +restoration, costs one call. All roles have arbitrary initial data. Extra roles +must finish as the identity operator, with no contamination of target outputs. + +Scalar GL operations are optimistically free. Conjugating them into the paid +couplings preserves rank one. Augmentation sends every paid factor and the target +to identity, so the scalar operation remaining at the end is identity. There are +no free address maps, clean roles, COPY, ERASE, higher-rank paid operations, or +unpaid inverses. Equality means the full formal group-algebra operator, not its +image at a sampled address size. + +Gareth Davidson's [PR2027](https://github.com/CrocSwap/integer-mult-bounds/pull/2027) +proves the separate-letter bounds below and their sharpness when there are no +pure-central roles. Its explicit next question is one z role and one uz role. +ToikY's [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662) +supplies the central-target middle quotient; PR1680 supplies the workspace-span +compression method. We use those methods and Aaron Wang's PR1690 profile-screen +method. The new statements are the mixed middle bound, its application to this +endpoint, and the exact exclusion of its thirteen-call split. + +## A mixed middle bound + +For the more general diagonal endpoint + +``` +diag([u^s_i v^t_i z^h_i]), +``` + +let `S,T,H` denote the binary diagonal matrices with entries `s_i,t_i,h_i`. +Let `d` count coordinates with at least one of these entries nonzero, and `k` +count pure-central coordinates, where `s_i=t_i=0,h_i=1`. + +**Lemma.** Every such word has + +``` +n_b >= 2d+k. +``` + +This strengthens PR2027's `n_b>=2d` by charging each pure-central role once more. +It is only a necessary bound for the general family, not a general sharp tariff. + +Use the predecessor quotient + +``` +Q=F2/(A^2,B^2,C^2,AC-CA, all terms of degree at least four). +``` + +Its seventeen-element monomial basis and its group homomorphism are independently +reconstructed in `verify.py`. The program checks all 4,096 group products and +all 4,913 basis associativity triples. In this quotient, + +``` +u maps to 1+AB+BA+ABA+BAB, +v maps to 1+BC+CB+BCB+CBC, +z maps to 1+ABC+ACB+BAC+CBA. +``` + +Products of nonconstant root terms have degree at least four. Thus the endpoint +has coefficients `S` on the four u terms, `T` on the four v terms, and `H` on +the four z terms. + +Number the b calls in chronological product order. Write their couplings as +`x_j y_j^T`. Let `P_j` be the sum of a couplings before call j and `Q_j` the +sum of c couplings after it. Define + +``` +X=[x_j], Y=[y_j^T], U=[P_j x_j], V=[y_j^T Q_j]. +``` + +Here X,U have shape `r by n_b`; Y,V have shape `n_b by r`. Ordered expansion +without commuting scalar matrices gives + +``` +XY=0, UY=S, XV=T, UV=H. (1) +``` + +PR2027's same-label span argument applies unchanged. Coefficients BA,BC,BAC +force the column span of X to contain the union of the active target coordinates. +AB,CB,ACB force the analogous row span of Y. The two representatives BAC and +BCA both start with B; ACB and CAB both end with B. Consequently + +``` +rank X >= d, rank Y >= d. (2) +``` + +Let pi delete output coordinates in the support of S, and restrict the input +to `ker T`. By (1), `V(ker T)` is contained in `ker X`, and `pi U` annihilates +`im Y`. Thus `pi H` restricted to `ker T` factors through + +``` +ker X / im Y. +``` + +Its rank is exactly k because H is diagonal. Since XY=0, the quotient has +dimension `n_b-rank X-rank Y`. Therefore that dimension is at least k; (2) +proves `n_b>=2d+k`. This argument includes all restored identity roles. + +For comparison, the necessary four-matrix relaxation is attained at five middle +columns for one z and one uz role. One explicit fixture is + +``` +X = [1 1 1 0 1; 0 0 0 1 1], +Y = [1 0; 1 0; 0 1; 0 1; 0 1], +U = [0 0 1 1 0; 0 0 0 0 1], +V = [1 0; 0 0; 1 1; 0 1; 0 1]. +``` + +All X columns and Y rows are nonzero; both ranks are two. These matrices satisfy +(1) with `S=diag(0,1), T=0, H=I2`. They do not supply P_j,Q_j from paid +chronological paths or satisfy every quotient coefficient. In particular, this +fixture must not be described as a thirteen-call word. The tests check it and +reject a changed V entry. + +## Compression of the only possible thirteen-call word + +The desired endpoint is + +``` +diag([z],[uz],I on every other role). +``` + +Here d=2 and k=1. PR2027's outer bounds give `n_a,n_c>=4`; the new middle bound +gives `n_b>=5`. Fewer than thirteen calls are impossible. At thirteen calls the +counts must be exactly `(4,5,4)`. + +For each outer letter, its column and row spans contain the two active coordinate +directions. Their ranks sum to at most its call count because the first-order +sum is zero. Hence both ranks equal two. For b, the proof above gives +`rank X+rank Y<=n_b-k=4`, so both ranks also equal two. + +Every one of these six spans is therefore exactly the active two-coordinate +plane. Each x_j and y_j is supported in that plane. Every coupling is its active +2x2 block, with zeros elsewhere. The entire word is already block diagonal with +identity on the dirty complement. Restriction to two roles preserves every +nonzero factor and its letter. No extra role, regardless of its initial dirty +value, can rescue a thirteen-call word. This is a special exact-span application +of PR1680's method, not a claim for longer words or arbitrary target families. + +## Complete two-role exclusion + +On two roles there are nine nonzero rank-one binary couplings. The first-order +coefficient of each letter is zero. The census covers all `(4,5,4)` words as +follows, without scalar conjugation or permutation symmetry reductions. + +1. Enumerate all `9^5=59049` ordered middle sequences. Retain the 3,600 with zero + sum. Every legal endpoint must be among them. +2. Enumerate all `9^4=6561` outer sequences. Retain those with zero sum. Place + the four calls into all six chronological gaps around the five middle calls, + using all 126 nondecreasing gap assignments. Retain every concrete realization + and its prefix-sum profile. There are 9,721 distinct profiles. +3. For a profile P, the four one-sided coefficients are + + ``` + AB = sum P_j B_j, BA = sum B_j P_j, + ABA = sum P_j B_j P_j, + BAB = sum_{j=2**. +This does not prove the optimal weighted tariff, nor exclude longer words with +fewer b calls and more outer calls. It does not implement a physical address +alphabet or improve the selected multiplication bound. + +## Credit and remaining obligations + +Credit Gareth Davidson/PR2027 for the mixed family, sharp noncentral tariffs, +span unions and the explicit z/uz handoff; ToikY/PR1662 and PR1680 for the quotient +and compression methods; Aaron Wang/PR1690 for the profile-screen algorithm; +steph4n-gh/PR1573, Arham Tahir/PR1589 and Hanson Sun/PR1607 for the retained +zero-sum and coefficient-span lineage. All predecessor files remain unchanged. + +The finite homomorphism and exclusion census are premises of this +computer-assisted theorem. Lean/kernel verification, physical letters, +rational-frame conversion, common-label realization, hosting, precision/tape, +all-size compilation and outer analytic transfer remain unproved here. +Apache-2.0. No literature-priority or independent human review claim is made. diff --git a/research/register-pairing-compression/sources/weighted-boundary.md b/research/register-pairing-compression/sources/weighted-boundary.md new file mode 100644 index 0000000000..d5ba9d06c0 --- /dev/null +++ b/research/register-pairing-compression/sources/weighted-boundary.md @@ -0,0 +1,194 @@ +# The weighted boundary for one z and one uz target + +In the full formal model below, every fourteen-call word for +`diag([z],[uz],I_rest)` has counts `(n_a,n_b,n_c)=(4,6,4)`, for every finite +number of arbitrary restored dirty roles. In particular, five b calls require +at least ten outer calls. The direct word is therefore optimal at every +nonnegative uniform letter price satisfying `beta <= 2 min(alpha,gamma)`. + +This is a written uniform argument plus complete finite quotient censuses. +It extends Nick Petalas's [PR2175](https://github.com/CrocSwap/integer-mult-bounds/pull/2175) +at `1d943bc9e0718c8a2f15e1d0a22b73ad528ef0ca`, whose unit optimum fourteen +and direct upper word are retained results. The new cases are its explicit +weighted handoff, `(5,5,4)` and `(4,5,5)`. The span, quotient and profile methods +retain the PR2027/1662/1680/1690 attribution; no new rank principle is claimed. + +## Model and inherited algebra + +Let `G=UT4(F2)`, `R=F2[G]`, and + +``` +a=I+E12, b=I+E23, c=I+E34, +u=I+E13, z=I+E14. +``` + +On any finite `r>=2` scalar roles, every paid call is +`D_N(g)=I+([g]+1)N`, with `g in {a,b,c}` and `N=xy^T` nonzero of rank one +over F2. Both idempotent and nilpotent couplings are allowed. Each factor is +an involution, since `([g]+1)^2=0`. Every occurrence, including restoration, +is charged. Arbitrary scalar GL mixing is optimistically free: conjugate it +into the couplings and normalize the final scalar map by augmentation. +The target and all paid factors augment to I, so that final map is I. + +There are no free address maps, initialized extra roles, COPY, ERASE, +higher-rank unit calls or unpriced inverses. Every extra role starts arbitrary +dirty and must end as its own identity, without contaminating either target. +Equality is in `Mat_r(R)`, not a finite sample of input bits. The formal price +does not implement a physical recursive child. + +Use the retained quotient + +``` +Q=F2/(A^2,B^2,C^2, AC-CA, all monomials of degree >=4). +``` + +It has seventeen monomial basis elements. The retained checker verifies its +associativity on all `17^3=4913` triples and the map `a,b,c -> 1+A,1+B,1+C` +on all `64^2=4096` group products. The separate checker reconstructs the +quotient by commutation orbits of all forty words of degree at most three, +and the group by literal four-by-four binary matrices. A fixed ring map +extends entrywise to matrices of every finite role count. + +The images are + +``` +u -> 1+AB+BA+ABA+BAB, +z -> 1+ABC+ACB+BAC+CBA. +``` + +Write `P=diag(1,1,0,...)` and `S=diag(0,1,0,...)`. Nonconstant products of +these root images have degree at least four, so the target has coefficient S +at `AB,BA,ABA,BAB`, P at `ABC,ACB,BAC,CBA`, and zero elsewhere except I. + +For each label g, collect its coupling columns in X_g and rows in Y_g. +The zero first-degree coefficient gives `X_g Y_g=0`, and hence +`n_g >= rank X_g + rank Y_g`. All six spans contain the active two-coordinate +plane: use the first and last factors contributing to ABC and CBA for a,c, +and BAC and ACB for b. The commuting representatives BCA and CAB still start +or end with b, respectively; no scalar matrices are commuted. + +For the b calls, set X=X_b, Y=Y_b. Let U have columns `A_j x_j`, where A_j is +the sum of earlier a couplings, and let V have rows `y_j^T C_j`, where C_j is +the sum of later c couplings. Chronological expansion gives + +``` +XY=0, UY=S, XV=0, UV=P. +``` + +Delete the second output coordinate with pi. Then `pi U` annihilates im Y +and V maps into ker X. Thus `pi P = (pi U)V`, of rank one, factors through +`ker X / im Y`. It follows that + +``` +n_b >= rank X_b + rank Y_b + 1. +``` + +This is PR2175's mixed-middle argument specialized to z/uz. In particular +`n_a>=4`, `n_b>=5`, `n_c>=4`, for every word length and every finite r. + +## Compression at fourteen calls + +Sum the three label inequalities. For a word of length L, + +``` +L >= 1 + sum_g(rank X_g + rank Y_g) >= 13. +``` + +If `L<=14`, the six integer ranks have total excess at most one above two. +Every span except possibly one equals the corresponding active plane by +containment. If the exceptional span is a column span, all row spans are +active; hence `NP=N` for every coupling. If it is a row span, `PN=N` for +every coupling. With no exception, both statements hold. This is ToikY's +PR1680 common-orientation argument applied to the mixed-middle inequality. + +Split roles into the active plane and the dirty complement. All factors are +simultaneously block lower triangular or simultaneously block upper triangular. +Projection to the active corner is multiplicative over the full noncommutative +ring R: the discarded cross-block product is zero. The projected product is +therefore `diag([z],[uz])`. A projected coupling is an outer product and has +rank one or zero. Delete zero identity factors; each letter count can only +decrease. This proves compression uniformly in r and arbitrary dirty inputs. +Opposite orientations on different factors would invalidate the projection; +an explicit rejected feedback pair is checked in `controls.py`. + +The only possible thirteen-call split is `(4,5,4)`. Its complete quotient +exclusion is replayed byte for byte from PR2175's receipt. Thus no projected +fourteen-call word can lose a factor: that would give a word of at most thirteen +calls. The only remaining fourteen-call splits are `(4,6,4)`, `(5,5,4)` and +`(4,5,5)`, with their exact counts preserved by compression. + +## Complete new two-role censuses + +There are nine nonzero binary rank-one couplings on two roles. Each legal +endpoint has zero first-degree sum for each label. Enumerate all `9^5` middle +sequences and retain their 3600 zero-sum sequences. For each outer count four +or five, enumerate every zero-sum coupling sequence and every nondecreasing +assignment of its calls to the six gaps around those five middle calls. + +| Outer calls | Zero-sum sequences | Gap assignments each | Realizations | Distinct profiles | +| ---: | ---: | ---: | ---: | ---: | +| 4 | 441 | 126 | 55,566 | 9,721 | +| 5 | 3,600 | 252 | 907,200 | 47,521 | + +The profile stores each outer prefix sum at the five b calls; all concrete +realizations are retained. The predecessor's AB/BA/ABA/BAB equations for a, +and CB/BC/CBC/BCB equations for c, hold for either outer length. Their target +values are S and zero respectively. Zero total outer sum identifies the +suffix sums needed by the c screen. Transported column/row keys impose +`ABC=CBA=P` by exact parity equations; every compatible profile pair remains. + +For each pair, expand every retained realization and every A/C interleaving +within each gap, then evaluate all seventeen quotient coefficients. Every +concrete word has a unique middle sequence, two outer sequences, gap assignments +and within-gap interleaving. The enumeration covers these without symmetry or +heuristic pruning. All prior screens impose necessary equations only. + +| Split (a,b,c) | A / C profile passes | Key pairs | Profile pairs | Expanded words | Q survivors | +| --- | ---: | ---: | ---: | ---: | ---: | +| (4,5,4), retained control | 89,052 / 1,201,320 | 68 | 152 | 5,536 | 0 | +| (5,5,4), new | 236,224 / 1,201,320 | 144 | 944 | 211,968 | 0 | +| (4,5,5), new | 89,052 / 2,899,368 | 136 | 912 | 209,920 | 0 | + +For the new domains, 125,636 / 117,308 words first fail AC and 86,332 / 92,612 +first fail ACB. Full expansion digests are in RESULT.json. Quotient rejection +is sufficient to reject a formal identity; no construction is accepted from +this nonfaithful image. Independent subsequence expansion checks all 20,440 +short words and the planted long-word fixtures. The five-call catalogue is +separately checked for complete, duplicate-free gap coverage. + +Consequently every fourteen-call full formal word on any finite dirty workspace +has counts `(4,6,4)`. The credited coordinate word `abcbabcb` on the z role +and `acbabc` on the uz role attains these counts. The full group-algebra check, +192 faithful regular columns including a dirty spectator, fourteen one-call +omissions and a wrong-letter control are retained/replayed. + +## Weighted implication for arbitrary word lengths + +Every word has `n_a,n_c>=4` and `n_b>=5`. If `n_b=5` and `n_a+n_c<=9`, its +length is at most fourteen, and the preceding exclusions apply. Therefore +every five-b word has `n_a+n_c>=10`, with no bound on r or total length. + +For arbitrary nonnegative real letter prices alpha,beta,gamma, every complete +word costs at least + +``` +min(4 alpha + 6 beta + 4 gamma, + 4 alpha + 5 beta + 4 gamma + 2 min(alpha,gamma)). +``` + +The first branch covers `n_b>=6`. For `n_b=5`, the outer calls beyond the +four-per-label floor number at least two and each costs at least +`min(alpha,gamma)`, giving the second branch. This is a necessary lower +envelope; it asserts no five-b construction attaining its second branch. + +When `beta<=2 min(alpha,gamma)`, the direct `(4,6,4)` bill is the smaller +branch and is attained. Thus it is the exact optimum on that entire price +cone, including its boundary and zero prices. At `(alpha,beta,gamma)=(1,2,1)` +the exact price is twenty. Outside the cone, for example `(1,3,1)`, the lower +envelope is twenty-five and the direct price is twenty-six; sharpness is open. + +No claim is made for all weighted prices, larger-slack workspace compression, +native/compiler realization, rational-frame transfer, physical hosting, +precision/reserves, or a multiplication exponent. The result is exact within +the stated formal alphabet, with substantial OpenAI Codex assistance and no +proof-kernel or independent human review. diff --git a/research/register-pairing-compression/verify.py b/research/register-pairing-compression/verify.py new file mode 100644 index 0000000000..5dae7cd4ec --- /dev/null +++ b/research/register-pairing-compression/verify.py @@ -0,0 +1,423 @@ +#!/usr/bin/env python3 +"""Finite corroboration and boundary controls, not proof of the uniform lemma. +Gareth Davidson / @bitplane, substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from copy import deepcopy +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("pairing_core", HERE / "compression.py") +c = importlib.util.module_from_spec(spec) +sys.modules[spec.name] = c +spec.loader.exec_module(c) +require = c.require + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def source_check(package=HERE): + source = json.loads((package / "SOURCES.json").read_text()) + checked = [] + for item in source["files"]: + if item["usage"] != "input": + continue + data = (package.parents[1] / item["path"]).read_bytes() + require(sha(data) == item["sha256"], "changed live proof input: " + item["path"]) + require(hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + == item["git_blob"], "changed Git source blob") + checked.append(item["path"]) + for item in source["archived_proofs"]: + data = (package / item["path"]).read_bytes() + require(sha(data) == item["sha256"], "changed archived proof: " + item["path"]) + require(hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + == item["git_blob"], "changed archived source blob") + checked.append(item["path"]) + return sorted(checked) + + +def bindings(package=HERE): + return {name: sha((package / name).read_bytes()) + for name in ("compression.py", "verify.py", "PROOF.md", "SOURCES.json")} + + +def preflight(package=HERE): + source_check(package) + task = json.loads((package / "TASK.json").read_text()) + expected = json.loads((package / "RESULT.json").read_text()) + require(sha(canonical(expected)) == task["receipt_sha256"], "changed mathematical receipt") + require(expected["bindings"] == bindings(package), "changed proof or verifier binding") + return expected + + +def all_subspaces(width): + found = {frozenset({0})} + frontier = list(found) + while frontier: + current = frontier.pop() + for v in range(1, 1 << width): + if v not in current: + enlarged = frozenset(current | {u ^ v for u in current}) + if enlarged not in found: + found.add(enlarged) + frontier.append(enlarged) + return sorted(found, key=lambda s: (len(s), sorted(s))) + + +def set_basis(subspace): + result, built = [], frozenset({0}) + for v in sorted(subspace): + if v not in built: + result.append(v) + built = frozenset(built | {u ^ v for u in built}) + require(built == subspace, "subspace basis did not generate its input") + return result + + +def oracle_pairing_rank(uspace, vspace): + # Image enumeration is separate from the core's Gaussian elimination. + image = {tuple((u & v).bit_count() % 2 for v in sorted(vspace)) for u in uspace} + require(len(image) & (len(image) - 1) == 0, "pairing image is not a binary space") + return len(image).bit_length() - 1 + + +def compare_word(word, active, roles, coefficients=c.COEFFICIENTS): + reduced, maps = c.compress(word, active, roles) + require(c.word_matrix(reduced, active + maps["rank"], coefficients) + == c.sandwich(c.word_matrix(word, roles, coefficients), maps), + "full noncommutative product identity failed") + before, after = Counter(f.label for f in word), Counter(f.label for f in reduced) + require(all(after[g] <= n for g, n in before.items()), "letter cost increased") + return reduced, maps + + +def subspace_census(): + rows, digest = [], hashlib.sha256() + coefficients = {"a": (1 << 1) ^ (1 << 8) ^ (1 << 13), + "b": 1 ^ (1 << 32) ^ (1 << 6), "c": (1 << 3) ^ (1 << 37)} + for width, expected in enumerate((1, 2, 5, 16, 67)): + spaces = all_subspaces(width) + require(len(spaces) == expected, "incomplete binary subspace enumeration") + histogram = Counter() + for uspace in spaces: + for vspace in spaces: + ub, vb = set_basis(uspace), set_basis(vspace) + word = [c.Factor("abc"[i % 3], 1 | (u << 1), 1 | (v << 1)) + for i, (u, v) in enumerate(itertools.zip_longest(ub, vb, fillvalue=0))] + reduced, maps = compare_word(word, 1, width + 1, coefficients) + rank = oracle_pairing_rank(uspace, vspace) + require(maps["rank"] == rank, "pairing image oracle disagrees") + histogram[rank] += 1 + digest.update(canonical([width, sorted(uspace), sorted(vspace), maps, + [[f.label, f.x, f.y] for f in reduced]])) + rows.append({"workspace": width, "subspaces": expected, "pairs": expected ** 2, + "pairing_rank_histogram": dict(sorted(histogram.items()))}) + return {"domains": rows, "total_pairs": sum(r["pairs"] for r in rows), + "transcript_sha256": digest.hexdigest()} + + +POSITIONS = ((0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)) + + +def literal_matrix(g): + matrix = [[int(i == j) for j in range(4)] for i in range(4)] + for bit, (i, j) in enumerate(POSITIONS): + matrix[i][j] = g >> bit & 1 + return matrix + + +def literal_product(g, h): + a, b = literal_matrix(g), literal_matrix(h) + out = [[sum(a[i][k] * b[k][j] for k in range(4)) % 2 for j in range(4)] for i in range(4)] + return sum(out[i][j] << bit for bit, (i, j) in enumerate(POSITIONS)) + + +LITERAL_GROUP = [[literal_product(g, h) for h in range(64)] for g in range(64)] + + +def faithful_columns(word, roles, matrix, coefficients=c.COEFFICIENTS): + # Separate left regular representation on EVERY basis vector. Product + # factors act in reverse order. No matrix-product helper is called. + for input_role in range(roles): + for address in range(64): + vector = [0] * roles + vector[input_role] = 1 << address + for f in reversed(word): + total = 0 + for j in range(roles): + if f.y >> j & 1: + total ^= vector[j] + delta = 0 + for g in range(64): + if coefficients[f.label] >> g & 1: + for h in range(64): + if total >> h & 1: + delta ^= 1 << LITERAL_GROUP[g][h] + for j in range(roles): + if f.x >> j & 1: + vector[j] ^= delta + expected = [] + for output_role in range(roles): + value = 0 + for g in range(64): + if matrix[output_role][input_role] >> g & 1: + value ^= 1 << LITERAL_GROUP[g][address] + expected.append(value) + require(vector == expected, "literal faithful column differs") + return roles * 64 + + +def pair_census(): + histogram, naive_failures, digest = Counter(), 0, hashlib.sha256() + for x, y, z, w in itertools.product(range(1, 8), repeat=4): + word = [c.Factor("a", x, y), c.Factor("b", z, w)] + reduced, maps = compare_word(word, 1, 3) + histogram[maps["rank"]] += 1 + naive = [c.Factor(f.label, f.x & 1, f.y & 1) for f in word if f.x & 1 and f.y & 1] + naive_failures += c.word_matrix(naive, 1)[0][0] != c.word_matrix(word, 3)[0][0] + digest.update(canonical([x, y, z, w, maps["rank"], [[f.label, f.x, f.y] for f in reduced]])) + require(naive_failures > 0, "naive projection control did not exercise feedback") + return {"ordered_pairs": 7 ** 4, "pairing_rank_histogram": dict(sorted(histogram.items())), + "naive_projection_failures": naive_failures, "transcript_sha256": digest.hexdigest()} + + +def dirty_change_basis(word, active, width): + result = list(word) + for i in range(width): + if width < 2: + break + j = (i + 1) % width + ii, jj = active + i, active + j + result = [c.Factor(f.label, f.x ^ (((f.x >> jj) & 1) << ii), + f.y ^ (((f.y >> ii) & 1) << jj)) for f in result] + return result + + +def endpoint_fixtures(): + fixtures, columns, deleted, idem, nilpotent = [], 0, 0, 0, 0 + for width in range(7): + for rank in range(width + 1): + word = c.direct_word() + noise = [c.Factor("abc"[j % 3], 1 | (1 << (j + 2)), + 2 | ((1 << (j + 2)) if j < rank else 0)) for j in range(width)] + # Every letter factor is an involution; this is an exact relator. + word[5:5] = noise + list(reversed(noise)) + word = dirty_change_basis(word, 2, width) + reduced, maps = compare_word(word, 2, width + 2) + require(maps["rank"] == rank, "fixture pairing rank") + require(c.word_matrix(word, width + 2) == c.target(width + 2), "dirty endpoint not restored") + require(c.word_matrix(reduced, 2 + rank) == c.target(2 + rank), "compressed dirty endpoint") + columns += faithful_columns(word, width + 2, c.target(width + 2)) + columns += faithful_columns(reduced, 2 + rank, c.target(2 + rank)) + for f in word: + if c.dot(f.x, f.y): + idem += 1 + else: + nilpotent += 1 + deleted += len(word) - len(reduced) + fixtures.append({"roles": width + 2, "rank": rank, "length": len(word), + "compressed_length": len(reduced)}) + # Both spans leave H, but their dirty pairing vanishes: neither common + # block orientation from PR1680 holds, yet all four noise factors vanish. + orthogonal = [c.Factor("a", 1, 8), c.Factor("b", 4, 1)] + word = orthogonal + list(reversed(orthogonal)) + c.direct_word() + reduced, maps = compare_word(word, 2, 4) + require(maps["rank"] == 0 and maps["column_span_rank"] == maps["row_span_rank"] == 1, + "orthogonal bidirectional workspace fixture") + require(len(reduced) == 14 and c.word_matrix(word, 4) == c.target(4), "zero factors not removed") + columns += faithful_columns(word, 4, c.target(4)) + deleted += 4 + require(idem > 0 and nilpotent > 0 and deleted > 0, "missing coupling boundary cases") + return {"fixtures": fixtures, "orthogonal_bidirectional_fixture": True, + "faithful_columns": columns, "deleted_nilpotent_factors": deleted, + "idempotent_occurrences": idem, "nilpotent_occurrences": nilpotent} + + +def expect_failure(function, fragment): + try: + function() + except (ValueError, OSError) as exc: + require(fragment in str(exc), "wrong failure: " + str(exc)) + else: + raise ValueError("control unexpectedly accepted: " + fragment) + + +def semantic_controls(): + controls = [] + word = [c.Factor("a", 1, 2), c.Factor("b", 2, 1)] + reduced, maps = compare_word(word, 1, 2) + require(maps["rank"] == 1 and c.word_matrix(word, 2)[0][0] != 1, "feedback is absent") + controls.append("naive active-corner projection loses feedback") + for field in ("F_rows", "G_columns"): + bad = deepcopy(maps) + bad[field] = [0] + expect_failure(lambda: c.check_compression(word, reduced, bad), "FG is not identity") + controls.append("wrong " + field) + bad = deepcopy(maps) + bad.update(rank=0, F_rows=[], G_columns=[]) + expect_failure(lambda: c.check_compression(word, [], bad), "incorrect pairing rank") + controls.append("incorrect zero pairing rank") + # FG=I alone is insufficient: choose an unrelated ambient direction. + reduced, maps = c.compress(word, 1, 3) + bad = deepcopy(maps) + bad.update(F_rows=[2], G_columns=[2]) + expect_failure(lambda: c.check_compression(word, reduced, bad), "ordered contraction changed") + controls.append("FG identity without contraction preservation") + transposed = [c.Factor(f.label, f.y, f.x) for f in reduced] + expect_failure(lambda: c.check_compression(word, transposed, maps), "compressed word mismatch") + controls.append("transposed coupling") + bad = deepcopy(maps) + bad["retained_indices"] = [0] + expect_failure(lambda: c.check_compression(word, reduced, bad), "deleted-factor indices") + controls.append("unpriced deletion") + for f, name in ((c.Factor("a", 4, 4), "unrestored dirty role"), + (c.Factor("a", 1, 4), "dirty input contaminates target")): + actual = c.word_matrix(c.direct_word() + [f], 3) + require([row[:2] for row in actual[:2]] == c.target(2), "active corner fixture") + expect_failure(lambda: require(actual == c.target(3), "full endpoint differs"), "full endpoint differs") + controls.append(name) + require(c.ring_multiply(c.COEFFICIENTS["a"], c.COEFFICIENTS["b"]) + != c.ring_multiply(c.COEFFICIENTS["b"], c.COEFFICIENTS["a"]), "coefficients commute") + controls.append("ordered noncommutative coefficients") + direct = c.direct_word() + expect_failure(lambda: require(c.word_matrix(direct[:-1], 2) == c.target(2), "omitted call"), "omitted call") + direct[0] = c.Factor("c", 1, 1) + expect_failure(lambda: require(c.word_matrix(direct, 2) == c.target(2), "wrong letter"), "wrong letter") + controls.extend(["omitted restoration call", "wrong paid letter"]) + expect_failure(lambda: c.compress([c.Factor("a", 0, 1)], 1, 2), "nonzero") + expect_failure(lambda: c.compress([c.Factor("a", 4, 1)], 1, 2), "within the role") + controls.extend(["zero original factor", "out-of-domain role"]) + return controls + + +def excess_profiles(budget, parts): + if parts == 0: + yield () + else: + for first in range(budget + 1): + for rest in excess_profiles(budget - first, parts - 1): + yield (first,) + rest + + +def ut4_budget(): + # Integer consequences of inherited inequalities, NOT a replay of the + # PR2175/2314 exhaustive exclusion certificates. + rows = [] + for length in range(13, 25): + excess, cases, maximum = length - 13, 0, 0 + for e in excess_profiles(excess, 6): + u, v = sum(e[::2]), sum(e[1::2]) + require(min(u, v) <= excess // 2, "excess does not bound pairing rank") + maximum = max(maximum, min(u, v)) + cases += 1 + require(maximum == excess // 2, "relaxation endpoint was not attained") + rows.append({"length": length, "span_profiles": cases, "role_bound": 2 + maximum}) + cheaper = [] + for a, b, cc in itertools.product(range(27), repeat=3): + if a >= 4 and cc >= 4 and b >= 5 and (b != 5 or a + cc >= 10) and a + 3 * b + cc < 26: + cheaper.append([a, b, cc]) + require(sorted(cheaper) == [[4, 5, 6], [5, 5, 5], [6, 5, 4]], "weighted candidate splits") + require(all(sum(s) == 15 and s[0] + 3 * s[1] + s[2] == 25 for s in cheaper), "fifteen-call budget") + return {"span_relaxations": rows, "price": [1, 3, 1], "direct_price": 26, + "only_cheaper_count_splits": sorted(cheaper), "cheaper_price": 25, + "maximum_roles_for_cheaper_word": 3, "fifteen_call_existence_decided": False} + + +def run(): + sources = source_check() + require(LITERAL_GROUP == c.GROUP, "literal UT4 multiplication disagrees") + for g in (1, 8, 32): + require(c.GROUP[g][g] == 0, "letter is not an involution") + print("checked source pins and all 4096 literal group products", flush=True) + subspaces, pairs = subspace_census(), pair_census() + print("checked 4775 subspace pairs and 2401 ordered rank-one pairs", flush=True) + fixtures, controls, budget = endpoint_fixtures(), semantic_controls(), ut4_budget() + return {"schema_version": 1, "bindings": bindings(), "source_inputs": sources, + "literal_group_products": 4096, "subspace_census": subspaces, + "rank_one_pair_census": pairs, "full_endpoint_fixtures": fixtures, + "semantic_controls": controls, "ut4_consequence": budget, + "scope": "Finite corroboration of PROOF.md; no fifteen-call census, native supplier, or kappa claim."} + + +def disk_controls(): + preflight() + with tempfile.TemporaryDirectory(prefix="pairing-compression-controls-") as tmp: + root = Path(tmp) + package = root / "research" / HERE.name + shutil.copytree(HERE, package) + # The source may be a read-only export. Only this private temporary + # copy becomes writable for deliberate corruption controls. + package.chmod(0o755) + for path in package.rglob("*"): + path.chmod(0o755 if path.is_dir() else 0o644) + source = json.loads((HERE / "SOURCES.json").read_text()) + for item in source["files"]: + if item["usage"] == "input": + dst = root / item["path"] + dst.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(HERE.parents[1] / item["path"], dst) + command = [sys.executable, "-I", "-O", "-B", str(package / "verify.py"), "--preflight"] + good = subprocess.run(command, cwd=root, capture_output=True, text=True) + require(good.returncode == 0, "Git-free relocated preflight failed: " + good.stderr) + targets = [(root / next(i["path"] for i in source["files"] if i["usage"] == "input"), "changed live proof"), + (package / source["archived_proofs"][0]["path"], "changed archived proof"), + (package / "PROOF.md", "changed proof or verifier binding"), + (package / "RESULT.json", "changed mathematical receipt")] + for path, marker in targets: + original = path.read_bytes() + if path.name == "RESULT.json": + value = json.loads(original) + value["ut4_consequence"]["maximum_roles_for_cheaper_word"] = 2 + path.write_text(json.dumps(value)) + else: + path.write_bytes(original + b"\ncorrupted proof input\n") + result = subprocess.run(command, cwd=root, capture_output=True, text=True) + require(result.returncode != 0 and marker in result.stderr, "disk fault was not rejected: " + marker) + path.write_bytes(original) + print("PASS_PAIRING_COMPRESSION_DISK_CONTROLS mutations=4 relocated_preflight=1") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + mode = parser.add_mutually_exclusive_group() + mode.add_argument("--write-result", type=Path, help="write to a new, unoccupied path") + mode.add_argument("--preflight", action="store_true") + mode.add_argument("--controls", action="store_true") + args = parser.parse_args() + if args.preflight: + preflight() + print("PASS_PAIRING_COMPRESSION_PREFLIGHT") + return + if args.controls: + disk_controls() + return + expected = None if args.write_result else preflight() + if args.write_result: + require(not args.write_result.exists(), "output path is occupied") + result = run() + if args.write_result: + with args.write_result.open("x") as handle: + json.dump(result, handle, indent=2, sort_keys=True) + handle.write("\n") + else: + require(canonical(result) == canonical(expected), "mathematical receipt differs") + print("PASS_REGISTER_PAIRING_COMPRESSION receipt_sha256=" + sha(canonical(result))) + + +if __name__ == "__main__": + main()