From 0b8c5a69297c794f2de22c04494c83e41300ae36 Mon Sep 17 00:00:00 2001 From: steph4n-gh <284007938+steph4n-gh@users.noreply.github.com> Date: Tue, 13 Oct 2026 23:12:36 -0400 Subject: [PATCH] Prove all-register UT3 commutator call bound for any target count --- .../CERTIFICATE.json | 997 ++++++++++++++++++ .../ut3-commutator-all-registers/CLAIM.json | 63 ++ .../ut3-commutator-all-registers/README.md | 214 ++++ .../ut3-commutator-all-registers/SOURCES.json | 57 + .../ut3-commutator-all-registers/TASK.json | 61 ++ .../VALIDATION.md | 91 ++ .../ut3-commutator-all-registers/VERIFY.json | 20 + .../independent.py | 376 +++++++ .../ut3-commutator-all-registers/verify.py | 331 ++++++ 9 files changed, 2210 insertions(+) create mode 100644 research/ut3-commutator-all-registers/CERTIFICATE.json create mode 100644 research/ut3-commutator-all-registers/CLAIM.json create mode 100644 research/ut3-commutator-all-registers/README.md create mode 100644 research/ut3-commutator-all-registers/SOURCES.json create mode 100644 research/ut3-commutator-all-registers/TASK.json create mode 100644 research/ut3-commutator-all-registers/VALIDATION.md create mode 100644 research/ut3-commutator-all-registers/VERIFY.json create mode 100644 research/ut3-commutator-all-registers/independent.py create mode 100644 research/ut3-commutator-all-registers/verify.py diff --git a/research/ut3-commutator-all-registers/CERTIFICATE.json b/research/ut3-commutator-all-registers/CERTIFICATE.json new file mode 100644 index 0000000000..6b628a82ef --- /dev/null +++ b/research/ut3-commutator-all-registers/CERTIFICATE.json @@ -0,0 +1,997 @@ +{ + "independent": { + "arbitrary_word_factorization_cases": 195, + "arithmetic": "GF(2), exact integer bitsets", + "attaining_operator_cases": 45, + "cases": [ + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 0, + "paid_calls": 4, + "roles": 1, + "targets": 1 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 1, + "paid_calls": 4, + "roles": 1, + "targets": 1 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 2, + "paid_calls": 4, + "roles": 1, + "targets": 1 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 0, + "paid_calls": 4, + "roles": 2, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 0, + "paid_calls": 8, + "roles": 2, + "targets": 2 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 1, + "paid_calls": 4, + "roles": 2, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 1, + "paid_calls": 8, + "roles": 2, + "targets": 2 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 2, + "paid_calls": 4, + "roles": 2, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 2, + "paid_calls": 8, + "roles": 2, + "targets": 2 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 0, + "paid_calls": 4, + "roles": 3, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 0, + "paid_calls": 8, + "roles": 3, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 0, + "paid_calls": 12, + "roles": 3, + "targets": 3 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 1, + "paid_calls": 4, + "roles": 3, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 1, + "paid_calls": 8, + "roles": 3, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 1, + "paid_calls": 12, + "roles": 3, + "targets": 3 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 2, + "paid_calls": 4, + "roles": 3, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 2, + "paid_calls": 8, + "roles": 3, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 2, + "paid_calls": 12, + "roles": 3, + "targets": 3 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 0, + "paid_calls": 4, + "roles": 4, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 0, + "paid_calls": 8, + "roles": 4, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 0, + "paid_calls": 12, + "roles": 4, + "targets": 3 + }, + { + "a_calls": 8, + "b_calls": 8, + "basis_variant": 0, + "paid_calls": 16, + "roles": 4, + "targets": 4 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 1, + "paid_calls": 4, + "roles": 4, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 1, + "paid_calls": 8, + "roles": 4, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 1, + "paid_calls": 12, + "roles": 4, + "targets": 3 + }, + { + "a_calls": 8, + "b_calls": 8, + "basis_variant": 1, + "paid_calls": 16, + "roles": 4, + "targets": 4 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 2, + "paid_calls": 4, + "roles": 4, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 2, + "paid_calls": 8, + "roles": 4, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 2, + "paid_calls": 12, + "roles": 4, + "targets": 3 + }, + { + "a_calls": 8, + "b_calls": 8, + "basis_variant": 2, + "paid_calls": 16, + "roles": 4, + "targets": 4 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 0, + "paid_calls": 4, + "roles": 5, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 0, + "paid_calls": 8, + "roles": 5, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 0, + "paid_calls": 12, + "roles": 5, + "targets": 3 + }, + { + "a_calls": 8, + "b_calls": 8, + "basis_variant": 0, + "paid_calls": 16, + "roles": 5, + "targets": 4 + }, + { + "a_calls": 10, + "b_calls": 10, + "basis_variant": 0, + "paid_calls": 20, + "roles": 5, + "targets": 5 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 1, + "paid_calls": 4, + "roles": 5, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 1, + "paid_calls": 8, + "roles": 5, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 1, + "paid_calls": 12, + "roles": 5, + "targets": 3 + }, + { + "a_calls": 8, + "b_calls": 8, + "basis_variant": 1, + "paid_calls": 16, + "roles": 5, + "targets": 4 + }, + { + "a_calls": 10, + "b_calls": 10, + "basis_variant": 1, + "paid_calls": 20, + "roles": 5, + "targets": 5 + }, + { + "a_calls": 2, + "b_calls": 2, + "basis_variant": 2, + "paid_calls": 4, + "roles": 5, + "targets": 1 + }, + { + "a_calls": 4, + "b_calls": 4, + "basis_variant": 2, + "paid_calls": 8, + "roles": 5, + "targets": 2 + }, + { + "a_calls": 6, + "b_calls": 6, + "basis_variant": 2, + "paid_calls": 12, + "roles": 5, + "targets": 3 + }, + { + "a_calls": 8, + "b_calls": 8, + "basis_variant": 2, + "paid_calls": 16, + "roles": 5, + "targets": 4 + }, + { + "a_calls": 10, + "b_calls": 10, + "basis_variant": 2, + "paid_calls": 20, + "roles": 5, + "targets": 5 + } + ], + "exact_operators_sha256": "65fd1fe044e2142a32e867a879e3b03c6e1213d0dc5f03eaa7e6a3c8af7beccc", + "group_elements": 8, + "homomorphism_products_per_representation": 64, + "maximum_regular_operator_dimension": 40, + "natural_and_swapped_c": "I_3 + E_02", + "negative_controls_rejected": { + "corrupted_regular_matrix": 1, + "extra_dirty_target": 30, + "missing_call": 45, + "representation_invisible_dirty_shear": 30, + "wrong_label": 45 + }, + "regular_group_algebra_basis_rank": 8, + "representations": [ + "natural 3x3", + "generator-swapped 3x3", + "faithful regular 8x8" + ], + "roles_checked": [ + 1, + 2, + 3, + 4, + 5 + ], + "scalar_basis_variants_per_pair": 3, + "schema": "ut3-independent-binary-matrix-check-v1", + "scope": "Finite exact checks only; the all-register theorem requires the written proof.", + "targets_checked": "every 1 <= k <= r" + }, + "no_new_kappa": true, + "primary": { + "arbitrary_word_formula_fixtures": 75, + "fixtures": [ + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": false, + "r": 1 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": true, + "r": 1 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": false, + "r": 2 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": true, + "r": 2 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 2, + 2, + 4 + ], + "2": [ + 2, + 2, + 4 + ] + }, + "calls": 8, + "k": 2, + "mixed": false, + "r": 2 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 2, + 2, + 4 + ], + "2": [ + 2, + 2, + 4 + ] + }, + "calls": 8, + "k": 2, + "mixed": true, + "r": 2 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": false, + "r": 3 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": true, + "r": 3 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 2, + 2, + 4 + ], + "2": [ + 2, + 2, + 4 + ] + }, + "calls": 8, + "k": 2, + "mixed": false, + "r": 3 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 2, + 2, + 4 + ], + "2": [ + 2, + 2, + 4 + ] + }, + "calls": 8, + "k": 2, + "mixed": true, + "r": 3 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 3, + 3, + 6 + ], + "2": [ + 3, + 3, + 6 + ] + }, + "calls": 12, + "k": 3, + "mixed": false, + "r": 3 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 3, + 3, + 6 + ], + "2": [ + 3, + 3, + 6 + ] + }, + "calls": 12, + "k": 3, + "mixed": true, + "r": 3 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": false, + "r": 4 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": true, + "r": 4 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 2, + 2, + 4 + ], + "2": [ + 2, + 2, + 4 + ] + }, + "calls": 8, + "k": 2, + "mixed": false, + "r": 4 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 2, + 2, + 4 + ], + "2": [ + 2, + 2, + 4 + ] + }, + "calls": 8, + "k": 2, + "mixed": true, + "r": 4 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 3, + 3, + 6 + ], + "2": [ + 3, + 3, + 6 + ] + }, + "calls": 12, + "k": 3, + "mixed": false, + "r": 4 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 3, + 3, + 6 + ], + "2": [ + 3, + 3, + 6 + ] + }, + "calls": 12, + "k": 3, + "mixed": true, + "r": 4 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 4, + 4, + 8 + ], + "2": [ + 4, + 4, + 8 + ] + }, + "calls": 16, + "k": 4, + "mixed": false, + "r": 4 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 4, + 4, + 8 + ], + "2": [ + 4, + 4, + 8 + ] + }, + "calls": 16, + "k": 4, + "mixed": true, + "r": 4 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": false, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 1, + 1, + 2 + ], + "2": [ + 1, + 1, + 2 + ] + }, + "calls": 4, + "k": 1, + "mixed": true, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 2, + 2, + 4 + ], + "2": [ + 2, + 2, + 4 + ] + }, + "calls": 8, + "k": 2, + "mixed": false, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 2, + 2, + 4 + ], + "2": [ + 2, + 2, + 4 + ] + }, + "calls": 8, + "k": 2, + "mixed": true, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 3, + 3, + 6 + ], + "2": [ + 3, + 3, + 6 + ] + }, + "calls": 12, + "k": 3, + "mixed": false, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 3, + 3, + 6 + ], + "2": [ + 3, + 3, + 6 + ] + }, + "calls": 12, + "k": 3, + "mixed": true, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 4, + 4, + 8 + ], + "2": [ + 4, + 4, + 8 + ] + }, + "calls": 16, + "k": 4, + "mixed": false, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 4, + 4, + 8 + ], + "2": [ + 4, + 4, + 8 + ] + }, + "calls": 16, + "k": 4, + "mixed": true, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 5, + 5, + 10 + ], + "2": [ + 5, + 5, + 10 + ] + }, + "calls": 20, + "k": 5, + "mixed": false, + "r": 5 + }, + { + "a_b_span_ranks_and_counts": { + "1": [ + 5, + 5, + 10 + ], + "2": [ + 5, + 5, + 10 + ] + }, + "calls": 20, + "k": 5, + "mixed": true, + "r": 5 + } + ], + "formal_endpoint_sha256": "224b0f2cdc7118035e4a256a2f32faec09daf6e2a2758ab8b8a15b9dbeb101c9", + "formula_fixture_seed": 14, + "group_associativity_cases": 512, + "homomorphism_cases_per_representation": 64, + "hypothesis_boundary_witnesses": { + "expanded_c_alphabet": { + "calls": 3, + "k": 3, + "r": 4 + }, + "rank_k_paid_projectors": { + "calls": 4, + "k": 3, + "r": 4 + } + }, + "invisible_nonzero_coefficient_mask": 51, + "method": "formal group-algebra coefficients with triple group law", + "negative_controls": [ + "omit_call_0", + "wrong_label_0", + "omit_call_1", + "wrong_label_1", + "omit_call_2", + "wrong_label_2", + "omit_call_3", + "wrong_label_3", + "omit_call_4", + "wrong_label_4", + "omit_call_5", + "wrong_label_5", + "omit_call_6", + "wrong_label_6", + "omit_call_7", + "wrong_label_7", + "omit_call_8", + "wrong_label_8", + "omit_call_9", + "wrong_label_9", + "omit_call_10", + "wrong_label_10", + "omit_call_11", + "wrong_label_11", + "nonidempotent", + "unpriced_c", + "zero_projector", + "out_of_range", + "unrestored_dirty_extra", + "both_images_miss_formal_dirty_shear" + ], + "proof_scope": "README theorem is universal; these checks are finite corroboration" + }, + "schema_version": 1, + "statement": "For every r>=k>=1, n_a>=2k and n_b>=2k; direct word attains4k." +} diff --git a/research/ut3-commutator-all-registers/CLAIM.json b/research/ut3-commutator-all-registers/CLAIM.json new file mode 100644 index 0000000000..00c806f37f --- /dev/null +++ b/research/ut3-commutator-all-registers/CLAIM.json @@ -0,0 +1,63 @@ +{ + "assignment_seed": 14, + "random_source": "Python secrets.randbelow(100), operating-system randomness", + "track": "bit supplier", + "base_commit": "680967accfd4311f3241dc154e1f434869747b43", + "started_utc": "2026-10-14T02:58:00Z", + "expected_finish_utc": "2026-10-14T03:58:00Z", + "object": "Formal F2[UT_3(F2)] paid a/b rank-one-idempotent register words for k central commutator targets and any finite restored dirty workspace", + "hypothesis": "The two natural three-dimensional representations interchanging a and b imply at least 2k a calls and 2k b calls; the direct 4k word attains both.", + "method": "Written dimension/rank argument via sum of rank-one projectors zero and two off-diagonal coefficient factorizations. Independent full formal-algebra and faithful-regular checks of attaining witnesses; semantic failure controls.", + "domain": "All integers r>=k>=1 in the proof; bounded exact controls use seed14 to select k=1+14%3=3 and one extra dirty register, plus smaller cases.", + "expected_deliverable": "Scoped sharp paid-call theorem or precise failed-lemma counterexample; self-contained proof, two implementations, certificate, provenance, no new kappa.", + "predecessor": { + "pr": 1478, + "author": "juper997", + "head": "b30fdba48f3db70e3589ba740b0782b56ec0ba2e", + "scope": "Two central targets, exactly two or three registers, finite radius-three census; explicitly leaves arbitrary workspace open." + }, + "candidate_tasks": [ + { + "task": "Replacement H2/K contract for one R439 helper star", + "decision": "Declined: existing semantic prefix and active interface work make duplication likely." + }, + { + "task": "Lower-frame resynthesis for R439 block509 exceptional source22", + "decision": "Declined: PR1535 inverse-frame obstruction overlaps the immediate next question." + }, + { + "task": "All-register central-commutator paid-call theorem", + "decision": "Chosen: removes PR1478 fixed-register restriction through two representations and rank factorization, rather than a larger census." + } + ], + "coordination": "No pinned issues returned by GitHub. Claim recorded locally per donor instruction. Read Discussion1163, handoffs1166, and UT3 comments in1317; overlap snapshot complete for718 open PRs and218 discussion records at2026-10-14T03:00:54Z.", + "optimistic_complete_cost": "Direct4k paid calls, no extra copies or clean registers, free scalar mixing only as explicitly allowed by this abstract model. No source-access, frame or supplier implementation is claimed.", + "stop_rule": "One algebraic proof attempt, at most45 minutes including implementation; final15 minutes reserved for independent checking and handoff. No expanded Cayley search.", + "credit": "steph4n-gh with substantial OpenAI Codex assistance; predecessor credit retained; Apache-2.0.", + "final_overlap": { + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T03:08:36.580730+00:00", + "complete_pagination": true, + "records": 725 + }, + "discussions": { + "fetched_at": "2026-10-14T03:08:58.777900+00:00", + "complete_pagination": true, + "records": 225 + } + }, + "terms": [ + "UT_3", + "UT3", + "commutator-register", + "commutator targets" + ], + "matches_total": 12, + "additional_predecessor": "PR1443 by woklerx, two-register D8 result at965ff75aabb16cdd0978f4bf9222bcdedf514021, found by broadening the final search to commutator targets; now pinned and credited.", + "concurrent_claim": "Discussion1569, Arham Tahir, created03:07UTC: arbitrary workspace for two targets. Our all-k theorem and separate2k per-label bounds add scope; no priority claimed for overlap." + }, + "status": "completed", + "result": "Written all-r/all-k sharp theorem: n_a>=2k, n_b>=2k, direct4k witness; two exact implementations and semantic controls pass. No new kappa.", + "result_link": "README.md" +} diff --git a/research/ut3-commutator-all-registers/README.md b/research/ut3-commutator-all-registers/README.md new file mode 100644 index 0000000000..4a6a4ee9d9 --- /dev/null +++ b/research/ut3-commutator-all-registers/README.md @@ -0,0 +1,214 @@ +# A sharp commutator call bound with arbitrary restored dirty workspace + +**Scoped theorem; no new kappa.** In the formal `F2[UT_3(F2)]` register +model of [PR1478](https://github.com/CrocSwap/integer-mult-bounds/pull/1478), +`k` central commutator targets require at least **2k calls of each generator**, +hence exactly **4k paid calls**, for every finite register count `r >= k >= 1`. +Any number of additional arbitrary dirty registers, restored at the endpoint, +cannot save calls. The direct construction attains both separate bounds. + +PR1443 by @woklerx established the two-register D8 case; PR1478 by @juper997 +established the eight-call minimum for two targets on exactly two or three +registers by a finite exhaustive census. Its explicit +open question was whether the restriction on workspace could be removed. +The proof below removes that restriction and handles any target count. It +uses two small representations and a rank inequality, with no census of +register words or extrapolation from tests. Credit for the model, earlier +finite result and question remains with PR1478 and its predecessors. + +The final overlap refresh found Arham Tahir's concurrent +[Discussion1569](https://github.com/CrocSwap/integer-mult-bounds/discussions/1569), +claiming the **two-target, arbitrary-register** case by a degree-two quotient +and separate label parity. This package's additional scope is **every target +count k**, with separate `2k` lower bounds for each label and the resulting +weighted tariff. It also supplies independently implemented exact witnesses +and failure controls. No priority is claimed for the overlapping two-target +case, and the concurrent claim is not used as an established premise. + +## Exact model and bill + +Let `G = UT_3(F2)` with elements `(x,y,z)` representing entries `01,12,02`. +Multiplication is + +`(x,y,z)(X,Y,Z) = (x+X, y+Y, z+Z+xY)`. + +Write `a = I+E01`, `b = I+E12`, and `c = abab = I+E02`. The group has eight +elements; `a,b,c` are involutions and `c` is central. Work over the **formal +group algebra** `R = F2[G]`, not only its natural three-dimensional image. +There are `r` scalar registers with arbitrary inputs. An allowed paid factor is + +`D_N(g) = I_r + ([g]+1) N`, + +where `g` is `a` or `b`, and `N = u v^T` is a binary rank-one idempotent: +`v^T u = 1`. Each occurrence costs one. Arbitrary scalar `GL_r(F2)` maps are +free. No other address operation, higher-rank paid call, clean allocation, +COPY, ERASE or free undo is admitted. The exact endpoint is + +`T = diag([c], ..., [c], 1, ..., 1) = I_r + ([c]+1) P`, + +where `P = diag(I_k,0)` has rank `k`. The last `r-k` roles are restored as +operators on **all** inputs, not merely initialized to zero. The same result +holds for a scalar conjugate of this endpoint, by changing the register basis. + +As in the predecessor's augmentation argument, interleaved free scalar maps +can be moved to one end by conjugating each `N`. Augmentation `[g] -> 1` +sends every paid factor and `T` to `I_r`, so that remaining scalar map is +`I_r`. Every conjugate of a rank-one idempotent is again an allowed projector. +It therefore suffices to consider a product of the displayed paid factors. + +The complete attaining word applies `(a,b,a,b)` to each of the first `k` +coordinate projectors. On that coordinate the product is `[abab]=[c]`; +on every other coordinate it is identity. It uses `2k` a-calls and `2k` +b-calls, exactly `k` data roles and `r-k` unused/restored dirty roles, with +no scalar mixing, source-access operation, copy or restoration outside those +`4k` calls. This is an abstract paid-call bill. It does not price an +implementation of these calls in the selected multiplication supplier. + +## Proof for all register counts + +All ranks and spans in this proof are over `F2`. Products are written in +left-to-right matrix order. Let `n_a,n_b` count the occurrences of the two +labels. For each label collect its column factors `u_j` as columns of `X_a` +or `X_b`, and its row factors `v_j^T` as rows of `Y_a` or `Y_b`. In particular, + +`sum_{a calls} N_j = X_a Y_a`, and similarly for `b`. + +**First representation.** Apply the natural representation of `G` entrywise +to the formal register matrix, and reorder coordinates into three address +blocks of size `r`. The two paid factors become + +```text +a: [ I N 0 ] b: [ I 0 0 ] + [ 0 I 0 ] [ 0 I N ] + [ 0 0 I ] [ 0 0 I ]. +``` + +Multiplying them gives diagonal blocks `I`, blocks `01` and `12` equal to +the respective projector sums, and block `02` equal to + +`C_ab = sum_{i 1 -> 2`. The exact formal target +therefore implies + +`X_a Y_a = 0`, `X_b Y_b = 0`, and `C_ab = P`. + +Each summand `N_i N_j = u_i (v_i^T u_j) v_j^T` has its column space in +`im X_a` and its row space in `row Y_b`. Consequently + +`rank X_a >= k`, `rank Y_b >= k`. + +**Second representation.** The map + +`sigma(x,y,z) = (y,x,z+xy)` + +is a group automorphism: substitution into the displayed group law verifies +multiplicativity, and `sigma^2` is identity. It swaps `a` and `b` and fixes +`c`. (Simply swapping `x,y` without the `xy` correction is not this map.) +Compose the natural representation with `sigma`. The same endpoint now +forces + +`C_ba = sum_{i= k`, `rank Y_a >= k`. + +**Dimension bound.** Since `X_a Y_a = 0`, the image of +`Y_a : F2^r -> F2^{n_a}` lies inside the kernel of +`X_a : F2^{n_a} -> F2^r`. Rank-nullity gives + +`rank X_a + rank Y_a <= n_a`. + +Both terms are at least `k`, so `n_a >= 2k`. Applying the same argument to +`b` gives `n_b >= 2k`. The direct word attains equality in both bounds. +This proves the stated minimum for every `r >= k`, without an upper bound +on dirty workspace or word length. + +For fixed positive per-label tariffs `cost(a)=alpha`, `cost(b)=beta`, the +same proof and witness give exactly `2k(alpha+beta)`. This corollary assumes +uniform prices within each label; it is not a statement about port-dependent +or word-dependent implementation overhead. + +Neither representation is faithful on the group algebra. They are used +only for necessary conditions in the lower bound. The attaining word is +proved in the formal algebra itself. In particular, the nonzero element +`lambda = ([a]+1)([c]+1)` is killed by **both** representations; a suitable +off-diagonal `lambda` perturbation of the endpoint must still be rejected. +The verification includes this control explicitly. + +## Reproduce and evidence boundary + +From the repository root, using Python 3.12 or later and its standard library: + +```sh +python3 -I -O -B research/ut3-commutator-all-registers/verify.py +``` + +`verify.py` uses formal group-algebra coefficients. `independent.py` imports +none of that implementation and constructs a faithful regular representation +from explicit binary address matrices. The committed `CERTIFICATE.json` +records their deterministic finite checks. The default command is read-only; +`--emit` prints a fresh receipt for comparison without overwriting files. +The registered replay is + +```sh +python3.12 scripts/research_package.py --package research/ut3-commutator-all-registers +``` + +The scripts check the algebraic maps, attaining words, full dirty boundaries +and semantic mutations. They are finite corroboration of the definitions and +witnesses. The argument above, not those finite fixtures, proves the unbounded +register and target statement. This is not a proof-assistant verification or +an independent human review. Exact executed coverage is in the certificate +and `VALIDATION.md`. + +## Provenance, selection and limits + +Base: `680967accfd4311f3241dc154e1f434869747b43`. OS assignment seed **14** +selected the bit-supplier track. Its residue selects the three-target, +one-dirty-extra fixture (`k = 1 + 14 mod 3 = 3`, `r = 4`) for emphasis; +the mathematical proof is seed-independent. `CLAIM.json` records all three +candidates, overlap checks, the local claim and the stopping rule. No pinned +sprint issue existed. `TASK.json` records the catalogue refinement. + +PR1478 is pinned at `b30fdba48f3db70e3589ba740b0782b56ec0ba2e`. +PR1443 is pinned at `965ff75aabb16cdd0978f4bf9222bcdedf514021`. +The selected record at the base is PR1094, conditional +`kappa = 0.001672660197076918`, with PR589 on PR555 as the bit supplier; +the complex supplier binds. `SOURCES.json` records exact contextual source +pins. No predecessor executable is imported or needed by the standalone check. + +This closes the arbitrary-workspace question for **these central targets +and this two-letter alphabet**. It does not exclude savings for other +targets, expanded address alphabets, clean/noninvertible workspace contracts, +or different realization interfaces. It neither reopens the already proved +abelian three-register result nor establishes an all-size rational-frame +identity. There is no proposed selected-supplier replacement, new paid rank +histogram, new kappa, physical compiler, hosting, precision/tape or analytic +transfer result. The selected construction and `upstream/` are unchanged. + +## Open next questions + +Can a legally priced larger address alphabet improve the complete supplier +budget? Allowing `c` itself at price `gamma` already offers the direct +`k*gamma` bill, while the proved two-letter bill is `2k(alpha+beta)`. +The first useful step is to specify and fully price one actual implementation +of the additional call, including frames and restoration, before any search. +The blocker is its realization in the supplier: declaring it a unit-cost +operation would change the model without establishing an improvement. +The present theorem settles the workspace-only route in the stated model. + +## Credit and disclosure + +Prepared for **steph4n-gh** with substantial **OpenAI Codex assistance** in +research, proof, implementation, independent AI checking and packaging. +Credit @juper997 (PR1478) for the finite commutator result and explicit +all-register question; @woklerx (PR1443) for the earlier two-register D8 +commutator result; Arham Tahir (Discussion1569) for the concurrent two-target +all-register argument; Gareth Davidson / @bitplane (PR1333) for the +restricted-alphabet direction and augmentation normalization; @commdata2338 +(PR1414) for the related coordinate-swap investigation; and eumemic (PR288), +Ali Romman (PR468), David Govea (PR720) and the retained register-model +lineage. No broader literature-priority claim is made. Apache-2.0. diff --git a/research/ut3-commutator-all-registers/SOURCES.json b/research/ut3-commutator-all-registers/SOURCES.json new file mode 100644 index 0000000000..d779edd61f --- /dev/null +++ b/research/ut3-commutator-all-registers/SOURCES.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "base_commit": "680967accfd4311f3241dc154e1f434869747b43", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + } + ], + "contextual_predecessors": [ + { + "pr": 1478, + "author": "juper997", + "commit": "b30fdba48f3db70e3589ba740b0782b56ec0ba2e", + "path": "research/ut3-commutator-register-bound/README.md", + "git_blob": "26af5fcb949eb68e6a43001fe1debd2d465b0504", + "sha256": "6a8c399bfc765050ee80a20ec83251cfcf435b90ad528a6f4ae4f7f770991e59", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/b30fdba48f3db70e3589ba740b0782b56ec0ba2e/research/ut3-commutator-register-bound/README.md", + "usage": "Contextual model, prior finite result and open question. No imported implementation or premise of its finite census is needed by this proof." + }, + { + "pr": 1443, + "author": "woklerx", + "commit": "965ff75aabb16cdd0978f4bf9222bcdedf514021", + "path": "research/bit-dihedral-commutator/README.md", + "git_blob": "b7619a5d56f32daf7f48d6cc3a0e260c5a333510", + "sha256": "4f3f9df6d6d96a26ccb0fcd2ef947cce5d53b0d992da22e866f1e025be4c0492", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/965ff75aabb16cdd0978f4bf9222bcdedf514021/research/bit-dihedral-commutator/README.md", + "usage": "Earlier two-register finite D8 commutator result. Context only; no executable or census imported." + } + ], + "standalone_dependencies": "Python standard library and this package only; no external proof-relevant runtime inputs.", + "concurrent_work": [ + { + "discussion": 1569, + "author": "Arham Tahir", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1569", + "created_at_utc": "2026-10-14T03:07:00Z", + "observed_status": "Claim, not an accepted proof", + "scope": "Two targets and arbitrary restored dirty register count via degree-two quotient and parity; our theorem covers all target counts via paired representations and span ranks." + } + ] +} diff --git a/research/ut3-commutator-all-registers/TASK.json b/research/ut3-commutator-all-registers/TASK.json new file mode 100644 index 0000000000..b6fba563ea --- /dev/null +++ b/research/ut3-commutator-all-registers/TASK.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "680967accfd4311f3241dc154e1f434869747b43", + "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": "refined", + "actual_scope": "Sharp all-register bound for k central UT3 commutator targets with rank-one a/b paid calls and arbitrary restored dirty workspace.", + "scope_change_reason": "Fix the nonabelian group and endpoint from PR1478, then remove its fixed-register restriction through a written rank argument rather than enlarging the finite census.", + "bottleneck_link": "Closes the workspace-only escape for this explicit bit-register relaxation. This scoped obstruction does not change the selected paid profile or kappa.", + "budget_minutes": 60, + "stop_rule": "One structural proof attempt; no larger Cayley census. Reserve final quarter of actual session for independent proof/code review, replay and handoff.", + "outcome": "negative-result", + "evidence": "README universal rank proof; formal-coefficient and code-disjoint faithful-regular finite checks; CERTIFICATE.json and VALIDATION.md.", + "author": "steph4n-gh", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, packaging and independent AI checks by two delegated workers. No independent human or proof-assistant review.", + "assignment_seed": 14, + "open_questions": [ + { + "question": "Can an explicitly implemented, legally priced expanded address alphabet improve the complete supplier budget?", + "why_it_matters": "The theorem closes workspace-only savings for central targets under the two-label alphabet; changing the alphabet is a material way outside its scope.", + "first_step": "Specify one implementation of an additional call such as c, price every frame and restoration, and compare its direct k*gamma bill to2k*(alpha+beta).", + "blocked_by": "No realization or full supplier cost of the added operation is established by this package." + } + ] +} diff --git a/research/ut3-commutator-all-registers/VALIDATION.md b/research/ut3-commutator-all-registers/VALIDATION.md new file mode 100644 index 0000000000..a6313b8109 --- /dev/null +++ b/research/ut3-commutator-all-registers/VALIDATION.md @@ -0,0 +1,91 @@ +# Executed validation + +Base: `680967accfd4311f3241dc154e1f434869747b43`. +Local execution: October 13, 2026, America/New_York (October 14 UTC), +macOS arm64, Python 3.12.9 and 3.14.4, standard library only. + +The written proof was independently reviewed by a delegated Codex worker; +a second worker wrote `independent.py` without importing the primary or +predecessor implementation and reviewed the primary implementation afterward. +Both final reviews reported no actionable defect. This is independent AI +checking, not independent human review or proof-assistant verification. + +## Passing commands + +```sh +python3 -I -O -B research/ut3-commutator-all-registers/verify.py +python3 -I -B research/ut3-commutator-all-registers/verify.py +python3 scripts/research_package.py --package research/ut3-commutator-all-registers --check-only +python3.12 scripts/research_package.py --package research/ut3-commutator-all-registers +python3 -B scripts/research_baseline.py +make selected-record-check +git diff --check +``` + +The local Python 3.12 command used the already installed interpreter at +`~/.local/share/uv/python/cpython-3.12.9-macos-aarch64-none/bin/python3.12`. +The registered replay passed with `outcome=negative-result`; both standalone +runs printed `PASS_UT3_ALL_REGISTERS`. The baseline reported the complex side +binding and `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. The selected-record check +validated the unchanged conditional `836330098538459/500000000000000000`. +The latter two commands establish orientation/source integrity, not a fresh +selected-supplier cold replay. + +## Exact finite evidence + +`CERTIFICATE.json` is reproduced and compared in full by the standalone +command. No files are generated by the default replay. + +- Primary engine: all 512 group associativity cases, all 64 products for each + small representation, 30 full formal endpoint fixtures for every + `1 <= k <= r <= 5` in coordinate and mixed bases, 75 deterministic + arbitrary-word formula checks, and 30 rejected semantic mutations. +- Independent engine: all 64 group products in natural, swapped and faithful + regular representations; rank eight for the regular group-algebra basis; + 45 complete operator fixtures on matrices up to 40 by 40; 195 arbitrary-word + factorization checks; and 151 rejected semantic mutations. +- Both engines reject dirty-boundary errors invisible to both small proof + representations. The primary also checks actual cheaper witnesses after + removing either the two-label or rank-one-call restriction. These are + counterexamples to broader claims, not legal improvements within the model. + +The universal statement comes from the written rank proof. These finite +fixtures are not an enumeration of all circuits or a formal proof of that +universal statement. Their seed is 14; their loops terminate at the explicit +fixture ranges, without optimizer restarts or larger-search escalation. + +## Relocation and corruption controls + +Copied only `verify.py`, `independent.py` and `CERTIFICATE.json` into a fresh +temporary directory outside Git. Set those files read-only and the directory +nonwritable. Running the optimized command from that directory passed in +0.2221 seconds on the measured host, and all file hashes were unchanged. +This is one observed replay time, not a performance claim. + +In separate writable copies, each of the following failed with exit code one: + +| Mutation | Observed rejection | +|---|---| +| Change the receipt's `no_new_kappa` field | `certificate differs` | +| Remove the `xy` correction from the swap automorphism | `automorphism` | +| Remove the final `b` in every attaining `abab` word | `formal dirty endpoint` | + +Main-context source pins passed the registered metadata check. Both contextual +predecessor READMEs were fetched at their exact PR heads and bound to their +Git blobs and SHA256 values; no predecessor code is executed by the package. + +## Overlap and outstanding scope + +The final overlap refresh covered 725 open PRs and 225 discussion records, +with complete reported pagination, at 03:08:36/03:08:58 UTC. It found the +earlier PR1443 two-register result and the concurrent Discussion1569 claim +for two targets with arbitrary workspace. Both are credited in the README +and exact provenance is recorded in `SOURCES.json` and `CLAIM.json`. +This package adds every target count `k` and a sharp separate bound for each +generator. No priority is claimed for the shared two-target conclusion. +The base remained the upstream main head at the publication check. + +No selected-supplier cold replay, native compiler, physical hosting, +precision/tape, analytic transfer or Lean proof was run or established. +Hosted CI is separate from the completed local checks. No change to kappa, +the selected frontier, frozen predecessor files or `upstream/` is proposed. diff --git a/research/ut3-commutator-all-registers/VERIFY.json b/research/ut3-commutator-all-registers/VERIFY.json new file mode 100644 index 0000000000..a8a761a63f --- /dev/null +++ b/research/ut3-commutator-all-registers/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Both exact engines, full dirty endpoints, paired representation/rank identities, semantic mutants and frozen receipt comparison." + } + ] +} diff --git a/research/ut3-commutator-all-registers/independent.py b/research/ut3-commutator-all-registers/independent.py new file mode 100644 index 0000000000..b92331ac29 --- /dev/null +++ b/research/ut3-commutator-all-registers/independent.py @@ -0,0 +1,376 @@ +#!/usr/bin/env python3 +"""Code-disjoint finite checks using binary address matrices and regular action. + +No group triples, formal group-algebra arithmetic, producer imports, or external +packages are used. Finite success supports the fixtures, not the universal +rank proof. Matrix products use the written left-to-right factor order. + +steph4n-gh, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from dataclasses import dataclass +import hashlib +import json +import random + + +@dataclass(frozen=True) +class Matrix: + """Exact GF(2) matrix, storing each row as a bitset (bit j = column j).""" + + rows: tuple + width: int + + def __post_init__(self): + if self.width < 0 or any(x < 0 or x >> self.width for x in self.rows): + raise ValueError("invalid binary matrix") + + @property + def height(self): + return len(self.rows) + + def __xor__(self, other): + require((self.height, self.width) == (other.height, other.width), + "addition dimensions") + return Matrix(tuple(a ^ b for a, b in zip(self.rows, other.rows)), self.width) + + def __matmul__(self, other): + require(self.width == other.height, "product dimensions") + result = [] + for row in self.rows: + total = 0 + while row: + bit = row & -row + total ^= other.rows[bit.bit_length() - 1] + row ^= bit + result.append(total) + return Matrix(tuple(result), other.width) + + def rank(self): + pivots = {} + for row in self.rows: + while row: + col = row.bit_length() - 1 + if col not in pivots: + pivots[col] = row + break + row ^= pivots[col] + return len(pivots) + + def transpose(self): + return Matrix(tuple(sum(((row >> j) & 1) << i + for i, row in enumerate(self.rows)) + for j in range(self.width)), self.height) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return Matrix(tuple(1 << i for i in range(n)), n) + + +def zero(height, width): + return Matrix((0,) * height, width) + + +def unit(n, i, j): + return Matrix(tuple((1 << j) if row == i else 0 for row in range(n)), n) + + +def xor_sum(matrices, height, width): + out = zero(height, width) + for matrix in matrices: + out = out ^ matrix + return out + + +def kron(left, right): + rows = [] + for outer in left.rows: + for inner in right.rows: + row = 0 + for j in range(left.width): + if (outer >> j) & 1: + row ^= inner << (j * right.width) + rows.append(row) + return Matrix(tuple(rows), left.width * right.width) + + +def inverse(matrix): + n = matrix.height + require(n == matrix.width, "inverse needs a square matrix") + rows = [row | (1 << (n + i)) for i, row in enumerate(matrix.rows)] + for col in range(n): + pivot = next((i for i in range(col, n) if (rows[i] >> col) & 1), None) + require(pivot is not None, "singular scalar change of basis") + rows[col], rows[pivot] = rows[pivot], rows[col] + for i in range(n): + if i != col and ((rows[i] >> col) & 1): + rows[i] ^= rows[col] + out = Matrix(tuple(row >> n for row in rows), n) + require(matrix @ out == identity(n) and out @ matrix == identity(n), + "inverse round trip") + return out + + +def product(factors, n): + out = identity(n) + for factor in factors: + out = out @ factor + return out + + +def address_group(): + """Enumerate the group by closure of concrete three-by-three matrices.""" + eye = identity(3) + generators = {"a": eye ^ unit(3, 0, 1), "b": eye ^ unit(3, 1, 2)} + words = {eye: ""} + queue = [eye] + for element in queue: + for label in ("a", "b"): + new = element @ generators[label] + if new not in words: + words[new] = words[element] + label + queue.append(new) + require(len(queue) == 8, "UT3 order") + natural = {element: product((generators[label] for label in word), 3) + for element, word in words.items()} + swapped = {element: product((generators[{"a": "b", "b": "a"}[label]] + for label in word), 3) + for element, word in words.items()} + indices = {element: index for index, element in enumerate(queue)} + regular = {} + for element in queue: + rows = [0] * 8 + for column, basis in enumerate(queue): + rows[indices[element @ basis]] |= 1 << column + regular[element] = Matrix(tuple(rows), 8) + require(len(set(regular.values())) == 8, "faithful regular representation") + flattened = Matrix(tuple(sum(row << (8 * i) for i, row in enumerate(g.rows)) + for g in regular.values()), 64) + require(flattened.rank() == 8, "group-algebra regular map is not injective") + for left in queue: + for right in queue: + composed = left @ right + require(composed in indices, "group closure") + require(swapped[composed] == swapped[left] @ swapped[right], + "swapped homomorphism") + require(regular[composed] == regular[left] @ regular[right], + "regular homomorphism") + require(natural[composed] == natural[left] @ natural[right], + "natural homomorphism from independently enumerated words") + central = product((generators[x] for x in "abab"), 3) + require(central == eye ^ unit(3, 0, 2), "natural central image") + require(swapped[central] == eye ^ unit(3, 0, 2), "swapped central image") + require(central != eye and central @ central == eye, "central involution") + require(all(central @ g == g @ central for g in queue), "centrality") + # A single flipped regular-action entry must violate a multiplication law. + broken = dict(regular) + original = broken[generators["a"]] + changed_rows = list(original.rows) + changed_rows[0] ^= 1 + broken[generators["a"]] = Matrix(tuple(changed_rows), 8) + require(any(broken[x @ y] != broken[x] @ broken[y] + for x in queue for y in queue), "corrupted regular matrix accepted") + return generators, swapped, regular, central + + +def basis_change(n, variant): + out = identity(n) + if variant and n > 1: + # Common public fixture: factors are multiplied in displayed order. + for i in range(n): + out = out @ (identity(n) ^ unit(n, i, (i + 1) % n)) + if variant == 2 and n > 1: + for i in range(n - 1, 0, -1): + out = out @ (identity(n) ^ unit(n, i, i - 1)) + return out + + +def projectors(change): + n = change.height + back = inverse(change) + out = [] + for i in range(n): + column = Matrix(tuple((row >> i) & 1 for row in change.rows), 1) + row = Matrix((back.rows[i],), n) + p = column @ row + require(p.rank() == 1 and p @ p == p, "rank-one idempotent premise") + require(row @ column == identity(1), "dual scalar vectors") + require(p == change @ unit(n, i, i) @ back, "projector conjugation") + out.append((p, column, row)) + require(xor_sum((p for p, _, _ in out), n, n) == identity(n), + "projector resolution") + return out + + +def lifted_word(word, representation, generators, roles): + dimension = next(iter(representation.values())).height + eye = identity(roles * dimension) + return product((eye ^ kron(p, representation[generators[label]] ^ identity(dimension)) + for label, p, _, _ in word), roles * dimension) + + +def block(matrix, address_row, address_col, roles): + """Extract a role matrix from the role-major natural address operator.""" + return Matrix(tuple(sum(((matrix.rows[3 * i + address_row] >> + (3 * j + address_col)) & 1) << j + for j in range(roles)) + for i in range(roles)), roles) + + +def rank_premises(word, generators, swapped, roles): + natural = {g: g for g in swapped} + full = lifted_word(word, natural, generators, roles) + reverse = lifted_word(word, swapped, generators, roles) + sums = {label: xor_sum((p for tag, p, _, _ in word if tag == label), roles, roles) + for label in ("a", "b")} + c = xor_sum((p @ q for i, (tag, p, _, _) in enumerate(word) + for label, q, _, _ in word[i + 1:] if tag == "a" and label == "b"), + roles, roles) + cp = xor_sum((p @ q for i, (tag, p, _, _) in enumerate(word) + for label, q, _, _ in word[i + 1:] if tag == "b" and label == "a"), + roles, roles) + expected = [[identity(roles), sums["a"], c], + [zero(roles, roles), identity(roles), sums["b"]], + [zero(roles, roles), zero(roles, roles), identity(roles)]] + reverse_expected = [[identity(roles), sums["b"], cp], + [zero(roles, roles), identity(roles), sums["a"]], + [zero(roles, roles), zero(roles, roles), identity(roles)]] + for i in range(3): + for j in range(3): + require(block(full, i, j, roles) == expected[i][j], + "natural coefficient expansion") + require(block(reverse, i, j, roles) == reverse_expected[i][j], + "swapped coefficient expansion") + ranks = {} + for label, column_target, row_target in (("a", c, cp), ("b", cp, c)): + other = {"a": "b", "b": "a"}[label] + selected = [(i, u, v) for i, (tag, _, u, v) in enumerate(word) if tag == label] + count = len(selected) + x = Matrix(tuple(sum(u.rows[row] << i for i, (_, u, _) in enumerate(selected)) + for row in range(roles)), count) + y = Matrix(tuple(v.rows[0] for _, _, v in selected), roles) + right_rows = [] + left_columns = [] + for index, u, v in selected: + suffix = xor_sum((p for tag, p, _, _ in word[index + 1:] if tag == other), + roles, roles) + prefix = xor_sum((p for tag, p, _, _ in word[:index] if tag == other), + roles, roles) + right_rows.append((v @ suffix).rows[0]) + left_columns.append(prefix @ u) + right = Matrix(tuple(right_rows), roles) + left = Matrix(tuple(sum(u.rows[row] << i for i, u in enumerate(left_columns)) + for row in range(roles)), count) + require(x @ y == sums[label], "rank-factorization zero-sum premise") + require(x @ right == column_target, "column-span factorization") + require(left @ y == row_target, "row-span factorization") + xr, yr, sr = x.rank(), y.rank(), sums[label].rank() + require(column_target.rank() <= xr and row_target.rank() <= yr, + "rank monotonicity") + require(xr + yr <= count + sr, "Sylvester rank inequality") + if sums[label] == zero(roles, roles): + require(xr + yr <= count, "zero-sum dimension premise") + ranks[label] = {"calls": count, "column_rank": xr, "row_rank": yr} + return sums, c, cp, ranks + + +def run(): + generators, swapped, regular, central = address_group() + cases = [] + matrix_hash = hashlib.sha256() + negatives = {"missing_call": 0, "wrong_label": 0, "extra_dirty_target": 0, + "corrupted_regular_matrix": 1, "representation_invisible_dirty_shear": 0} + # Both small representations have a common kernel. The regular one must + # detect this nonzero group-algebra element, not certify its image as zero. + regular_kernel = ((regular[generators["a"]] ^ identity(8)) @ + (regular[central] ^ identity(8))) + natural_kernel = ((generators["a"] ^ identity(3)) @ (central ^ identity(3))) + swapped_kernel = ((swapped[generators["a"]] ^ identity(3)) @ + (swapped[central] ^ identity(3))) + require(regular_kernel != zero(8, 8), "formal kernel element vanished in regular action") + require(natural_kernel == swapped_kernel == zero(3, 3), "common representation kernel") + arbitrary_cases = 0 + rng = random.Random(14) + for roles in range(1, 6): + for variant in range(3): + change = basis_change(roles, variant) + ps = projectors(change) + for targets in range(1, roles + 1): + ptarget = xor_sum((p for p, _, _ in ps[:targets]), roles, roles) + word = [(label, p, u, v) for p, u, v in ps[:targets] for label in "abab"] + actual = lifted_word(word, regular, generators, roles) + expected = identity(8 * roles) ^ kron(ptarget, regular[central] ^ identity(8)) + require(actual == expected, "faithful full operator endpoint") + require(ptarget.rank() == targets, "target rank") + # Conjugating back exposes every arbitrary dirty spectator as I_8. + original_basis = kron(inverse(change), identity(8)) @ actual @ kron(change, identity(8)) + coordinate_target = xor_sum((unit(roles, i, i) for i in range(targets)), roles, roles) + require(original_basis == identity(8 * roles) ^ + kron(coordinate_target, regular[central] ^ identity(8)), + "dirty spectators not restored") + sums, c, cp, ranks = rank_premises(word, generators, swapped, roles) + require(sums["a"] == sums["b"] == zero(roles, roles), "endpoint zero sums") + require(c == cp == ptarget, "both endpoint coefficients") + for label in ("a", "b"): + require(ranks[label] == {"calls": 2 * targets, "column_rank": targets, + "row_rank": targets}, "sharp witness ranks") + require(lifted_word(word[:-1], regular, generators, roles) != expected, + "missing-call control accepted") + negatives["missing_call"] += 1 + wrong = [("b", word[0][1], word[0][2], word[0][3])] + word[1:] + require(lifted_word(wrong, regular, generators, roles) != expected, + "wrong-label control accepted") + negatives["wrong_label"] += 1 + if targets < roles: + bad_target = expected ^ kron(ps[targets][0], regular[central] ^ identity(8)) + require(actual != bad_target, "extra dirty target control accepted") + negatives["extra_dirty_target"] += 1 + dirty_shear_role = change @ unit(roles, roles - 1, 0) @ inverse(change) + shear = identity(8 * roles) ^ kron(dirty_shear_role, regular_kernel) + require(shear @ shear == identity(8 * roles), "dirty shear involution") + mutant = actual @ shear + require(mutant != expected, "representation-invisible dirty shear accepted") + require(identity(3 * roles) ^ kron(dirty_shear_role, natural_kernel) == + identity(3 * roles), "natural image should miss dirty shear") + require(identity(3 * roles) ^ kron(dirty_shear_role, swapped_kernel) == + identity(3 * roles), "swapped image should miss dirty shear") + negatives["representation_invisible_dirty_shear"] += 1 + matrix_hash.update(json.dumps([roles, targets, variant, actual.rows], + separators=(",", ":")).encode()) + cases.append({"roles": roles, "targets": targets, "basis_variant": variant, + "paid_calls": len(word), "a_calls": ranks["a"]["calls"], + "b_calls": ranks["b"]["calls"]}) + # These deliberately need not restore spectators or reach a target. + # They check the expansion and factorization independently of abab. + for length in range(13): + pool = ps + projectors(basis_change(roles, (variant + 1) % 3)) + word = [(rng.choice(("a", "b")), *rng.choice(pool)) for _ in range(length)] + rank_premises(word, generators, swapped, roles) + arbitrary_cases += 1 + return { + "schema": "ut3-independent-binary-matrix-check-v1", + "arithmetic": "GF(2), exact integer bitsets", + "group_elements": 8, + "regular_group_algebra_basis_rank": 8, + "homomorphism_products_per_representation": 64, + "representations": ["natural 3x3", "generator-swapped 3x3", "faithful regular 8x8"], + "natural_and_swapped_c": "I_3 + E_02", + "attaining_operator_cases": len(cases), + "arbitrary_word_factorization_cases": arbitrary_cases, + "maximum_regular_operator_dimension": 40, + "roles_checked": [1, 2, 3, 4, 5], + "targets_checked": "every 1 <= k <= r", + "scalar_basis_variants_per_pair": 3, + "negative_controls_rejected": negatives, + "exact_operators_sha256": matrix_hash.hexdigest(), + "cases": cases, + "scope": "Finite exact checks only; the all-register theorem requires the written proof." + } + + +if __name__ == "__main__": + print(json.dumps(run(), indent=2, sort_keys=True)) diff --git a/research/ut3-commutator-all-registers/verify.py b/research/ut3-commutator-all-registers/verify.py new file mode 100644 index 0000000000..a359dabf83 --- /dev/null +++ b/research/ut3-commutator-all-registers/verify.py @@ -0,0 +1,331 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written all-register UT3 theorem. + +steph4n-gh, with substantial OpenAI Codex assistance. Apache-2.0. +The universal lower bound is the README proof, not a finite search here. +""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path +import random + + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def group_mul(g, h): + x, y, z = g & 1, (g >> 1) & 1, (g >> 2) & 1 + X, Y, Z = h & 1, (h >> 1) & 1, (h >> 2) & 1 + return (x ^ X) | ((y ^ Y) << 1) | ((z ^ Z ^ (x & Y)) << 2) + + +def swap(g): + x, y, z = g & 1, (g >> 1) & 1, (g >> 2) & 1 + return y | (x << 1) | ((z ^ (x & y)) << 2) + + +def coeff_mul(left, right): + value = 0 + for g in range(8): + if (left >> g) & 1: + for h in range(8): + if (right >> h) & 1: + value ^= 1 << group_mul(g, h) + return value + + +def fid(r): + return tuple(tuple(int(i == j) for j in range(r)) for i in range(r)) + + +def fmul(left, right): + r = len(left) + out = [[0] * r for _ in range(r)] + for i in range(r): + for k in range(r): + if left[i][k]: + for j in range(r): + out[i][j] ^= coeff_mul(left[i][k], right[k][j]) + return tuple(map(tuple, out)) + + +def bid(r): + return tuple(1 << i for i in range(r)) + + +def bmul(left, right): + out = [] + for row in left: + value = 0 + for i, source in enumerate(right): + if (row >> i) & 1: + value ^= source + out.append(value) + return tuple(out) + + +def bxor(left, right): + return tuple(a ^ b for a, b in zip(left, right)) + + +def rank(rows): + pivots = {} + for row in rows: + while row: + p = row.bit_length() - 1 + if p in pivots: + row ^= pivots[p] + else: + pivots[p] = row + break + return len(pivots) + + +def projector(r, u, v): + require(0 < u < 1 << r and 0 < v < 1 << r, 'projector dimensions') + require((u & v).bit_count() % 2 == 1, 'projector is not idempotent') + return tuple(v if (u >> i) & 1 else 0 for i in range(r)) + + +def factor(r, call): + label, u, v = call + require(label in (1, 2), 'unpriced address label') + n = projector(r, u, v) + delta = (1 << label) ^ 1 + return tuple(tuple(int(i == j) ^ (delta if (n[i] >> j) & 1 else 0) + for j in range(r)) for i in range(r)) + + +def word_matrix(r, word): + out = fid(r) + for call in word: + out = fmul(out, factor(r, call)) + return out + + +def target(r, k): + require(1 <= k <= r, 'target dimensions') + return tuple(tuple((1 << 4 if i < k else 1) if i == j else 0 + for j in range(r)) for i in range(r)) + + +def scalar_form(rows): + r = len(rows) + return tuple(tuple((row >> j) & 1 for j in range(r)) for row in rows) + + +def bases(r): + s, inv = bid(r), bid(r) + if r > 1: + for i in range(r): + e = list(bid(r)) + e[i] ^= 1 << ((i + 1) % r) + s = bmul(s, e) + inv = bmul(e, inv) + require(bmul(s, inv) == bid(r), 'basis inverse') + return s, inv + + +def witness(r, k, mixed=False): + s, inv = bases(r) if mixed else (bid(r), bid(r)) + word = [] + for i in range(k): + u = sum(((s[j] >> i) & 1) << j for j in range(r)) + v = inv[i] + word.extend((g, u, v) for g in (1, 2, 1, 2)) + expected = fmul(fmul(scalar_form(s), target(r, k)), scalar_form(inv)) + p = bmul(bmul(s, tuple(1 << i if i < k else 0 for i in range(r))), inv) + return word, expected, p + + +def natural(g): + return (1 | ((g & 1) << 1) | (((g >> 2) & 1) << 2), + 2 | (((g >> 1) & 1) << 2), 4) + + +def image(matrix, swapped=False): + r = len(matrix) + out = [0] * (3 * r) + for i in range(r): + for j in range(r): + for g in range(8): + if (matrix[i][j] >> g) & 1: + rep = natural(swap(g) if swapped else g) + for a in range(3): + for b in range(3): + if (rep[a] >> b) & 1: + out[a * r + i] ^= 1 << (b * r + j) + return tuple(out) + + +def block(matrix, r, a, b): + return tuple((matrix[a * r + i] >> (b * r)) & ((1 << r) - 1) + for i in range(r)) + + +def rank_evidence(r, word, formal, expected_p=None): + zero = (0,) * r + sums = {1: zero, 2: zero} + cross = {(1, 2): zero, (2, 1): zero} + for g, u, v in word: + n = projector(r, u, v) + other = 3 - g + cross[other, g] = bxor(cross[other, g], bmul(sums[other], n)) + sums[g] = bxor(sums[g], n) + span_ranks = {} + for g in (1, 2): + calls = [(u, v) for label, u, v in word if label == g] + x = tuple(sum(((u >> i) & 1) << j for j, (u, v) in enumerate(calls)) + for i in range(r)) + y = tuple(v for u, v in calls) + require(bmul(x, y) == sums[g], 'sum factorization') + rx, ry = rank(x), rank(y) + require(rx + ry <= len(calls) + rank(sums[g]), 'rank inequality') + span_ranks[g] = (rx, ry, len(calls)) + for swapped in (False, True): + a, b = (2, 1) if swapped else (1, 2) + rep = image(formal, swapped) + for i in range(3): + for j in range(3): + expected = (bid(r) if i == j else sums[a] if (i, j) == (0, 1) + else sums[b] if (i, j) == (1, 2) + else cross[a, b] if (i, j) == (0, 2) else zero) + require(block(rep, r, i, j) == expected, 'representation block formula') + require(rank(cross[a, b]) <= min(span_ranks[a][0], span_ranks[b][1]), + 'cross span bounds') + if expected_p is not None: + k = rank(expected_p) + require(sums[1] == sums[2] == zero, 'target linear blocks') + require(cross[1, 2] == cross[2, 1] == expected_p, 'target cross blocks') + for g in (1, 2): + rx, ry, count = span_ranks[g] + require(rx >= k and ry >= k and count >= 2 * k, 'target call bound') + return {str(g): list(span_ranks[g]) for g in (1, 2)} + + +def primary(): + for g in range(8): + require(swap(swap(g)) == g, 'automorphism involution') + for h in range(8): + require(swap(group_mul(g, h)) == group_mul(swap(g), swap(h)), 'automorphism') + for switched in (False, True): + phi = lambda x: natural(swap(x) if switched else x) + require(phi(group_mul(g, h)) == bmul(phi(g), phi(h)), 'homomorphism') + for f in range(8): + require(group_mul(group_mul(g, h), f) == group_mul(g, group_mul(h, f)), + 'group associativity') + require(group_mul(group_mul(group_mul(1, 2), 1), 2) == 4, 'central commutator') + fixtures = [] + digest = hashlib.sha256() + for r in range(1, 6): + for k in range(1, r + 1): + for mixed in (False, True): + word, expected, p = witness(r, k, mixed) + actual = word_matrix(r, word) + require(actual == expected, 'formal dirty endpoint') + ranks = rank_evidence(r, word, actual, p) + require(len(word) == 4 * k, 'complete witness bill') + digest.update(bytes(value for row in actual for value in row)) + fixtures.append({'r': r, 'k': k, 'mixed': mixed, 'calls': 4 * k, + 'a_b_span_ranks_and_counts': ranks}) + # Deterministic formula checks, not an optimality search or claimed coverage. + rng = random.Random(14) + for r in range(1, 6): + for length in range(15): + word = [] + for _ in range(length): + u = rng.randrange(1, 1 << r) + choices = [v for v in range(1, 1 << r) if (u & v).bit_count() % 2] + word.append((rng.choice((1, 2)), u, rng.choice(choices))) + rank_evidence(r, word, word_matrix(r, word)) + controls = [] + r, k = 4, 3 + word, expected, _ = witness(r, k, True) + for i in range(len(word)): + require(word_matrix(r, word[:i] + word[i + 1:]) != expected, 'omission accepted') + controls.append('omit_call_' + str(i)) + changed = list(word) + g, u, v = changed[i] + changed[i] = (3 - g, u, v) + require(word_matrix(r, changed) != expected, 'wrong label accepted') + controls.append('wrong_label_' + str(i)) + for label, call in [('nonidempotent', (1, 1, 2)), ('unpriced_c', (4, 1, 1)), + ('zero_projector', (1, 0, 1)), ('out_of_range', (1, 16, 1))]: + try: + factor(r, call) + except ValueError: + controls.append(label) + else: + raise ValueError('invalid call accepted: ' + label) + direct, expected, _ = witness(r, k) + dirty = direct + [(g, 8, 8) for g in (1, 2, 1, 2)] + require(word_matrix(r, dirty) != expected, 'dirty extra not restored') + controls.append('unrestored_dirty_extra') + lam = coeff_mul((1 << 1) ^ 1, (1 << 4) ^ 1) + require(lam != 0, 'nonfaithfulness fixture vanished formally') + mutation = [list(row) for row in fid(r)] + mutation[3][0] ^= lam + mutation = tuple(map(tuple, mutation)) + require(fmul(mutation, mutation) == fid(r), 'dirty shear invertibility') + fake = fmul(expected, mutation) + require(fake != expected, 'formal mutation accepted') + for switched in (False, True): + require(image(fake, switched) == image(expected, switched), + 'intended invisible representation control') + controls.append('both_images_miss_formal_dirty_shear') + # Exact counterexamples to dropping either alphabet/rank-one hypothesis. + c_word = fid(r) + for i in range(k): + f = [list(row) for row in fid(r)] + f[i][i] = 1 << 4 + c_word = fmul(c_word, tuple(map(tuple, f))) + require(c_word == expected, 'expanded c-alphabet witness') + higher_rank_word = fid(r) + for g in (1, 2, 1, 2): + f = tuple(tuple((1 << g if i < k else 1) if i == j else 0 + for j in range(r)) for i in range(r)) + higher_rank_word = fmul(higher_rank_word, f) + require(higher_rank_word == expected and k > 1, 'higher-rank-call witness') + return {'method': 'formal group-algebra coefficients with triple group law', + 'group_associativity_cases': 512, 'homomorphism_cases_per_representation': 64, + 'fixtures': fixtures, 'formal_endpoint_sha256': digest.hexdigest(), + 'arbitrary_word_formula_fixtures': 75, 'formula_fixture_seed': 14, + 'negative_controls': controls, 'invisible_nonzero_coefficient_mask': lam, + 'hypothesis_boundary_witnesses': { + 'expanded_c_alphabet': {'r': r, 'k': k, 'calls': k}, + 'rank_k_paid_projectors': {'r': r, 'k': k, 'calls': 4}}, + 'proof_scope': 'README theorem is universal; these checks are finite corroboration'} + + +def run(): + spec = importlib.util.spec_from_file_location('ut3_independent', HERE / 'independent.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return {'schema_version': 1, 'primary': primary(), 'independent': module.run(), + 'statement': 'For every r>=k>=1, n_a>=2k and n_b>=2k; direct word attains4k.', + 'no_new_kappa': True} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true', help='print receipt without writing files') + args = parser.parse_args() + receipt = run() + if args.emit: + print(json.dumps(receipt, sort_keys=True, indent=2)) + else: + expected = json.loads((HERE / 'CERTIFICATE.json').read_text()) + require(receipt == expected, 'certificate differs; inspect exact evidence before updating') + print('PASS_UT3_ALL_REGISTERS minimum=4k a_calls>=2k b_calls>=2k ' + 'proof=all_r>=k>=1 finite_fixtures=see_certificate no_new_kappa') + + +if __name__ == '__main__': + main()