diff --git a/research/ut4-one-slack-workspace/CERTIFICATE.json b/research/ut4-one-slack-workspace/CERTIFICATE.json new file mode 100644 index 0000000000..ceda4f7389 --- /dev/null +++ b/research/ut4-one-slack-workspace/CERTIFICATE.json @@ -0,0 +1,146 @@ +{ + "active_width": 2, + "dropped_factor_occurrences": 2268, + "equal_rank_wrong_target_plane_control": { + "active_basis": [ + 1, + 2 + ], + "candidate_basis": [ + 1, + 4 + ], + "candidate_rank": 2, + "union_rank": 3 + }, + "full_witness_basis_columns": 2560, + "independent": { + "address_bit_positions": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 3 + ], + [ + 0, + 2 + ], + [ + 1, + 3 + ], + [ + 0, + 3 + ] + ], + "basis_order": "64*role+group_code", + "involution_controls": 3, + "method": "literal 4x4 binary matrices and full regular columns", + "mixed_active_feedback_sha256": "0a4012d66773923873a7f1ba87fe7e7de3af73db9708fdd5eb85aaaad22ba860", + "mixed_orientation_rejected": true, + "positive_compressions": [ + { + "active_basis_columns": 128, + "active_corner_sha256": "8c7b90c68fe842a18ec061fe7e812468d23b99bdcf7eb9cf2a2f61c26d6d16b2", + "active_output_rows": 128, + "common_orientation": "both", + "dropped_zero_calls": 0, + "input_calls": 16, + "kept_calls": 16, + "r": 3, + "w": 2 + }, + { + "active_basis_columns": 128, + "active_corner_sha256": "8c7b90c68fe842a18ec061fe7e812468d23b99bdcf7eb9cf2a2f61c26d6d16b2", + "active_output_rows": 128, + "common_orientation": "both", + "dropped_zero_calls": 0, + "input_calls": 18, + "kept_calls": 18, + "r": 3, + "w": 2 + }, + { + "active_basis_columns": 128, + "active_corner_sha256": "b71831d42eda94bf1e3acb9691a1b898e506b6892e610084332839dc6333e070", + "active_output_rows": 128, + "common_orientation": "columns", + "dropped_zero_calls": 1, + "input_calls": 6, + "kept_calls": 5, + "r": 3, + "w": 2 + }, + { + "active_basis_columns": 128, + "active_corner_sha256": "681ab4802ba10d82016a5725c95de6820f4132687afa3193d69b1380b882eb76", + "active_output_rows": 128, + "common_orientation": "rows", + "dropped_zero_calls": 1, + "input_calls": 6, + "kept_calls": 5, + "r": 3, + "w": 2 + } + ], + "product_order_controls": 1, + "schema_version": 1, + "scope": "compression fixtures and known16-call endpoint; no14/15-call attainment claim" + }, + "known_upper_witnesses": 10, + "mixed_feedback_rejected": true, + "new_14_or_15_word": false, + "ordered_triangular_pairs": 7938, + "pair_roles": 3, + "pair_transcript_sha256": "3bebc029cff84bf93dc2fb743aa5ec07daa011945bf85d1bd5af1ce73f393a78", + "quotient": { + "basis": [ + "", + "a", + "b", + "c", + "ab", + "ac", + "ba", + "bc", + "cb", + "aba", + "abc", + "acb", + "bab", + "bac", + "bcb", + "cba", + "cbc" + ], + "basis_associativity_products": 4913, + "central_image": [ + "", + "abc", + "acb", + "bac", + "cba" + ], + "common_kernel_zero": true, + "dimension": 17, + "distinct_group_images": 64, + "group_map_sha256": "9de6cc7ea95a1fd1f78782ba338371acbf0b667de289e787616582d262462443", + "group_products": 4096, + "schema_version": 1, + "scope": "Necessary cubic coefficients; full group-algebra endpoint admission remains separate." + }, + "rank_profile_sha256": "7f1d23fa671360548bfe8fddc8590b3e47d44836ecc3de82d30414491117700d", + "rank_profiles": 105, + "schema_version": 1, + "two_target_minimum": "C_r=C_2 in {14,15,16}; exact value unresolved", + "uniform_scope": "w>=2,L<=7w+1,r>=w; written proof, not finite extrapolation" +} diff --git a/research/ut4-one-slack-workspace/PROOF.md b/research/ut4-one-slack-workspace/PROOF.md new file mode 100644 index 0000000000..4ca867ca78 --- /dev/null +++ b/research/ut4-one-slack-workspace/PROOF.md @@ -0,0 +1,111 @@ +# One-slack workspace compression in the UT4 model + +**Uniform scoped theorem; no new construction or kappa.** The new result is +workspace compression near the retained call lower bound. It uses the span +and quotient lemmas of @ToikY's [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662), +pinned at `01cc02b164ecc4f9d84df3f56a1fe65b88daf390`. + +## Model and normalization + +All scalar coefficients and ranks are over F2. Let `G=UT4(F2)`, with +`a=I+E12`, `b=I+E23`, `c=I+E34`, and central `z=I+E14`. +Work in the full formal algebra `R=F2[G]`. For every finite `r>=w>=2`, a +paid factor is `D_N(g)=I_r+([g]+1)N`, where `g in {a,b,c}` and +`N=x y^T` for nonzero binary r-vectors x,y. Idempotent and nilpotent +rank-one couplings are both admitted. Count every paid occurrence at unit cost. +The required endpoint is `T=I_r+([z]+1)P`, `P=diag(I_w,0)`. +Every role has arbitrary input; the extra r-w roles must be restored exactly. + +Scalar GL_r(F2) maps may be free. Move them to one end by conjugating paid +couplings, which preserves their nonzero rank one and their labels. Augmentation +`[g]->1` sends every paid factor and T to identity, so the remaining free map +is identity. We therefore analyze a normalized paid word without changing its +count or endpoint. There are no other free address operations, clean workspace, +higher-rank paid couplings, COPY or ERASE. All equalities below are formal +operator equalities, not agreement only on inputs with zero extra roles. + +## Retained span premises + +For label g, let X_g collect its column vectors and Y_g its row vectors: +X_g is r by n_g and Y_g is n_g by r. Write u_g=rank(X_g), v_g=rank(Y_g). +The first-order coefficient gives `X_g Y_g=0`, hence `n_g>=u_g+v_g`. +The fixed degree-three quotient used in PR1662 is + +`Q=F2/(a^2,b^2,c^2,ac-ca,all monomials of degree>=4)`. + +Here a,b,c are augmentation variables: group generators map to 1+a,1+b,1+c, +and z maps to `1+abc+acb+bac+cba`. The unchanged pinned quotient implementation +replays all 4096 group products and 4913 basis associativity triples. This is +a fixed-group homomorphism certificate; it does not enumerate r,w or word lengths. +Each of these four target coefficients is P. Ordered scalar expansion gives: + +| Coefficient | Target containment forced by its first/last scalar factor | +|---|---| +| abc | im(P) contained in im(X_a); row(P) contained in row(Y_c) | +| cba | im(P) contained in im(X_c); row(P) contained in row(Y_a) | +| bac, combining BAC and BCA | im(P) contained in im(X_b) | +| acb, combining ACB and CAB | row(P) contained in row(Y_b) | + +No scalar matrices are commuted when the address monomials combine. +Consequently all six ranks are at least w. To recall the stronger middle bound, +number b factors and let A_j be the sum of preceding a couplings and C_j the +sum of following c couplings. Set X=X_b, Y=Y_b, `U=[A_j x_j]`, and let V +have rows `y_j^T C_j`. The B, AB, BC and ABC coefficients give +`XY=UY=XV=0`, `UV=P`. The last map factors through `ker(X)/im(Y)`, of dimension +`n_b-u_b-v_b`; therefore `n_b>=w+u_b+v_b`. These are inherited premises. + +## New one-slack theorem + +For every normalized legal word of length L with endpoint T, if `L<=7w+1`, +there is a legal word on exactly w roles with endpoint `[z]I_w` and length +at most L. More precisely, all normalized couplings share at least one orientation: + +`N P=N for every factor`, or `P N=N for every factor`. + +**Proof.** Summing the retained per-letter inequalities gives + +`L=n_a+n_b+n_c >= w+sum_g(u_g+v_g) >= 7w`. + +All ranks are integers. Thus their total excess over w is at most one. +At most one of the six spans can have dimension w+1; every other span has +dimension w and, by containment, equals the corresponding target span. +If the exceptional span is a column span, every row span equals row(P). +Thus each y satisfies `y^T P=y^T`, giving `N P=N` for every factor. +If it is a row span, every column span equals im(P), giving `P N=N`. +If no span is exceptional, both conclusions hold. The orientation is common +to the whole word, not chosen separately at each factor. + +Split roles as the active w roles followed by the extra r-w roles. In the +first case each paid factor is block lower triangular; in the second it is +block upper triangular. On either common block-triangular algebra, projection +pi to the active corner is multiplicative, including over the noncommutative +ring R: the discarded cross-block product is zero. Therefore +`pi(product D_N(g))=product pi(D_N(g))=pi(T)=[z]I_w`. +Each projected coupling is the outer product of the active components of x,y, +so it has rank one or zero. Retain the former and discard zero identity factors. +This produces the claimed legal word. Each label count can only decrease; +no new preparation, inverse or restoration factor is introduced. This proves +the theorem for arbitrary extra-role inputs, using the full endpoint premise. + +## Two-target optimum is independent of workspace + +Let C_r be the minimum unit paid count for two targets and r>=2 roles. +Embedding a two-role word gives `C_r<=C_2`. The retained lower bound gives +`C_r>=14`, and `(abcb)^2=z` on each target gives `C_2<=16`. +If `C_r=2`. + +This does not decide which value occurs or provide a 14/15-call construction. +It does not claim that every 16-call word compresses. Optimal weighted tariffs +are outside this corollary: a cheaper weighted word may have more than 15 calls. +Physical/compiler/hosting, precision/tape, analytic transfer and proof-kernel +verification remain outside this formal-model theorem; the selected frontier is unchanged. + +Credit @ToikY/PR1662 for the UT4 span and quotient machinery, steph4n-gh/PR1573 +for the UT3 all-register rank method, Arham Tahir/PR1589 for nilpotent couplings, +and Hanson Sun (@bbMisk)/PR1607 for mixed-target coefficient spans. Their +retained source lineage remains credited. Prepared for @ToikY with substantial +OpenAI Codex assistance. Separate AI checks are not independent human review. +New work is Apache-2.0. diff --git a/research/ut4-one-slack-workspace/README.md b/research/ut4-one-slack-workspace/README.md new file mode 100644 index 0000000000..edae91965f --- /dev/null +++ b/research/ut4-one-slack-workspace/README.md @@ -0,0 +1,132 @@ +# UT4 one-slack compression removes the two-target workspace search + +**Uniform scoped reduction; no new word or kappa.** In the full formal +`F2[UT4(F2)]` alphabet of [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662), +every central-target word with `r>=w>=2` and unit paid length `L<=7w+1` +has an equivalent word on exactly `w` roles with no more calls. All extra +roles may begin arbitrary dirty and must be restored. Paid couplings may be +any nonzero binary rank-one matrix, including nilpotents; scalar mixing is +normalized first, and every paid call is counted. + +Consequently the optimal **two-target unit count is identical for every finite +`r>=2`**, with its exact value still one of **14,15,16**. A 14/15-call witness +or complete exclusion on two roles therefore answers the same question for +arbitrary workspace. No such witness or exclusion is supplied here. This adds +the missing workspace implication to the predecessor's unchanged 14..16 interval. + +The [written proof](PROOF.md) sums six scalar span inequalities. At length +`7w` all spans equal the active target plane; at `7w+1` at most one span has +one extra dimension. All paid factors therefore share one block orientation. +Projection to the active corner preserves their product over the **full +noncommutative group algebra**. Projected couplings have rank one or zero; +zero identity factors are discarded, so each label count can only decrease. + +This does not claim that every 16-call word compresses, that weighted tariff +optima are workspace independent, or that larger-slack words admit the same +argument. There are no clean roles, free address operations, higher-rank paid +factors, COPY or ERASE. No physical supplier, rational-frame identity, +compiler/hosting contract, multiplication exponent or selected-frontier change +is claimed. Kernel formalization, precision/tape and analytic transfer remain open. + +## Exact corroboration and scope controls + +The theorem is a written uniform argument with a retained fixed-group lemma; +finite role fixtures corroborate its algebra and do not prove its quantifiers. + +| Check | Coverage | +|---|---| +| Common-orientation formal/faithful operator comparison | 3,969 ordered pairs per upper/lower orientation on three roles, active width two | +| Distinct pair coverage | 7,209 distinct pairs; 729 belong to both orientation families, giving 7,938 recorded cases | +| Complete regular basis columns | 1,524,096 full input columns, including arbitrary dirty-role inputs | +| Zero projected factors actually discarded | 2,268 occurrences across the recorded pair cases | +| Integer span-slack profiles | 105 profiles, widths 2..16; all possible zero/one-excess positions | +| Known coordinate upper words | 10 fixtures through five roles, 2,560 complete basis columns | +| Retained quotient homomorphism/associativity | 4,096 group products and 4,913 basis triples | + +[CERTIFICATE.json](CERTIFICATE.json) retains exact digests, the fixed quotient +receipt and the separately implemented faithful checker's receipt. +The primary engine multiplies six-coordinate formal group coefficients; +[independent.py](independent.py) uses literal four-by-four address matrices +and simultaneous updates of every regular-basis input. It imports no primary +or predecessor executable. Its four fixtures include both common orientations, +noncoordinate/nilpotent couplings and discarded zero projections. The 16/18-call +endpoint fixtures verify compression's algebraic conclusion; they are not +14/15-call witnesses or instances establishing the one-slack forcing premise. + +A mixed upper/lower pair has two individually zero active projections, yet its +full product feeds the dirty role back into the active corner. The checker +rejects it. A rank-two plane missing one active direction demonstrates why +dimension counts alone do not replace the six target-span containments. +The fault suite covers the two-slack threshold, illegal alphabets/domains, +actual model/vendor/receipt corruption, occupied outputs and optimized read-only +relocation. No sampled bits or nonfaithful proof image admits a full endpoint. + +## Reproduce + +From the repository root, with Python3.12 and standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/ut4-one-slack-workspace +``` + +Expect `PASS_UT4_ONE_SLACK_WORKSPACE`, +`PASS_UT4_ONE_SLACK_INDEPENDENT`, passing fault tests and +`PASS_REGISTERED_RESEARCH_PACKAGE research/ut4-one-slack-workspace outcome=completed`. +Normal verification writes nothing. Explicit `verify.py --write-receipt NEW_PATH` +and `independent.py --write NEW_PATH` refuse occupied outputs. The registered +manifest is [VERIFY.json](VERIFY.json); actual local commands, environment and +unrun obligations are recorded in [VALIDATION.json](VALIDATION.json). +Standalone optimized replay also works in a source export containing the +declared live model input. Generic provenance checking requires the pinned Git history. + +## Scope, coordination and retained source credit + +Base main: `a18b4b0136d647529971e9fcb99fa83f5b9a0b81`; revision3 task +`bit-new-register-model`, nonce `e5da093483cfe0c1dfea3262d0f0935b`, scope key +`7f5f4426ef796683c485`. Scope is explicitly **changed** from constructing a +shortest identity to a useful missing-workspace reduction for that construction +problem. [TASK.json](TASK.json) retains the original card, reason, bound and +overlap limitations. The required selected-baseline source-binding control passed; +it was not the selected full cold replay. + +This is complementary to **Aaron Wang / navinor's active two-role exhaustive +search**, [claimed here](https://github.com/CrocSwap/integer-mult-bounds/discussions/1647#discussioncomment-18916137) +with Claude Code assistance. That claim leaves extra dirty roles open; this +package removes that gap at 14/15 calls without duplicating its search or +endorsing an unpublished result. [Our claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1647#discussioncomment-18916672) +states the complementary scope. Entry checks covered 537 open PR bodies including +drafts, local package metadata/ledger and bounded live Discussion reads. +Concurrent merges prevent an atomic PR snapshot; full Discussion pagination, +all diffs and unpublished work were not covered. No novelty guarantee is made. + +Credit **@ToikY / PR1662**, head `01cc02b164ecc4f9d84df3f56a1fe65b88daf390`, +for the UT4 six span containments and middle quotient. Its `quotient.py` is copied +**byte-for-byte**, with exact Git blob and SHA256 in [VENDOR.json](VENDOR.json), +so replay does not require an unmerged dependency checkout. Its unchanged fixed +homomorphism certificate is inherited evidence, not a new independent implementation. +[SOURCES.json](SOURCES.json) binds the live model input and selected/catalog provenance. + +Retain credit **steph4n-gh / [PR1573](https://github.com/CrocSwap/integer-mult-bounds/pull/1573)** +at `0b8c5a69297c794f2de22c04494c83e41300ae36` for all-register zero-sum ranks; +**Arham Tahir / [PR1589](https://github.com/CrocSwap/integer-mult-bounds/pull/1589)** +at `010ec8c01c0edbbb08b541be236ab78d096f2ca1` for nilpotent couplings; +**Hanson Sun (@bbMisk) / [PR1607](https://github.com/CrocSwap/integer-mult-bounds/pull/1607)** +at `9d6117918025cee6a0c5b7ef30ff8d936ca0621f` for coefficient spans, and the +juper997/PR1478, woklerx/PR1443, Gareth Davidson/bitplane/PR1333, +commdata2338/PR1414, eumemic/PR288 and Ali Romman/PR468 lineage retained by them. +No literature-priority claim is made. Prepared for @ToikY with substantial +OpenAI Codex assistance, including two bounded subagents; no independent human +or proof-kernel review claimed. Apache-2.0, with inherited notices preserved. + +## Open next questions + +Does the two-role 27-factor alphabet attain 14 calls? Coordinate with navinor's +active search and independently audit its eventual complete formal certificate. +The reduction makes a rigorous two-role exclusion decisive for all workspace +sizes; an incomplete census does not. No complete certificate is supplied here. + +If 14 is excluded, does a 15-call two-role word exist? Define a complete exact +domain and full endpoint check; extra dirty-role sizes need not be searched. +This remains blocked by the unresolved 14-call question and any overlapping +active investigation. Weighted tariffs and larger-slack workspace use are +separate questions, not conclusions of this package. diff --git a/research/ut4-one-slack-workspace/SOURCES.json b/research/ut4-one-slack-workspace/SOURCES.json new file mode 100644 index 0000000000..834910ebf1 --- /dev/null +++ b/research/ut4-one-slack-workspace/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "a18b4b0136d647529971e9fcb99fa83f5b9a0b81", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/ut4-one-slack-workspace/TASK.json b/research/ut4-one-slack-workspace/TASK.json new file mode 100644 index 0000000000..f60b7dd6c2 --- /dev/null +++ b/research/ut4-one-slack-workspace/TASK.json @@ -0,0 +1,165 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "a18b4b0136d647529971e9fcb99fa83f5b9a0b81", + "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" + ], + "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": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Uniform one-slack compression in the full formal UT4 alphabet for r>=w>=2 and unit paid lengthL<=7w+1; two-target optimum independent of arbitrary restored dirty workspace.", + "scope_change_reason": "The proposed construction attempt yielded a useful missing-workspace reduction. No14/15-call identity was constructed; this proof narrows that construction problem to exactlytwo roles and complements the active two-role search.", + "bottleneck_link": "Removes an unbounded workspace dimension from the smallest-unit-word search in a specified nonabelian register model. Scoped formal model only; no physical supplier or kappa gain.", + "budget_minutes": 60, + "stop_rule": "Session05:52:54UTC through06:52:54UTC; stop construction06:37:54UTC, final15minutes verification/publication/handoff. No large14/15-word census or frontier change.", + "outcome": "completed", + "evidence": "PROOF.md gives the uniform integer span-slack and common-triangular compression proof. CERTIFICATE.json corroborates fixed-group prerequisites, exhaustive three-role triangular factor pairs, complete operators and threshold/fault controls. Exact two-target count remains14,15or16.", + "author": "Prepared for @ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance; bounded separate proof review and independent faithful checker. No human or kernel review claim.", + "open_questions": [ + { + "question": "Does the two-role27-factor alphabet attain14calls, or can a complete exact certificate exclude it?", + "why_it_matters": "The new compression theorem makes a rigorous two-role exclusion decisive for arbitrary restored workspace at14calls.", + "first_step": "Coordinate with navinor current14-call census; independently audit its eventual full-formal certificate before transferring it.", + "blocked_by": "No complete census or witness supplied by this package." + }, + { + "question": "If14callsareexcluded, does a15-calltwo-rolewordexist?", + "why_it_matters": "The uniformminimumis14,15or16; extra dirty roles need not be searched for15calls either.", + "first_step": "Define a complete two-role15-call search with the full formal endpoint and source-bound coverage.", + "blocked_by": "No14exclusionyet; existingactive14searchmustberespected." + } + ], + "chooser": { + "seed": "825a224ec7f742d396fd07c46cd8f17c", + "track": "bit-mechanisms", + "method": "Derive a target-specific relaxation bound for that same explicit alphabet.", + "scope_key": "7084092dd726e7ba1f2f" + }, + "model": { + "group": "UT4(F2)", + "paid_address_alphabet": [ + "a=I+E12", + "b=I+E23", + "c=I+E34" + ], + "target": "I+([I+E14]+1)P_w, P_w=diag(I_w,0_(r-w))", + "scalar_couplings": "Every nonzero binary rank-one N, including idempotents and nilpotents", + "role_domain": "all integers r>=w>=2 for this lemma; all r-w dirty roles restored", + "free_maps": "Scalar GL_r(F2) mixing is normalized into the rank-one couplings; no arbitrary free address maps", + "tariffs": "unit paid occurrence count only; every factor including restoration counted", + "lower_relaxation": "L>=7w forw>=2, with inherited per-letter span ranks", + "known_upper_bill": "8w unitcalls via one (abcb)^2 word per target", + "open": "No14/15-call witness or nonexistence result; workspace elimination atunitL<=7w+1 only.", + "compression": "EitherallN=NP orallN=PN; projectthecommonactivecorneranddiscardzerofactors, preservingthefullformalendpoint." + }, + "predecessors": [ + { + "pr": 1662, + "author": "@ToikY with substantial OpenAI Codex assistance", + "head": "01cc02b164ecc4f9d84df3f56a1fe65b88daf390", + "credit": "UT4 all-six span containments, middle quotient and7w lower bound; unchanged copied fixed17-dimensional quotient." + }, + { + "pr": 1573, + "author": "steph4n-gh", + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "credit": "UT3 all-register zero-sum rank proof" + }, + { + "pr": 1589, + "author": "Arham Tahir", + "head": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", + "credit": "Expanded nilpotent coupling alphabet and degree-two quotient" + }, + { + "pr": 1607, + "author": "Hanson Sun (@bbMisk)", + "head": "9d6117918025cee6a0c5b7ef30ff8d936ca0621f", + "credit": "Mixed-target coefficient-span tariffs" + } + ], + "overlap": { + "entry_open_prs": 537, + "pagination": "Eight numbered pages requested, two terminal empty pages; concurrent merges prevent an atomic snapshot. Includes drafts.", + "discussion_coverage": "Fresh1163/1166 reads and UT4 search; no full Discussion pagination.", + "parallel_scope": { + "author": "Aaron Wang / navinor with Claude Code", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1647#discussioncomment-18916137", + "scope": "Active exhaustive r=w=2 14-call construction/nonexistence search. Our lemma removes the extra-workspace gap; no overlapping exhaustive search or result is claimed." + }, + "nearest_pr": 1662, + "delta": "Newone-slackcompressionandall-workspaceequivalenceoftwo-targetunitoptimum; prior14..16intervalitselfunchanged.", + "limits": "PR bodies, localmetadata/ledger, boundedDiscussionreads. No complete code-diff or unpublished-work coverage; no novelty guarantee.", + "pre_submit_source_refresh": { + "main": "418e40eb2572d930b58c1cf9b82b41c0fc7ee08d", + "unchanged_blobs": [ + "AGENTS.md", + "autoresearch.md", + "CONTRIBUTING.md", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json", + "research/bit-three-register-lower-bound/README.md" + ], + "predecessor_head_unchanged": "01cc02b164ecc4f9d84df3f56a1fe65b88daf390" + }, + "pre_submit_pr_refresh": { + "checked_utc": "2026-10-14T06:27:07Z", + "distinct_open_prs": 461, + "pages_requested": 7, + "empty_terminal_pages": 2, + "matching_UT4_prs": [ + 1662 + ], + "limits": "Includesdrafts;concurrentmergespreventatomicsnapshot;cachedhelperhasnoDiscussionpagination." + } + }, + "first_command": { + "argv": [ + "python3.12", + "-B", + "scripts/research_baseline.py" + ], + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; full selected source inventory checked, no cold replay." + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1647#discussioncomment-18916672", + "selection": { + "nonce": "e5da093483cfe0c1dfea3262d0f0935b", + "track": "bit-mechanisms", + "method": "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "scope_key": "7f5f4426ef796683c485" + } +} diff --git a/research/ut4-one-slack-workspace/VALIDATION.json b/research/ut4-one-slack-workspace/VALIDATION.json new file mode 100644 index 0000000000..68746a9eb5 --- /dev/null +++ b/research/ut4-one-slack-workspace/VALIDATION.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "scope": "Uniform one-slack workspace compression in the formal UT4 model; exact two-target optimum unresolved.", + "environment": { + "python": "3.12.14", + "platform": "macOS-26.5.2-arm64-arm-64bit", + "dependencies": "Python standard library only", + "launcher": "Codex bundled Python; exact local executable retained in session receipts" + }, + "registered_replay": { + "argv": [ + "{python}", + "-B", + "scripts/research_package.py", + "--package", + "research/ut4-one-slack-workspace" + ], + "returncode": 0, + "elapsed_seconds": 11.855, + "test_groups": 6, + "result": "PASS_REGISTERED_RESEARCH_PACKAGE research/ut4-one-slack-workspace outcome=completed" + }, + "additional_checks": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "research/ut4-one-slack-workspace/verify.py" + ], + "result": "PASS_UT4_ONE_SLACK_WORKSPACE pairs=7938 unit_two_target_minimum=workspace_independent exact_value_unresolved" + }, + { + "argv": [ + "{python}", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_research_*.py" + ], + "returncode": 0, + "elapsed_seconds": 1.571, + "tests": 20 + }, + { + "argv": [ + "{python}", + "-B", + "scripts/research_baseline.py" + ], + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; full selected inventory and proof source bindings checked, no cold construction replay." + } + ], + "evidence": { + "uniform_argument": "Six scalar target-span containments and integer rank budget force one common block orientation at L<=7w+1. Compression preserves full formal multiplication and never increases a paid label count.", + "fixed_group_prerequisite": "Exact unchanged copied PR1662 quotient; all4096 group products,4913 basis triples; not an independent new implementation.", + "operator_pair_cases": 7938, + "operator_pair_distinct_cases": 7209, + "pair_family_overlap": 729, + "full_regular_input_columns": 1524096, + "dropped_factor_occurrences": 2268, + "integer_profiles": 105, + "known_upper_witnesses": 10, + "full_upper_witness_basis_columns": 2560, + "separate_checker": "Literal4x4 address matrices and direct faithful full columns; no primary/predecessor imports.", + "controls": "Opposite two-slack profile, mixed-orientation active feedback, wrong target plane at equal rank, real model/vendor/receipt corruptions, occupied outputs, domain rejection and optimized read-only relocation." + }, + "not_checked": [ + "14/15-call witness or complete nonexistence search.", + "Compression of arbitrary16-call two-target words or larger-slack words.", + "Workspace independence of optimal weighted tariffs.", + "Kernel formalization or independent human mathematical review.", + "Physical primitive/compiler/hosting/common-label, precision/tape, analytic transfer or multiplication theorem.", + "Selected complete cold replay (unaffected separate model).", + "Hosted CI at local validation time." + ], + "source_refresh": { + "main": "418e40eb2572d930b58c1cf9b82b41c0fc7ee08d", + "guidance_selected_catalog_model": "Six entry blobs unchanged.", + "predecessor_head": "01cc02b164ecc4f9d84df3f56a1fe65b88daf390", + "predecessor_status": "Open and unmerged at source refresh." + }, + "selected_frontier_unchanged": true, + "ai_assistance": "Substantial OpenAI Codex assistance; two bounded separate AI checks are not human review." +} diff --git a/research/ut4-one-slack-workspace/VENDOR.json b/research/ut4-one-slack-workspace/VENDOR.json new file mode 100644 index 0000000000..b05ddba4ea --- /dev/null +++ b/research/ut4-one-slack-workspace/VENDOR.json @@ -0,0 +1,13 @@ +{ + "schema_version": 1, + "file": "quotient.py", + "origin_pr": 1662, + "origin_author": "Prepared for @ToikY with substantial OpenAI Codex assistance", + "origin_head": "01cc02b164ecc4f9d84df3f56a1fe65b88daf390", + "origin_path": "research/ut4-central-tariff-relaxation/quotient.py", + "git_blob": "658179a39c764ef01d9cbc941c6d746927235df5", + "sha256": "43d923961c584ec5b4b154656a5c93fe31b9ad7d7ee60469bbba4be3f42f9037", + "adaptation": "None; exactbyte-for-bytecopytoavoidrequiringanunmergedpredecessorcheckoutatreplaytime.", + "license": "Apache-2.0", + "scope": "Retainedfixed-groupprerequisite, not an independent new implementation or fullendpointadmission." +} diff --git a/research/ut4-one-slack-workspace/VERIFY.json b/research/ut4-one-slack-workspace/VERIFY.json new file mode 100644 index 0000000000..40a4d2678b --- /dev/null +++ b/research/ut4-one-slack-workspace/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fixedhomomorphism,105integerprofiles,7938orderedtriangularpairswithfullformal/faithfuloperators,10knownupperwitnessesandthresholdcontrols." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 60, + "checks": "Separatelyimplementedliteral64-addressregularcompression, commonorientationandmixedfeedbackcontrols." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 180, + "checks": "Rankbudgetanddomaincontrols, mixedfeedback, realmodel/vendor/receiptfaults, occupiedoutputs andread-onlyoptimizedrelocation." + } + ] +} diff --git a/research/ut4-one-slack-workspace/independent.py b/research/ut4-one-slack-workspace/independent.py new file mode 100644 index 0000000000..b2d380fb3f --- /dev/null +++ b/research/ut4-one-slack-workspace/independent.py @@ -0,0 +1,180 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Faithful active-corner compression checks with literal UT4 matrices. + +No primary or predecessor executable is imported. The checks concern +common triangular orientation, not attainment by a 14/15-call word. +""" +import argparse +import hashlib +import json +from functools import lru_cache +from pathlib import Path + +EDGES = ((0, 1), (1, 2), (2, 3), (0, 2), (1, 3), (0, 3)) +LETTER_CODES = {"a": 1, "b": 2, "c": 4} +ADDRESS_MASK = (1 << 64) - 1 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def literal_matrix(code): + require(type(code) is int and 0 <= code < 64, "invalid UT4 address") + matrix = [[int(i == j) for j in range(4)] for i in range(4)] + for bit, (i, j) in enumerate(EDGES): + matrix[i][j] = (code >> bit) & 1 + return matrix + + +def multiply_addresses(left, right): + a, b = literal_matrix(left), literal_matrix(right) + product = [[sum(a[i][k] * b[k][j] for k in range(4)) % 2 + for j in range(4)] for i in range(4)] + require(all(product[i][i] == 1 and all(product[i][j] == 0 for j in range(i)) + for i in range(4)), "literal product leaves UT4") + return sum(product[i][j] << bit for bit, (i, j) in enumerate(EDGES)) + + +@lru_cache(maxsize=None) +def address_permutation(code): + image = tuple(multiply_addresses(code, h) for h in range(64)) + require(len(set(image)) == 64, "left-regular address action is not a permutation") + return image + + +def paid_factors(word, r): + require(type(r) is int and r >= 1, "positive integer role count required") + checked = [] + for factor in word: + require(isinstance(factor, (tuple, list)) and len(factor) == 3, + "factor must have letter,x,y") + letter, x, y = factor + require(letter in LETTER_CODES, "unknown paid letter") + require(type(x) is int and type(y) is int and 0 < x < (1 << r) and 0 < y < (1 << r), + "coupling must use two nonzero r-bit vectors") + checked.append((letter, x, y)) + return checked + + +def regular_columns(word, r): + """Return all 64r operator columns, role-major then group-code order.""" + factors = paid_factors(word, r) + result = [] + for column in range(64 * r): + state = 1 << column + for letter, x, y in reversed(factors): + source = 0 + for role in range(r): + if (y >> role) & 1: + source ^= (state >> (64 * role)) & ADDRESS_MASK + translated = 0 + remaining, image = source, address_permutation(LETTER_CODES[letter]) + while remaining: + bit = remaining & -remaining + translated ^= 1 << image[bit.bit_length() - 1] + remaining ^= bit + update = source ^ translated + for role in range(r): + if (x >> role) & 1: + state ^= update << (64 * role) + result.append(state) + return result + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def verify_compression(word, r, w): + require(type(w) is int and 1 <= w <= r, "target width must satisfy 1<=w<=r") + factors = paid_factors(word, r) + all_columns_active = all(x >> w == 0 for _, x, _ in factors) + all_rows_active = all(y >> w == 0 for _, _, y in factors) + require(all_columns_active or all_rows_active, "no common triangular orientation") + mask = (1 << w) - 1 + projected = [(letter, x & mask, y & mask) for letter, x, y in factors if x & mask and y & mask] + full = regular_columns(factors, r) + active_mask = (1 << (64 * w)) - 1 + active_corner = [column & active_mask for column in full[:64 * w]] + compressed = regular_columns(projected, w) + require(active_corner == compressed, "faithful active corner differs from compressed operator") + orientation = "both" if all_columns_active and all_rows_active else "columns" if all_columns_active else "rows" + return {"r": r, "w": w, "input_calls": len(factors), "kept_calls": len(projected), + "dropped_zero_calls": len(factors) - len(projected), + "common_orientation": orientation, "active_basis_columns": 64 * w, + "active_output_rows": 64 * w, "active_corner_sha256": digest(active_corner)} + + +def self_checks(): + # The known sixteen-call endpoint is a positive fixture, not a new optimum. + coordinate = [(letter, 1 << role, 1 << role) for role in range(2) for letter in "abcbabcb"] + target = [1 << (64 * role + address_permutation(32)[h]) if role < 2 + else 1 << (64 * role + h) for role in range(3) for h in range(64)] + require(regular_columns(coordinate, 3) == target, "coordinate target fixture failed") + records = [verify_compression(coordinate, 3, 2)] + # outer(3,3)^2=0; its factor still is an involution and commutes with z on active roles. + nilpotent = [("b", 3, 3)] + coordinate + [("b", 3, 3)] + require(regular_columns(nilpotent, 3) == target, "nilpotent active fixture failed") + records.append(verify_compression(nilpotent, 3, 2)) + + upper = [("a", 1, 1), ("b", 2, 2), ("c", 1, 4), + ("a", 3, 5), ("b", 2, 1), ("c", 2, 2)] + lower = [(letter, y, x) for letter, x, y in upper] + records.extend((verify_compression(upper, 3, 2), verify_compression(lower, 3, 2))) + require(records[-2]["dropped_zero_calls"] == records[-1]["dropped_zero_calls"] == 1, + "triangular fixtures omit the expected zero projection") + + # Mixed upper/lower factors can feed a dirty role back into the active corner. + mixed = [("a", 1, 2), ("b", 2, 1)] + try: + verify_compression(mixed, 2, 1) + except ValueError as error: + require(str(error) == "no common triangular orientation", "mixed fixture failed for another reason") + else: + raise ValueError("mixed orientation was accepted") + full = regular_columns(mixed, 2) + active = [column & ADDRESS_MASK for column in full[:64]] + require(active != regular_columns([], 1), "mixed orientation does not exhibit active feedback") + + # Involutions and formal order are checked on all address columns. + for letter in LETTER_CODES: + twice = regular_columns([(letter, 3, 5), (letter, 3, 5)], 3) + require(twice == [1 << i for i in range(192)], "simultaneous rank-one update is not an involution") + ab = regular_columns([("a", 1, 1), ("b", 1, 1)], 1) + ab_code = multiply_addresses(1, 2) + require(ab == [1 << h for h in address_permutation(ab_code)], "factor application order is wrong") + require(ab != regular_columns([("b", 1, 1), ("a", 1, 1)], 1), "reversed product order control failed") + return {"schema_version": 1, "method": "literal 4x4 binary matrices and full regular columns", + "address_bit_positions": [list(edge) for edge in EDGES], + "basis_order": "64*role+group_code", "positive_compressions": records, + "mixed_orientation_rejected": True, "mixed_active_feedback_sha256": digest(active), + "involution_controls": 3, "product_order_controls": 1, + "scope": "compression fixtures and known16-call endpoint; no14/15-call attainment claim"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--check", type=Path, help="compare complete self-check receipt") + parser.add_argument("--write", type=Path, help="create a fresh receipt; never overwrite") + args = parser.parse_args() + try: + if args.write: + require(not args.write.exists(), "output already exists") + receipt = self_checks() + if args.check: + require(json.loads(args.check.read_text()) == receipt, "independent receipt differs") + if args.write: + with args.write.open("x") as stream: + json.dump(receipt, stream, indent=2, sort_keys=True) + stream.write("\n") + except (ValueError, OSError) as error: + parser.exit(1, "FAIL_UT4_ONE_SLACK_INDEPENDENT: " + str(error) + "\n") + print("PASS_UT4_ONE_SLACK_INDEPENDENT positive_compressions=4 " + "mixed_orientation_control=1 involutions=3 product_order=1") + + +if __name__ == "__main__": + main() diff --git a/research/ut4-one-slack-workspace/quotient.py b/research/ut4-one-slack-workspace/quotient.py new file mode 100644 index 0000000000..658179a39c --- /dev/null +++ b/research/ut4-one-slack-workspace/quotient.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact 17-dimensional degree-three UT4(F2) quotient. + +This quotient provides necessary coefficient conditions only. It is not +faithful on F2[UT4(F2)] and does not admit a formal endpoint on its own. +Prepared for @ToikY with substantial OpenAI Codex assistance. +""" +import argparse +import hashlib +import itertools +import json +from functools import lru_cache +from pathlib import Path + +BASIS = ("", "a", "b", "c", "ab", "ac", "ba", "bc", "cb", + "aba", "abc", "acb", "bab", "bac", "bcb", "cba", "cbc") +INDEX = {name: index for index, name in enumerate(BASIS)} +LETTERS = {"a": 1, "b": 2, "c": 4} +POSITIONS = ((0, 1), (1, 2), (2, 3), (0, 2), (1, 3), (0, 3)) +Z = 32 +UNIT = 1 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def reduced_word(word): + """Canonical monomial, or None for zero in the defined quotient.""" + require(isinstance(word, str) and all(letter in LETTERS for letter in word), + "invalid quotient monomial") + if len(word) >= 4: + return None + while "ca" in word: + word = word.replace("ca", "ac") + if any(letter * 2 in word for letter in LETTERS): + return None + require(word in INDEX, "incomplete quotient basis") + return word + + +@lru_cache(maxsize=1) +def basis_products(): + return tuple(tuple(0 if (name := reduced_word(left + right)) is None + else 1 << INDEX[name] for right in BASIS) for left in BASIS) + + +def algebra_mul(left, right): + require(type(left) is int and type(right) is int + and 0 <= left < (1 << len(BASIS)) and 0 <= right < (1 << len(BASIS)), + "quotient coefficient vector outside the 17-bit basis") + answer = 0 + table = basis_products() + while left: + bit = left & -left + i = bit.bit_length() - 1 + terms = right + while terms: + other = terms & -terms + answer ^= table[i][other.bit_length() - 1] + terms ^= other + left ^= bit + return answer + + +def paid_group_word(word): + image = UNIT + for letter in word: + require(letter in LETTERS, "invalid group generator") + image = algebra_mul(image, UNIT | (1 << INDEX[letter])) + return image + + +@lru_cache(maxsize=64) +def group_image(code): + require(type(code) is int and 0 <= code < 64, "group code outside 0..63") + A, B, C, D, E, F = [(code >> index) & 1 for index in range(6)] + # Normal form a^A b^B c^C d^(D+AB) e^(E+BC) z^(F+AE). + powers = (A, B, C, D ^ (A & B), E ^ (B & C), F ^ (A & E)) + words = ("a", "b", "c", "abab", "bcbc", "abcbabcb") + image = UNIT + for power, word in zip(powers, words): + if power: + image = algebra_mul(image, paid_group_word(word)) + return image + + +def literal_group_product(left_code, right_code): + """Independent literal four-by-four multiplication for map checking.""" + require(type(left_code) is int and type(right_code) is int + and 0 <= left_code < 64 and 0 <= right_code < 64, + "invalid group multiplication code") + matrices = [] + for code in (left_code, right_code): + rows = [[int(i == j) for j in range(4)] for i in range(4)] + for bit, (i, j) in enumerate(POSITIONS): + rows[i][j] = (code >> bit) & 1 + matrices.append(rows) + left, right = matrices + product = [[sum(left[i][k] * right[k][j] for k in range(4)) & 1 + for j in range(4)] for i in range(4)] + return sum(product[i][j] << bit for bit, (i, j) in enumerate(POSITIONS)) + + +def matrix_product(left, right): + rows = [] + for row in left: + value = 0 + while row: + bit = row & -row + value ^= right[bit.bit_length() - 1] + row ^= bit + rows.append(value) + return rows + + +def validate_matrix(rows, roles): + require(isinstance(rows, (list, tuple)) and len(rows) == roles + and all(type(row) is int and 0 <= row < (1 << roles) for row in rows), + "invalid binary role matrix") + + +def word_coefficients(word, roles): + """Evaluate arbitrary admitted paid words; return all named coefficients. + + A word entry is (label,x,y), with nonzero binary vector bit encodings. + Matrix rows use the same bit convention as the primary checker. + """ + require(type(roles) is int and roles >= 1, "positive integer role count required") + result = {"": [1 << i for i in range(roles)]} + for label, x, y in word: + require(label in LETTERS and type(x) is int and type(y) is int + and 0 < x < (1 << roles) and 0 < y < (1 << roles), + "invalid rank-one paid factor") + coupling = [y if (x >> i) & 1 else 0 for i in range(roles)] + updated = {name: rows[:] for name, rows in result.items()} + for name, rows in result.items(): + next_name = reduced_word(name + label) + if next_name is None: + continue + increment = matrix_product(rows, coupling) + updated[next_name] = [a ^ b for a, b in zip( + updated.get(next_name, [0] * roles), increment)] + result = {name: rows for name, rows in updated.items() if any(rows)} + return {name: result.get(name, [0] * roles) for name in BASIS} + + +mixed_coefficients = word_coefficients + + +def image_coefficients(formal, roles): + """Evaluate a full formal group-algebra operator in the quotient.""" + require(type(roles) is int and roles >= 1 and isinstance(formal, dict), + "invalid formal quotient input") + result = {name: [0] * roles for name in BASIS} + for code, rows in formal.items(): + validate_matrix(rows, roles) + image = group_image(code) + while image: + bit = image & -image + name = BASIS[bit.bit_length() - 1] + result[name] = [a ^ b for a, b in zip(result[name], rows)] + image ^= bit + return result + + +def self_checks(): + names = {reduced_word("".join(word)) for length in range(4) + for word in itertools.product(LETTERS, repeat=length)} - {None} + require(names == set(BASIS) and len(BASIS) == 17, "quotient basis coverage") + units = [1 << index for index in range(len(BASIS))] + require(all(algebra_mul(UNIT, value) == algebra_mul(value, UNIT) == value + for value in units), "quotient unit") + associative = 0 + for left, middle, right in itertools.product(units, repeat=3): + require(algebra_mul(algebra_mul(left, middle), right) + == algebra_mul(left, algebra_mul(middle, right)), "quotient associativity") + associative += 1 + images = [group_image(code) for code in range(64)] + require(len(set(images)) == 64, "group images collide") + products = [] + for left, right in itertools.product(range(64), repeat=2): + code = literal_group_product(left, right) + require(algebra_mul(images[left], images[right]) == images[code], + "normal-form map is not a group homomorphism") + products.append(code) + central = [BASIS[index] for index in range(len(BASIS)) if (images[Z] >> index) & 1] + require(central == ["", "abc", "acb", "bac", "cba"], "central cubic coefficients") + require(algebra_mul(images[Z] ^ UNIT, images[LETTERS["a"]] ^ UNIT) == 0, + "common formal kernel must be invisible in quotient") + # Compare direct coefficient expansion with the full-group-image route. + # Literal fixture: two central targets on two distinct coordinate projectors. + fixture = [(label, 1 << role, 1 << role) for role in range(2) + for label in "abcbabcb"] + expected = {0: [0, 0], Z: [1, 2]} + require(word_coefficients(fixture, 2) == image_coefficients(expected, 2), + "central word coefficients do not match its formal target image") + encoded = json.dumps([list(BASIS), images, products], separators=(",", ":")).encode() + return {"schema_version": 1, "basis": list(BASIS), "dimension": 17, + "basis_associativity_products": associative, "group_products": len(products), + "distinct_group_images": len(set(images)), "central_image": central, + "group_map_sha256": hashlib.sha256(encoded).hexdigest(), + "common_kernel_zero": True, + "scope": "Necessary cubic coefficients; full group-algebra endpoint admission remains separate."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--check", type=Path, help="compare every self-check receipt field") + parser.add_argument("--write", type=Path, help="write a fresh receipt; refuse occupied paths") + args = parser.parse_args() + result = self_checks() + if args.check: + require(json.loads(args.check.read_text()) == result, "quotient receipt differs") + if args.write: + with args.write.open("x") as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write("\n") + print("PASS_UT4_CUBIC_QUOTIENT dimension=17 products=4096 associative=4913") + + +if __name__ == "__main__": + main() diff --git a/research/ut4-one-slack-workspace/test_package.py b/research/ut4-one-slack-workspace/test_package.py new file mode 100644 index 0000000000..7bd2414776 --- /dev/null +++ b/research/ut4-one-slack-workspace/test_package.py @@ -0,0 +1,120 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Boundary/fault controls; prepared for @ToikY with substantial OpenAI Codex assistance.""" +import importlib.util +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] +spec = importlib.util.spec_from_file_location("workspace_primary", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + +def run(path, *args): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(path), *map(str, args)], + capture_output=True, text=True, timeout=120) + +def relocate(root): + package = root / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + inputs = [row["path"] for row in json.loads((HERE / "SOURCES.json").read_text())["files"] + if row["usage"] == "input"] + for name in inputs: + destination = root / name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, destination) + return package, inputs + +class PackageTests(unittest.TestCase): + def test_one_slack_and_threshold(self): + for exception in range(-1, 6): + spans = [2] * 6 + counts = [4, 6, 4] + if exception >= 0: + spans[exception] = 3 + counts[exception // 2] += 1 + answer = v.one_slack_orientation(2, counts, spans) + self.assertEqual(answer, {"columns": exception < 0 or exception % 2 == 1, + "rows": exception < 0 or exception % 2 == 0}) + for spans, counts in (([3, 2, 2, 3, 2, 2], [5, 7, 4]), + ([2, 2, 3, 2, 2, 3], [4, 7, 5])): + with self.assertRaisesRegex(ValueError, "outside one-slack length threshold"): + v.one_slack_orientation(2, counts, spans) + with self.assertRaisesRegex(ValueError, "requires w>=2"): + v.one_slack_orientation(1, [2, 4, 2], [1] * 6) + + def test_mixed_orientation_has_actual_feedback(self): + word = [("a", 1, 4), ("b", 4, 1)] + with self.assertRaisesRegex(ValueError, "no common triangular orientation"): + v.compress(word, 3, 2) + corner = v.active_corner(v.formal_product(word, 3), 2) + self.assertNotEqual(corner, v.formal_product([], 2)) + self.assertNotEqual(v.regular_columns(corner, 2), v.regular_columns({0: [1, 2]}, 2)) + + def test_invalid_paid_alphabet_and_domain(self): + for word, roles in (([("d", 1, 1)], 3), ([("a", True, 1)], 3), + ([("a", 1, 8)], 3), ([("a", 0, 1)], 3), ([], True)): + with self.assertRaises(ValueError): + v.formal_product(word, roles) + for width in (0, 4, True): + with self.assertRaises(ValueError): + v.compress([], 3, width) + + def test_real_source_and_vendor_faults_reject_before_import(self): + with tempfile.TemporaryDirectory(prefix="ut4-input-fault-") as raw: + root = Path(raw) + package, inputs = relocate(root) + source = root / inputs[0] + honest = source.read_bytes() + source.write_bytes(honest + b"\nchanged\n") + result = run(package / "verify.py") + self.assertNotEqual(result.returncode, 0) + self.assertIn("pinned model source changed", result.stderr) + source.write_bytes(honest) + (package / "quotient.py").write_text('raise RuntimeError("VENDOR_IMPORTED")\n') + result = run(package / "verify.py") + self.assertNotEqual(result.returncode, 0) + self.assertIn("pinned quotient source changed", result.stderr) + self.assertNotIn("VENDOR_IMPORTED", result.stderr) + + def test_actual_receipt_fault_and_no_overwrite(self): + with tempfile.TemporaryDirectory(prefix="ut4-receipt-fault-") as raw: + package, _ = relocate(Path(raw)) + path = package / "CERTIFICATE.json" + receipt = json.loads(path.read_text()) + receipt["ordered_triangular_pairs"] -= 1 + path.write_text(json.dumps(receipt)) + result = run(package / "verify.py") + self.assertNotEqual(result.returncode, 0) + self.assertIn("certificate differs", result.stderr) + occupied = Path(raw) / "occupied.json" + occupied.write_text("keep") + result = run(package / "verify.py", "--write-receipt", occupied) + self.assertNotEqual(result.returncode, 0) + self.assertEqual(occupied.read_text(), "keep") + + def test_optimized_readonly_relocation(self): + with tempfile.TemporaryDirectory(prefix="ut4 readonly path ") as raw: + root = Path(raw) + package, _ = relocate(root) + before = {str(p.relative_to(root)): p.read_bytes() for p in root.rglob("*") if p.is_file()} + for path in root.rglob("*"): + path.chmod(0o555 if path.is_dir() else 0o444) + root.chmod(0o555) + try: + for name in ("verify.py", "independent.py"): + result = run(package / name) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(before, {str(p.relative_to(root)): p.read_bytes() + for p in root.rglob("*") if p.is_file()}) + finally: + root.chmod(0o755) + for path in root.rglob("*"): + path.chmod(0o755 if path.is_dir() else 0o644) +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/ut4-one-slack-workspace/verify.py b/research/ut4-one-slack-workspace/verify.py new file mode 100644 index 0000000000..008a90e681 --- /dev/null +++ b/research/ut4-one-slack-workspace/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact corroboration of the written UT4 one-slack workspace reduction. + +Prepared for @ToikY with substantial OpenAI Codex assistance. +Finite fixtures do not establish 14/15-call existence or kernel formalization. +""" +import argparse +import hashlib +import importlib.util +import itertools +import json +from functools import lru_cache +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +LETTERS = {"a": 1, "b": 2, "c": 4} + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def sibling(name): + spec = importlib.util.spec_from_file_location("ut4_workspace_" + name, HERE / (name + ".py")) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def rank(vectors): + pivots = {} + for vector in vectors: + while vector: + p = vector.bit_length() - 1 + if p not in pivots: + pivots[p] = vector + break + vector ^= pivots[p] + return len(pivots) + + +def identity(r): + return [1 << i for i in range(r)] + + +def mul(a, b): + out = [] + for row in a: + value = 0 + while row: + bit = row & -row + value ^= b[bit.bit_length() - 1] + row ^= bit + out.append(value) + return out + + +def outer(x, y, r): + return [y if (x >> i) & 1 else 0 for i in range(r)] + + +@lru_cache(maxsize=4096) +def group_product(g, h): + a, b, c, d, e, f = [(g >> i) & 1 for i in range(6)] + A, B, C, D, E, F = [(h >> i) & 1 for i in range(6)] + values = (a ^ A, b ^ B, c ^ C, d ^ D ^ (a & B), + e ^ E ^ (b & C), f ^ F ^ (a & E) ^ (d & C)) + return sum(v << i for i, v in enumerate(values)) + + +def factors(word, r): + require(type(r) is int and r >= 1, "invalid role count") + checked = [] + for label, x, y in word: + require(label in LETTERS and type(x) is int and type(y) is int + and 0 < x < (1 << r) and 0 < y < (1 << r), "invalid paid alphabet") + checked.append((label, x, y)) + return checked + + +def formal_product(word, r): + result = {0: identity(r)} + for label, x, y in factors(word, r): + updated = {g: rows[:] for g, rows in result.items()} + for g, rows in result.items(): + increment = mul(rows, outer(x, y, r)) + for h in (g, group_product(g, LETTERS[label])): + updated[h] = [a ^ b for a, b in zip(updated.get(h, [0] * r), increment)] + result = {g: rows for g, rows in updated.items() if any(rows)} + return result + + +def active_corner(formal, w): + mask = (1 << w) - 1 + projected = {g: [row & mask for row in rows[:w]] for g, rows in formal.items()} + return {g: rows for g, rows in projected.items() if any(rows)} + + +def regular_columns(formal, r): + columns = [] + for role in range(r): + for h in range(64): + column = 0 + for g, rows in formal.items(): + for i, row in enumerate(rows): + if (row >> role) & 1: + column ^= 1 << (64 * i + group_product(g, h)) + columns.append(column) + return columns + + +def compress(word, r, w): + require(type(w) is int and 1 <= w <= r, "invalid active width") + word = factors(word, r) + columns = all(x >> w == 0 for _, x, _ in word) + rows = all(y >> w == 0 for _, _, y in word) + require(columns or rows, "no common triangular orientation") + mask = (1 << w) - 1 + return [(g, x & mask, y & mask) for g, x, y in word if x & mask and y & mask] + + +def one_slack_orientation(w, counts, spans): + """Check the integer rank-budget implication, assuming the stated containments. + + The full word's coefficient equations supply those containments in PROOF.md; + this function never accepts an endpoint from ranks alone. + """ + require(type(w) is int and w >= 2, "one-slack theorem requires w>=2") + require(len(counts) == 3 and len(spans) == 6 + and all(type(n) is int and n >= 0 for n in counts + spans), "invalid rank profile") + require(all(n >= w for n in spans), "missing target span rank") + require(counts[0] >= spans[0] + spans[1] + and counts[1] >= w + spans[2] + spans[3] + and counts[2] >= spans[4] + spans[5], "rank budget violation") + require(sum(counts) <= 7 * w + 1, "outside one-slack length threshold") + require(all(spans[i] == w for i in (0, 2, 4)) + or all(spans[i] == w for i in (1, 3, 5)), "no shared orientation") + return {"columns": all(spans[i] == w for i in (0, 2, 4)), + "rows": all(spans[i] == w for i in (1, 3, 5))} + + +def target(r, w): + P = [1 << i if i < w else 0 for i in range(r)] + return {g: rows for g, rows in {0: [a ^ b for a, b in zip(identity(r), P)], 32: P}.items() + if any(rows)} + + +def source_checks(): + for source in json.loads((HERE / "SOURCES.json").read_text())["files"]: + if source["usage"] == "input": + require(hashlib.sha256((ROOT / source["path"]).read_bytes()).hexdigest() == source["sha256"], + "pinned model source changed") + vendor = json.loads((HERE / "VENDOR.json").read_text()) + require(hashlib.sha256((HERE / "quotient.py").read_bytes()).hexdigest() == vendor["sha256"], + "pinned quotient source changed") + + +def build_receipt(): + source_checks() + independent, quotient = sibling("independent"), sibling("quotient") + require(all(group_product(g, h) == independent.multiply_addresses(g, h) + for g in range(64) for h in range(64)), "literal group mismatch") + profiles = [] + for w in range(2, 17): + for exception in range(-1, 6): + spans = [w] * 6 + if exception >= 0: + spans[exception] += 1 + counts = [spans[0] + spans[1], w + spans[2] + spans[3], spans[4] + spans[5]] + profiles.append([w, counts, spans, one_slack_orientation(w, counts, spans)]) + transcript, pairs, dropped = hashlib.sha256(), 0, 0 + for orientation in ("columns", "rows"): + alphabet = [(g, x, y) for g in LETTERS + for x in range(1, 4 if orientation == "columns" else 8) + for y in range(1, 8 if orientation == "columns" else 4)] + for word in itertools.product(alphabet, repeat=2): + compressed = compress(word, 3, 2) + full = formal_product(word, 3) + small = formal_product(compressed, 2) + require(active_corner(full, 2) == small, "formal compression mismatch") + faithful = independent.regular_columns(word, 3) + require(regular_columns(full, 3) == faithful, "independent full operator mismatch") + require([c & ((1 << 128) - 1) for c in faithful[:128]] + == independent.regular_columns(compressed, 2), "faithful compression mismatch") + pairs += 1 + dropped += len(word) - len(compressed) + transcript.update(json.dumps([orientation, word, compressed, small], sort_keys=True).encode()) + witnesses, witness_columns = 0, 0 + for r in range(2, 6): + for w in range(2, r + 1): + word = [(g, 1 << i, 1 << i) for i in range(w) for g in "abcbabcb"] + formal = formal_product(word, r) + require(formal == target(r, w), "known upper word endpoint") + require(regular_columns(formal, r) == independent.regular_columns(word, r), "upper faithful mismatch") + data = quotient.word_coefficients(word, r) + P = [1 << i if i < w else 0 for i in range(r)] + require(all(data[k] == P for k in ("abc", "cba", "bac", "acb")), "retained target coefficients") + require(all(not any(data[k]) for k in ("a", "b", "c", "ab", "bc")), "retained lower coefficients") + require(formal_product(compress(word, r, w), w) == target(w, w), "known upper word compression") + witnesses += 1 + witness_columns += 64 * r + mixed = [("a", 1, 4), ("b", 4, 1)] + require(active_corner(formal_product(mixed, 3), 2) != formal_product([], 2), "mixed feedback control") + try: + compress(mixed, 3, 2) + except ValueError as error: + require(str(error) == "no common triangular orientation", "wrong mixed rejection") + else: + raise ValueError("mixed orientation accepted") + require(rank([1, 4]) == 2 and rank([1, 4, 2]) == 3, "rank alone misses active containment") + return {"schema_version": 1, "uniform_scope": "w>=2,L<=7w+1,r>=w; written proof, not finite extrapolation", + "two_target_minimum": "C_r=C_2 in {14,15,16}; exact value unresolved", + "quotient": quotient.self_checks(), "independent": independent.self_checks(), + "rank_profiles": len(profiles), "rank_profile_sha256": hashlib.sha256(json.dumps(profiles, sort_keys=True).encode()).hexdigest(), + "ordered_triangular_pairs": pairs, "pair_roles": 3, "active_width": 2, + "dropped_factor_occurrences": dropped, "pair_transcript_sha256": transcript.hexdigest(), + "known_upper_witnesses": witnesses, "full_witness_basis_columns": witness_columns, + "mixed_feedback_rejected": True, + "equal_rank_wrong_target_plane_control": {"candidate_basis": [1, 4], "active_basis": [1, 2], + "candidate_rank": 2, "union_rank": 3}, + "new_14_or_15_word": False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path) + args = parser.parse_args() + if args.write_receipt: + require(not args.write_receipt.exists(), "output already exists") + receipt = build_receipt() + raw = json.dumps(receipt, sort_keys=True, indent=2) + "\n" + if args.write_receipt: + with args.write_receipt.open("x") as stream: + stream.write(raw) + else: + require(json.dumps(json.loads((HERE / "CERTIFICATE.json").read_text()), sort_keys=True) + == json.dumps(receipt, sort_keys=True), "certificate differs") + print("PASS_UT4_ONE_SLACK_WORKSPACE pairs=" + str(receipt["ordered_triangular_pairs"]) + + " unit_two_target_minimum=workspace_independent exact_value_unresolved") + + +if __name__ == "__main__": + main()