From 0cee0e104b68ce6f06bf84af03f46ac30680e64c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 00:27:57 +0000 Subject: [PATCH 01/10] feat(research): prove the conjugate-pair four-call floor in every group Corner sandwiches with the first and last projectors replace the group-specific support filter of #4089 and #4093, so the floor holds for every noncommuting pair, coefficient field and width. --- research/conjugate-pair-every-group/PROOF.md | 151 ++++++++ research/conjugate-pair-every-group/README.md | 106 ++++++ .../conjugate-pair-every-group/SOURCES.json | 36 ++ research/conjugate-pair-every-group/TASK.json | 70 ++++ .../conjugate-pair-every-group/VERIFY.json | 32 ++ research/conjugate-pair-every-group/verify.py | 355 ++++++++++++++++++ 6 files changed, 750 insertions(+) create mode 100644 research/conjugate-pair-every-group/PROOF.md create mode 100644 research/conjugate-pair-every-group/README.md create mode 100644 research/conjugate-pair-every-group/SOURCES.json create mode 100644 research/conjugate-pair-every-group/TASK.json create mode 100644 research/conjugate-pair-every-group/VERIFY.json create mode 100644 research/conjugate-pair-every-group/verify.py diff --git a/research/conjugate-pair-every-group/PROOF.md b/research/conjugate-pair-every-group/PROOF.md new file mode 100644 index 0000000000..46d33fc3b9 --- /dev/null +++ b/research/conjugate-pair-every-group/PROOF.md @@ -0,0 +1,151 @@ +# The conjugate-pair target needs four calls in every group + +**Scoped written theorem in a formal group-algebra model; no new κ.** + +## Model + +Let `G` be any group, `F` any field and `x, y ∈ G` with `xy ≠ yx`. Fix a +width `r ≥ 2`. A paid factor is + +```text +D_N(g) = I + ([g] - [e]) N, g ∈ {x, y}, +``` + +where `N ∈ M_r(F)` is a rank-one idempotent, `N = u vᵀ` with `vᵀu = 1`. +Over `F = F2` this is exactly the factor `I + ([g]+[e])N` of +[#4089](https://github.com/CrocSwap/integer-mult-bounds/pull/4089). Roles +beyond the first two are arbitrary dirty spectators that must return to `[e]`. +The target is + +```text +T = diag([xy], [yx], [e], …, [e]) ∈ M_r(F[G]). +``` + +**Theorem.** The minimum number of paid factors whose chronological product +equals `T` is exactly four. + +The direct word `D_{E00}(x) D_{E00}(y) D_{E11}(y) D_{E11}(x)` attains `T` for +every `G`, `F` and `r ≥ 2`. The rest of this file excludes every shorter word. + +## Expansion + +Write `N̄ = I - N`. Then `D_N(g) = [g] N + N̄`. Hence, for labels +`g_1, …, g_k` and idempotents `N_1, …, N_k`, + +```text +D_{N_1}(g_1) ⋯ D_{N_k}(g_k) = Σ_{U ⊆ {1..k}} [g_U] P_U, +P_U = X_1 ⋯ X_k, X_i = N_i if i ∈ U, else N̄_i, +``` + +where `g_U` is the ordered product of the labels in `U`. Since the elements +`[w] E_ij` form an `F`-basis of `M_r(F[G])`, the word realizes `T` if and only +if, for every `w ∈ G`, + +```text +Σ_{U : g_U = w} P_U = T_w, +``` + +with `T_xy = E00`, `T_yx = E11`, `T_e = I - E00 - E11` and `T_w = 0` otherwise. +These are well defined because `xy`, `yx` and `e` are distinct (below). + +**Facts about the pair.** Each item follows by cancellation, and each +violation would make `x` and `y` commute: + +* (F1) `x, y ∉ {e, xy, yx}` and `x ≠ y`; +* (F2) `xy, yx ∉ {e, x, y, x², y²}`; +* (F3) `x²y ≠ xy`, `xy² ≠ xy`, `y²x ≠ yx`, `yx² ≠ yx`, `xyx ∉ {xy, yx}`, + `yxy ∉ {xy, yx}`, and `x³, y³` cannot both equal `xy` and `yx`. + +For example, `xy = x²` gives `y = x`, and `xyx = xy` gives `x = e`. + +## Words of length at most two + +For `k ≤ 1` the only values `g_U` are `e` and one label, so by (F1) and (F2) +`T_xy = E00 ≠ 0` cannot be produced. For `k = 2`, the values are `e`, `g_1`, +`g_2` and `g_1 g_2`. By (F2) only `g_1 g_2` can equal `xy` or `yx`, and it +equals at most one of them. One of the nonzero coefficients `E00`, `E11` is +therefore missing. + +## Words of length three + +From `N² = N` and `N N̄ = N̄ N = 0`: + +```text +N_1 P_U = P_U if 1 ∈ U, else 0; N̄_1 P_U = P_U if 1 ∉ U, else 0; +P_U N_3 = P_U if 3 ∈ U, else 0; P_U N̄_3 = P_U if 3 ∉ U, else 0. +``` + +So each sandwich `A T_w B`, with `A ∈ {N_1, N̄_1}` and `B ∈ {N_3, N̄_3}`, keeps +exactly the subsets `U` with `g_U = w` in one corner. The four corners are +`{∅, {2}}`, `{{1}, {1,2}}`, `{{3}, {2,3}}` and `{{1,3}, {1,2,3}}`. Also +`T_w = (N_1 + N̄_1) T_w (N_3 + N̄_3)`. + +**Lemma 1.** `P_{1} = P_{2} = P_{3} = 0`. + +*Proof.* In corner `(N_1, N̄_3)` the values are `g_1` and `g_1 g_2 ≠ g_1`, so +`N_1 T_{g_1} N̄_3 = P_{1}`; by (F1), `T_{g_1} = 0`. In the same way +`N̄_1 T_{g_3} N_3 = P_{3}` (values `g_3`, `g_2 g_3 ≠ g_3`) and +`N̄_1 T_{g_2} N̄_3 = P_{2}` (values `e`, `g_2 ≠ e`). ∎ + +**Lemma 2.** For `w ∈ {xy, yx}`, `N̄_1 T_w N̄_3 = 0`. + +*Proof.* That corner has values `e` and `g_2`, neither of which is `w` by +(F1) and (F2). ∎ + +**Lemma 3.** `P_{12}` and `P_{23}` are not both nonzero. + +*Proof.* Write `N_i = u_i v_iᵀ`. Then `P_{12} = u_1 (v_1ᵀu_2)(v_2ᵀ N̄_3)`, +`P_{23} = (N̄_1 u_2)(v_2ᵀu_3) v_3ᵀ` and `P_{2} = (N̄_1 u_2)(v_2ᵀ N̄_3)`. If both +are nonzero, then `v_2ᵀ N̄_3 ≠ 0` and `N̄_1 u_2 ≠ 0`. Their outer product +`P_{2}` is then nonzero, contrary to Lemma 1. ∎ + +Now go through the eight label patterns. Write `E_a = e_a e_aᵀ`. + +**`xxx`, `yyy`.** The subsets of size at least two have values `x², x³` +(or `y², y³`). By (F2) and (F3) they cannot supply both `xy` and `yx`. + +**`xyx`, `yxy`.** For `xyx`, `g_{12} = xy`, `g_{23} = yx`, `g_{13} = x²` and +`g_{123} = xyx`. By (F2) and (F3), only `{1,2}` has value `xy` and only `{2,3}` +has value `yx`. Using the corner split and Lemma 2, `E00 = T_xy = P_{12}` and +`E11 = T_yx = P_{23}`. Both are nonzero, contradicting Lemma 3. The pattern +`yxy` is identical with `E00` and `E11` exchanged. + +**`xxy`, `yyx`.** For `xxy`, `g_{12} = x²`, `g_{13} = g_{23} = xy` and +`g_{123} = x²y ≠ xy`. The value `yx` can only come from `{1,2,3}`, so the word +fails unless `x²y = yx`; assume this. Put `a = 0`, `b = 1`; then +`T_xy = E_a` is carried by `{1,3}, {2,3}` and `T_yx = E_b` by `{1,2,3}` alone. +For `yyx` the same holds with `a = 1`, `b = 0` (and `y²x = xy` assumed). + +* `E_b` lies only in corner `(N_1, N_3)`, so `E_b = N_1 E_b N_3 + = u_1 (v_1ᵀ E_b u_3) v_3ᵀ`. Hence `u_1` and `v_3` are nonzero multiples of + `e_b`. +* `N_1 E_a N̄_3 = 0` because `{1,2}` has value `x²` (resp. `y²`). Therefore + `N_1 E_a = N_1 E_a N_3 = P_{13} = u_1 (v_1ᵀ N̄_2 u_3) v_3ᵀ`, a multiple of + `e_b e_bᵀ`. But `N_1 E_a = u_1 (v_1ᵀ e_a) e_aᵀ` is a multiple of `e_b e_aᵀ`. + So `N_1 E_a = 0` and `N̄_1 E_a = E_a`. +* Lemma 2 gives `0 = N̄_1 E_a N̄_3 = E_a N̄_3`, so + `E_a = E_a N_3 = e_a (e_aᵀ u_3) v_3ᵀ`, a multiple of `e_a e_bᵀ`. This is false. + +**`xyy`, `yxx`.** For `xyy`, `g_{12} = g_{13} = xy`, `g_{23} = y²` and +`g_{123} = xy² ≠ xy`. Then `yx` can only come from `{1,2,3}`; assume +`xy² = yx`. With `a = 0`, `b = 1` (for `yxx`: `a = 1`, `b = 0`): + +* As before, `E_b = N_1 E_b N_3`, so `u_1` and `v_3` are multiples of `e_b`. +* `N̄_1 E_a N_3 = 0` because `{2,3}` has value `y²` (resp. `x²`). Therefore + `E_a N_3 = N_1 E_a N_3 = P_{13}`, a multiple of `e_b e_bᵀ`, while + `E_a N_3 = e_a (e_aᵀ u_3) v_3ᵀ` is a multiple of `e_a e_bᵀ`. So + `E_a N_3 = 0` and `E_a N̄_3 = E_a`. +* Lemma 2 gives `0 = N̄_1 E_a N̄_3 = N̄_1 E_a`, so + `E_a = N_1 E_a = u_1 (v_1ᵀ e_a) e_aᵀ`, a multiple of `e_b e_aᵀ`. False. + +Every pattern fails, so no word of length three realizes `T`. ∎ + +## What is used and what is not + +The proof uses only the coefficient equations, `xy ≠ yx` and rank one of each +`N_i`. It uses no generation hypothesis, perfectness, element orders, support +filter or finite census. The noncommuting hypothesis is necessary: for +`y = x⁻¹` the target is `I` and is met by the empty word. + +This is a formal group-algebra theorem. It prices no native address +operation and does not change the selected κ. diff --git a/research/conjugate-pair-every-group/README.md b/research/conjugate-pair-every-group/README.md new file mode 100644 index 0000000000..47bb74c139 --- /dev/null +++ b/research/conjugate-pair-every-group/README.md @@ -0,0 +1,106 @@ +# The conjugate-pair target needs four calls in every group + +**Scoped written theorem in a formal group-algebra model, with finite +corroboration; no new κ.** This contribution was produced by Nick Petalas. +New work is Apache-2.0. + +Let `G` be any group, `F` any field and `x, y ∈ G` with `xy ≠ yx`. In the +rank-one-idempotent register model of +[#4089](https://github.com/CrocSwap/integer-mult-bounds/pull/4089), with paid +factors `I + ([g]-[e])N` for `g ∈ {x, y}`, the target + +```text +T = diag([xy], [yx], [e], …, [e]) ∈ M_r(F[G]) +``` + +has exact paid-call minimum **four** at every width `r ≥ 2`. Extra dirty +spectator roles never lower the bill. + +This answers Open next question 2 of Wentao Li's +[#4089](https://github.com/CrocSwap/integer-mult-bounds/pull/4089) +(`research/a5-conjugate-any-registers`) for every conjugate-pair alphabet at +once. #4089 proves the A5 case over F2 and Wentao Li's +[#4093](https://github.com/CrocSwap/integer-mult-bounds/pull/4093) proves +PSL(2,7). Both use a support filter specific to their group: they check that +only `xyx` and `yxy` can carry both `xy` and `yx`. In a general group, +coincidences such as `x²y = yx` defeat that filter. The new proof handles them. + +## The new step + +[PROOF.md](PROOF.md) has the full argument. Each factor is written as +`[g]N + (I-N)`, so a three-call product is `Σ_U [g_U] P_U` with +`P_U = X_1 X_2 X_3` and `X_i ∈ {N_i, I-N_i}`. Multiplying a coefficient on the +left by `N_1` or `I-N_1` and on the right by `N_3` or `I-N_3` isolates one +corner of subsets. This yields three uniform lemmas: + +1. the single-call products `P_{1}, P_{2}, P_{3}` vanish; +2. the `(I-N_1, I-N_3)` corner of the `xy` and `yx` coefficients vanishes; +3. `P_{12}` and `P_{23}` are not both nonzero. + +The patterns `xyx` and `yxy` then fail by Lemma 3. The patterns `xxy`, `yyx`, +`xyy` and `yxx`, which can survive the support test when `G` has a suitable +coincidence, fail by a rank-one column/row mismatch. Words of length at most +two fail by support alone. The proof uses no generation, perfectness, element +order or field characteristic. + +The noncommuting hypothesis is needed: for `y = x⁻¹` the target is `I`. + +## Evidence + +| Claim | Kind | Evidence | +|---|---|---| +| no word of length ≤ 3, every `G`, `F`, `r` | written proof | [PROOF.md](PROOF.md) | +| four calls suffice | construction | direct word `D_{E00}(x) D_{E00}(y) D_{E11}(y) D_{E11}(x)` | +| finite cross-check | exact finite certificate | `verify.py` | + +`verify.py` checks the expansion and corner identities on 200 seeded rational +triples. It collects the 82 distinct length-4 word-coincidence signatures of +noncommuting pairs in S3, S4, S5, Q8 and the free group. The direct word and +its four one-call deletions are checked on each. Their words of length 1..3 +reduce to 26 subset-class keys. Every key is excluded exhaustively over F2 at +widths 2 and 3 and over F3 at width 2. The finite check corroborates the proof +and does not replace it: it covers neither all groups nor all widths. + +## Reproduce + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/conjugate-pair-every-group/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/conjugate-pair-every-group/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/conjugate-pair-every-group +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/conjugate-pair-every-group --check-source-history +``` + +Any CPython 3.12 may replace that interpreter path. The expected marker is +`PASS_CONJUGATE_PAIR_EVERY_GROUP`; each run takes about five seconds locally. + +## Limits + +This is a theorem in the formal group-algebra model only. It prices no native +address operation, conversion, restoration or recursive caller, and it is not +a multiplication theorem. The selected κ is unchanged. The proof has had no +independent human or proof-kernel review. + +## Open next questions + +1. Which diagonal pair targets `diag([g],[h])` in an arbitrary group admit + cross-register sharing below the sum of their positive word lengths? The + corner-sandwich lemmas may give uniform floors in place of per-group + censuses such as the S3 and Q8 pair censuses. First step: try + `diag([xyx],[yxy])` at length five. Longer words have more corners and + coincidence patterns; no general lemma is supplied here. +2. Is there a priced native nonabelian address alphabet inside an admitted + BIT supplier? This theorem shows that the conjugate-pair target offers no + saving in any group, so such a proposal must find its gain elsewhere. + +The same questions are structured in [TASK.json](TASK.json). + +## Credit + +Wentao Li ([#4089](https://github.com/CrocSwap/integer-mult-bounds/pull/4089), +[#4093](https://github.com/CrocSwap/integer-mult-bounds/pull/4093)) supplied +the model, the any-register A5 and PSL(2,7) theorems and the open question. +Cinna Davis ([#2246](https://github.com/CrocSwap/integer-mult-bounds/pull/2246)) +supplied the original A5 target and its fixed-width result. Their results are +cited, not re-checked. Source pins are in [SOURCES.json](SOURCES.json). diff --git a/research/conjugate-pair-every-group/SOURCES.json b/research/conjugate-pair-every-group/SOURCES.json new file mode 100644 index 0000000000..43a163a151 --- /dev/null +++ b/research/conjugate-pair-every-group/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/a5-conjugate-any-registers/PROOF.md", + "usage": "provenance", + "git_blob": "a72b89bdd2428b78c6424d2d2299bdb1ac2981d3", + "sha256": "921a84d24148d27932aad24a9a5d74bd235de0c1b2f27c2b9bfc5d37fcf51dcf" + }, + { + "path": "research/psl27-conjugate-any-registers/README.md", + "usage": "provenance", + "git_blob": "a26e49a053f9a746cb5b452cbc77c3b8c1e446b0", + "sha256": "8d272a7b19d4c9df2e945713850ba90c45274e99ebc317c20228c31618e8c175" + }, + { + "path": "research/a5-conjugate-any-registers/README.md", + "usage": "provenance", + "git_blob": "92fa82d936248c7e3485e4ea3aecac88f42988f9", + "sha256": "26246a1b0448048f59d2a80e09addcf80950d728f2c768e56d32f145c59fd773" + } + ] +} diff --git a/research/conjugate-pair-every-group/TASK.json b/research/conjugate-pair-every-group/TASK.json new file mode 100644 index 0000000000..963d3138b7 --- /dev/null +++ b/research/conjugate-pair-every-group/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Open next question 2 of PR #4089 (research/a5-conjugate-any-registers): do any-register four-call floors for diag([xy],[yx],[e],...,[e]) hold for other conjugate-pair alphabets? Answered for every group G, every pair x,y in G with xy != yx, every coefficient field and every width r >= 2, in the same formal rank-one-idempotent group-algebra model.", + "scope_change_reason": "The card asks about larger or nonabelian register models. PR #4089 and PR #4093 settle A5 and PSL(2,7) with group-specific support filters; a uniform statement removes the need for further per-group censuses in this model.", + "bottleneck_link": "Side result for the bit-new-register-model family: it closes the cross-register sharing question for this two-role conjugate-pair target in every nonabelian address group, so a native nonabelian BIT proposal cannot save calls on it. It does not price any native operation.", + "budget_minutes": 60, + "stop_rule": "Stop at a written proof plus finite corroboration; do not search larger words or other targets.", + "outcome": "completed", + "evidence": "PROOF.md (written all-group, all-field, all-width proof); verify.py (finite corroboration: 82 signatures, 26 keys, F2 widths 2-3 and F3 width 2, PASS_CONJUGATE_PAIR_EVERY_GROUP).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which diagonal pair targets diag([g],[h]) in an arbitrary group admit cross-register sharing below the sum of their positive word lengths?", + "why_it_matters": "The corner-sandwich method may give uniform floors for longer targets, replacing per-group censuses such as the S3 and Q8 pair censuses.", + "first_step": "Try targets diag([xyx],[yxy]) or diag([xy],[xy]) with the same corner lemmas, starting at length five.", + "blocked_by": "Longer words have more corners and more coincidence patterns; no general lemma is supplied here." + }, + { + "question": "Is there a priced native realization of a nonabelian label alphabet inside an admitted BIT supplier?", + "why_it_matters": "This theorem shows that the conjugate-pair target offers no saving in any group, so a native proposal must find its gain elsewhere.", + "first_step": "Name one runtime address operation and give its full entrance, exit and restoration invoice.", + "blocked_by": "No native nonabelian address contract exists in the selected supplier." + } + ] +} diff --git a/research/conjugate-pair-every-group/VERIFY.json b/research/conjugate-pair-every-group/VERIFY.json new file mode 100644 index 0000000000..1d62ce2cd0 --- /dev/null +++ b/research/conjugate-pair-every-group/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact expansion and corner identities on 200 rational triples; direct four-call word and its four one-call deletions on 82 noncommuting length-4 signatures (S3, S4, S5, Q8, free group); exhaustive exclusion of every word of length 1..3 for all 26 subset-class keys over F2 at widths 2 and 3 and over F3 at width 2; inverse-pair control." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks under optimized execution; the verifier uses explicit exceptions, not assert." + } + ] +} diff --git a/research/conjugate-pair-every-group/verify.py b/research/conjugate-pair-every-group/verify.py new file mode 100644 index 0000000000..75ee7b2e86 --- /dev/null +++ b/research/conjugate-pair-every-group/verify.py @@ -0,0 +1,355 @@ +#!/usr/bin/env python3 +"""Finite corroboration for the every-group conjugate-pair four-call floor. + +The written proof is PROOF.md. This verifier checks, with exact arithmetic: + +1. the factor and product expansions used by the proof, on seeded random + rational and binary instances; +2. the corner-selection identities N1 P_U N3 = P_U or 0 used by Lemma 1; +3. the direct four-call word, for every signature and checked field/width; +4. that no word of length at most three realizes the target, for every + distinct length-three coincidence signature of a noncommuting pair in + S3, S4, S5, Q8 and the free group, over F2 at widths 2 and 3 and over F3 + at width 2; +5. failure controls: the four-call word with one call removed, and the + commuting pair y = x^-1, whose target is the identity. + +Standard library only. Prints PASS_CONJUGATE_PAIR_EVERY_GROUP on success. +""" + +import itertools +import random +import sys +from fractions import Fraction + +MARKER = "PASS_CONJUGATE_PAIR_EVERY_GROUP" +WORDS = tuple(w for k in range(5) for w in itertools.product("xy", repeat=k)) + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +# ---------------------------------------------------------------- matrices + +def mat_mul(a, b, p): + n = len(a) + return tuple( + tuple(sum(a[i][k] * b[k][j] for k in range(n)) % p for j in range(n)) + for i in range(n) + ) + + +def mat_add(a, b, p): + return tuple(tuple((x + y) % p for x, y in zip(r, s)) for r, s in zip(a, b)) + + +def mat_sub(a, b, p): + return tuple(tuple((x - y) % p for x, y in zip(r, s)) for r, s in zip(a, b)) + + +def identity(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def zero(n): + return tuple(tuple(0 for _ in range(n)) for _ in range(n)) + + +def unit(n, i): + return tuple(tuple(int(a == i and b == i) for b in range(n)) for a in range(n)) + + +def rank_one_idempotents(r, p): + """All N = u v^T over F_p with v^T u = 1 (each N listed once).""" + vectors = [v for v in itertools.product(range(p), repeat=r) if any(v)] + found = set() + for u in vectors: + for v in vectors: + if sum(a * b for a, b in zip(u, v)) % p == 1: + found.add(tuple(tuple(a * b % p for b in v) for a in u)) + expected = (p ** r - 1) * p ** (r - 1) // (p - 1) + require(len(found) == expected, "idempotent count at r=%d p=%d" % (r, p)) + return sorted(found) + + +# ---------------------------------------------------------- group signatures + +def compose(a, b): + """Group product a*b for permutations: apply b first.""" + return tuple(a[i] for i in b) + + +def signature(x, y, e, mul): + """Partition of all positive words of length <= 4 by group value.""" + index = {} + labels = [] + for word in WORDS: + g = e + for c in word: + g = mul(g, x if c == "x" else y) + labels.append(index.setdefault(g, len(index))) + return tuple(labels) + + +def permutation_signatures(): + sigs = {} + for n in (3, 4, 5): + elements = list(itertools.permutations(range(n))) + e = tuple(range(n)) + for x in elements: + for y in elements: + if compose(x, y) != compose(y, x): + sigs.setdefault(signature(x, y, e, compose), "S%d" % n) + return sigs + + +def quaternion_signatures(): + # Q8 as pairs (sign, unit) with units 1,i,j,k. + table = { + ("1", u): (1, u) for u in "1ijk" + } + table.update({(u, "1"): (1, u) for u in "1ijk"}) + table.update({ + ("i", "i"): (-1, "1"), ("j", "j"): (-1, "1"), ("k", "k"): (-1, "1"), + ("i", "j"): (1, "k"), ("j", "i"): (-1, "k"), + ("j", "k"): (1, "i"), ("k", "j"): (-1, "i"), + ("k", "i"): (1, "j"), ("i", "k"): (-1, "j"), + }) + + def mul(a, b): + s, u = table[(a[1], b[1])] + return (a[0] * b[0] * s, u) + + elements = [(s, u) for s in (1, -1) for u in "1ijk"] + sigs = {} + for x in elements: + for y in elements: + if mul(x, y) != mul(y, x): + sigs.setdefault(signature(x, y, (1, "1"), mul), "Q8") + return sigs + + +def free_signature(): + return {signature("x", "y", "", lambda a, b: a + b): "free"} + + +def word_value(sig, word): + return sig[WORDS.index(word)] + + +# ------------------------------------------------------------ word products + +def corner_products(ns, p): + """P_U for every subset U (bitmask over call positions).""" + r = len(ns[0]) + comps = [mat_sub(identity(r), n, p) for n in ns] + out = {} + for mask in range(1 << len(ns)): + prod = identity(r) + for i, n in enumerate(ns): + prod = mat_mul(prod, n if mask >> i & 1 else comps[i], p) + out[mask] = prod + return out + + +def coefficients(sig, labels, ns, p): + """Group-algebra coefficients of a chronological product of paid factors.""" + r = len(ns[0]) + acc = {} + for mask, prod in corner_products(ns, p).items(): + word = tuple(labels[i] for i in range(len(labels)) if mask >> i & 1) + g = word_value(sig, word) + acc[g] = mat_add(acc.get(g, zero(r)), prod, p) + return acc + + +def target(sig, r): + rest = tuple(tuple(int(i == j and i >= 2) for j in range(r)) for i in range(r)) + out = {word_value(sig, ()): rest} + for word, role in ((("x", "y"), 0), (("y", "x"), 1)): + g = word_value(sig, word) + out[g] = mat_add(out.get(g, zero(r)), unit(r, role), 2 ** 31) + return out + + +def realizes(sig, labels, ns, p): + r = len(ns[0]) + got = coefficients(sig, labels, ns, p) + want = {g: tuple(tuple(v % p for v in row) for row in m) + for g, m in target(sig, r).items()} + for g in set(got) | set(want): + if got.get(g, zero(r)) != want.get(g, zero(r)): + return False + return True + + +def class_key(sig, labels): + """Canonical map from call subsets to coefficient classes. + + Realizability of the target depends only on this key: which subsets share + a group value, and which classes are e, xy and yx. + """ + special = {word_value(sig, ()): "e", word_value(sig, ("x", "y")): "xy", + word_value(sig, ("y", "x")): "yx"} + names = {} + key = [] + for mask in range(1 << len(labels)): + word = tuple(labels[i] for i in range(len(labels)) if mask >> i & 1) + g = word_value(sig, word) + key.append(special.get(g) or names.setdefault(g, len(names))) + return tuple(key) + + +def key_realizable(key, products, r, p): + want = {"e": tuple(tuple(int(i == j and i >= 2) for j in range(r)) + for i in range(r)), + "xy": unit(r, 0), "yx": unit(r, 1)} + if "xy" not in key or "yx" not in key: + return False + for cls in ("xy", "yx", "e") + tuple(sorted(c for c in set(key) + if isinstance(c, int))): + acc = zero(r) + for mask, c in enumerate(key): + if c == cls: + acc = mat_add(acc, products[mask], p) + if acc != want.get(cls, zero(r)): + return False + return True + + +def short_word_keys(sigs): + keys = set() + for sig in sigs: + for k in (1, 2, 3): + for labels in itertools.product("xy", repeat=k): + keys.add(class_key(sig, labels)) + return keys + + +def no_short_word(keys, idems, p): + """Exhaustive search over every word of length 1..3 for every key.""" + r = len(idems[0]) + by_len = {} + for key in keys: + by_len.setdefault(len(key), []).append(key) + for size, group in by_len.items(): + k = size.bit_length() - 1 + for ns in itertools.product(idems, repeat=k): + products = corner_products(ns, p) + for key in group: + if key_realizable(key, products, r, p): + return False + return True + + +# ----------------------------------------------------------------- checks + +def check_expansion_identities(): + """D_N(g) = [g]N + (I-N) and the corner selection identities.""" + rng = random.Random(20261028) + for _ in range(200): + r = rng.choice((2, 3, 4)) + ns = [] + for _ in range(3): + while True: + u = [Fraction(rng.randint(-3, 3)) for _ in range(r)] + v = [Fraction(rng.randint(-3, 3)) for _ in range(r)] + s = sum(a * b for a, b in zip(u, v)) + if s != 0: + break + ns.append(tuple(tuple(a * b / s for b in v) for a in u)) + eye = tuple(tuple(Fraction(int(i == j)) for j in range(r)) for i in range(r)) + + def mm(a, b): + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(r)) + for j in range(r)) for i in range(r)) + + def ms(a, b): + return tuple(tuple(x - y for x, y in zip(c, d)) for c, d in zip(a, b)) + + for n in ns: + require(mm(n, n) == n, "rational idempotent") + require(mm(n, ms(eye, n)) == mm(ms(eye, n), n) == ms(eye, eye), + "complementary idempotents annihilate") + comps = [ms(eye, n) for n in ns] + zero_r = ms(eye, eye) + for mask in range(8): + prod = eye + for i in range(3): + prod = mm(prod, ns[i] if mask >> i & 1 else comps[i]) + left = mm(ns[0], prod) + right = mm(prod, ns[2]) + require(left == (prod if mask & 1 else zero_r), + "left corner selection") + require(right == (prod if mask & 4 else zero_r), + "right corner selection") + bar_left = mm(comps[0], prod) + require(bar_left == (prod if not mask & 1 else zero_r), + "left complement selection") + # Sum over subsets of P_U equals I: the product of (N_i + (I - N_i)). + total = tuple(tuple(Fraction(0) for _ in range(r)) for _ in range(r)) + for mask in range(8): + prod = eye + for i in range(3): + prod = mm(prod, ns[i] if mask >> i & 1 else comps[i]) + total = tuple(tuple(a + b for a, b in zip(c, d)) + for c, d in zip(total, prod)) + require(total == eye, "subset expansion sums to identity") + return 200 + + +def check_direct_word(sig, r, p): + labels = ("x", "y", "y", "x") + ns = (unit(r, 0), unit(r, 0), unit(r, 1), unit(r, 1)) + require(realizes(sig, labels, ns, p), "direct four-call word") + for drop in range(4): + sub_l = labels[:drop] + labels[drop + 1:] + sub_n = ns[:drop] + ns[drop + 1:] + require(not realizes(sig, sub_l, sub_n, p), "mutated direct word rejected") + + +def check_commuting_control(): + """The noncommuting hypothesis is needed: y = x^-1 gives target I.""" + e = (0, 1, 2) + x = (1, 2, 0) + y = (2, 0, 1) + require(compose(x, y) == e == compose(y, x), "inverse control pair") + sig = signature(x, y, e, compose) + r = 2 + got = target(sig, r) + require(got == {word_value(sig, ()): identity(r)}, + "inverse pair target is the identity, met by the empty word") + return r + + +def main(): + checked = check_expansion_identities() + print("expansion and corner identities: %d random rational triples" % checked) + sigs = {} + sigs.update(permutation_signatures()) + sigs.update(quaternion_signatures()) + sigs.update(free_signature()) + print("distinct noncommuting length-4 signatures: %d" % len(sigs)) + keys = short_word_keys(sigs) + print("distinct subset-class keys for words of length 1..3: %d" % len(keys)) + for sig in sigs: + require(word_value(sig, ()) not in + (word_value(sig, ("x", "y")), word_value(sig, ("y", "x"))), + "the empty word cannot realize the target") + for (r, p) in ((2, 2), (3, 2), (2, 3)): + idems = rank_one_idempotents(r, p) + for sig in sigs: + check_direct_word(sig, r, p) + require(no_short_word(keys, idems, p), + "a word of length <= 3 realizes the target (r=%d p=%d)" % (r, p)) + print("F%d width %d: %d idempotents, no word of length <= 3 for any " + "key; direct word passes" % (p, r, len(idems))) + control = check_commuting_control() + print("control y = x^-1: target is I at width %d, met by zero calls" % control) + print(MARKER) + + +if __name__ == "__main__": + main() From e743e8037f4fcce60f8eee05b72c444e2ed32fe6 Mon Sep 17 00:00:00 2001 From: josie Date: Tue, 27 Oct 2026 23:12:01 -0400 Subject: [PATCH 02/10] =?UTF-8?q?Audit=20#6038=20and=20prove=20a=20group-f?= =?UTF-8?q?ree=20four-call=20floor=20for=20diagonal=20pair=20targets=20(no?= =?UTF-8?q?=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Independent line-by-line audit of PR6038's conjugate-pair proof (no error), Theorem S: any label set avoiding the two target entries needs four calls, with a two-case proof, and a stdlib group-free finite certificate. Co-Authored-By: Claude Opus 5.5 --- .../conjugate-pair-group-free-audit/PROOF.md | 122 ++++++ .../conjugate-pair-group-free-audit/README.md | 135 +++++++ .../SOURCES.json | 24 ++ .../conjugate-pair-group-free-audit/TASK.json | 101 +++++ .../VERIFY.json | 34 ++ .../conjugate-pair-group-free-audit/verify.py | 356 ++++++++++++++++++ 6 files changed, 772 insertions(+) create mode 100644 research/conjugate-pair-group-free-audit/PROOF.md create mode 100644 research/conjugate-pair-group-free-audit/README.md create mode 100644 research/conjugate-pair-group-free-audit/SOURCES.json create mode 100644 research/conjugate-pair-group-free-audit/TASK.json create mode 100644 research/conjugate-pair-group-free-audit/VERIFY.json create mode 100644 research/conjugate-pair-group-free-audit/verify.py diff --git a/research/conjugate-pair-group-free-audit/PROOF.md b/research/conjugate-pair-group-free-audit/PROOF.md new file mode 100644 index 0000000000..a92cbe6f25 --- /dev/null +++ b/research/conjugate-pair-group-free-audit/PROOF.md @@ -0,0 +1,122 @@ +# A four-call floor that uses only the single labels + +**Scoped written theorem in the formal group-algebra model of #4089 / #6038; no +new κ.** It strengthens the length-three exclusion of +[PR #6038](https://github.com/CrocSwap/integer-mult-bounds/pull/6038) +(`research/conjugate-pair-every-group`, head +`0cee0e104b68ce6f06bf84af03f46ac30680e64c`) and replaces its eight-pattern case +analysis with two cases. + +## Statement + +Let `G` be a group, `F` a field and `r ≥ 2`. Let `a, b ∈ G` be distinct and +both different from `e`, and let + +```text +T = diag([a], [b], [e], …, [e]) ∈ M_r(F[G]). +``` + +A paid call is `D_N(g) = [g] N + N̄` with `N̄ = I - N`, where `N` is a rank-one +idempotent of `M_r(F)` and `g ∈ L` for a label set `L ⊆ G`. + +**Theorem S.** If no label equals `e`, `a` or `b`, then no product of at most +three paid calls equals `T`. This holds for every label set and whatever +coincidences hold among products of labels. + +A call with label `e` is the identity matrix, so `e ∉ L` costs nothing: drop +such calls. The only hypothesis that matters is that no single label equals `a` +or `b`. + +**Corollary (PR6038's length-three step).** Take `L = {x, y}` with `xy ≠ yx`, +`a = xy` and `b = yx`. Then `a ≠ b` and `a, b ≠ e`, and `x, y ∉ {e, xy, yx}` +by cancellation, which is #6038's (F1). Theorem S excludes every word of length +at most three. #6038's facts (F2) and (F3) and its pattern-by-pattern analysis +are not needed. With #6038's four-call direct word, the minimum is four. + +## Proof + +Expand `D_{N_1}(g_1) ⋯ D_{N_k}(g_k) = Σ_U [g_U] P_U` as in #6038, where +`P_U = X_1 ⋯ X_k`, `X_i = N_i` if `i ∈ U` and `N̄_i` otherwise. Group the +subsets by value into three classes: `𝔸 = {U : g_U = a}`, `𝔹 = {U : g_U = b}` +and `𝔼 = {U : g_U = e}`. Since `[w] E_ij` is a basis, the word realizes `T` +only if + +```text +Σ_{U∈𝔸} P_U = E_00, Σ_{U∈𝔹} P_U = E_11, Σ_{U∈𝔼} P_U = T_e := I - E_00 - E_11. +``` + +The proof uses only these three equations. The equations at other group +elements are never used. By hypothesis, `∅ ∈ 𝔼`, and no singleton lies in +`𝔸`, `𝔹` or `𝔼`. + +**k ≤ 2.** `𝔸` and `𝔹` are disjoint and nonempty, because `E_00, E_11 ≠ 0`. +They lie in the subsets of size at least two, and there is at most one such +subset. Contradiction. + +**k = 3.** Write `N_i = u_i v_iᵀ` with `v_iᵀu_i = 1`. Then `𝔸, 𝔹 ⊆ S := +{12, 13, 23, 123}`, and + +```text +P_12 = u_1 (v_1ᵀu_2)(v_2ᵀN̄_3), P_13 = u_1 (v_1ᵀN̄_2u_3) v_3ᵀ, +P_23 = (N̄_1u_2)(v_2ᵀu_3) v_3ᵀ, P_123 = u_1 (v_1ᵀu_2)(v_2ᵀu_3) v_3ᵀ, +P_2 = (N̄_1u_2)(v_2ᵀN̄_3), P_∅ + P_2 = N̄_1 N̄_3. +``` + +Corner rules (as in #6038): `N_1 P_U = P_U` if `1 ∈ U` and `0` otherwise; +`N̄_1 P_U` is the complement. The same holds on the right with `N_3` and +position 3. + +*Step 1: `23 ∈ 𝔸 ∪ 𝔹` and `12 ∈ 𝔸 ∪ 𝔹`.* Every `P_U` with `U ∈ S \ {23}` +has column space in `span(u_1)`. If neither `𝔸` nor `𝔹` contained `23`, then +`E_00` and `E_11` would both have column space in `span(u_1)`. Then `u_1` would +be parallel to both `e_0` and `e_1`, which is impossible. The same argument +with row spaces and `v_3ᵀ` gives `12`. So the cases are (up to the symmetry +below): (1) `12, 23 ∈ 𝔸`, or (2) `23 ∈ 𝔸` and `12 ∈ 𝔹`. + +*Symmetry.* Exchanging `a ↔ b` together with the coordinates `0 ↔ 1` +(conjugation by a permutation matrix maps rank-one idempotents to rank-one +idempotents) exchanges `𝔸` and `𝔹`. The hypotheses are symmetric, so the +other two placements reduce to these. + +*Case 1: `12, 23 ∈ 𝔸`.* Then `𝔹 ⊆ {13, 123}`, so `E_11` is a multiple of +`u_1 v_3ᵀ`, and `u_1 ∥ e_1`, `v_3 ∥ e_1`. Within `S`, only `12` omits position +3, so `E_00 N̄_3 = P_12`. The left side has column space in `span(e_0)`. The +right side has column space in `span(u_1) = span(e_1)`. So `P_12 = 0`. +Likewise only `23` omits position 1, so `N̄_1 E_00 = P_23`. The left side has +row space `span(e_0ᵀ)` and the right side has row space `span(v_3ᵀ) = +span(e_1ᵀ)`, so `P_23 = 0`. Then `E_00 = N_1 E_00 N_3`, a multiple of +`u_1 v_3ᵀ ∥ e_1 e_1ᵀ`. Contradiction. + +*Case 2: `23 ∈ 𝔸`, `12 ∈ 𝔹`.* `𝔸` omits `12`, so every member of `𝔸` +contains position 3. Hence `E_00 N̄_3 = 0`, and `E_00` has row space in +`span(v_3ᵀ)`, so `v_3 ∥ e_0`. `𝔹` omits `23`, so every member contains +position 1. Hence `N̄_1 E_11 = 0` and `u_1 ∥ e_1`. + +* `P_12 ≠ 0`: within `𝔹` only `12` omits position 3, so `E_11 N̄_3 = P_12`. + If this were zero, `E_11 = E_11 N_3` would be a multiple of + `e_1 v_3ᵀ ∥ e_1 e_0ᵀ`, which is false. +* `P_23 ≠ 0`: within `𝔸` only `23` omits position 1, so `N̄_1 E_00 = P_23`. + If this were zero, `E_00 = N_1 E_00` would be a multiple of + `u_1 e_0ᵀ ∥ e_1 e_0ᵀ`, which is false. +* Hence `v_2ᵀN̄_3 ≠ 0` and `N̄_1 u_2 ≠ 0`, so `P_2 ≠ 0`. +* The corner `(N̄_1, N̄_3)` keeps `∅` and `{2}`. Only `∅` lies in `𝔼`, so + `P_∅ = N̄_1 T_e N̄_3 = N̄_1 N̄_3 - N̄_1 E_00 N̄_3 - N̄_1 E_11 N̄_3 = N̄_1 N̄_3`, + using `E_00 N̄_3 = 0` and `N̄_1 E_11 = 0`. With `P_∅ + P_2 = N̄_1 N̄_3`, + this gives `P_2 = 0`. Contradiction. ∎ + +## What is used + +The proof uses three things: the three class equations, `∅ ∈ 𝔼`, and the +fact that no singleton is in a target class. It uses no element of `L`, no +relation among labels, no field characteristic and no width beyond `r ≥ 2`. +It does not use the equations at the other group elements; dropping them only +enlarges the set of systems excluded. The verifier's `singleton` tier searches +exactly this relaxed system over small prime fields and widths and finds no +solution. Its controls show the search is not vacuous: it finds four-call +solutions, and a single label allowed to equal `xy` reopens length three. + +## Scope + +This is a statement in the formal group-algebra model. It prices no native +address operation, conversion, restoration or caller and changes no κ. No +proof-kernel check and no independent human review is claimed. diff --git a/research/conjugate-pair-group-free-audit/README.md b/research/conjugate-pair-group-free-audit/README.md new file mode 100644 index 0000000000..c1e9d01910 --- /dev/null +++ b/research/conjugate-pair-group-free-audit/README.md @@ -0,0 +1,135 @@ +# Independent audit of #6038: a group-free four-call floor + +**Independent proof audit, a stronger written theorem and a group-free finite +certificate. No new κ.** This package is by Josie Elliston, with substantial +Claude (Anthropic) assistance. New work is Apache-2.0. + +Subject: Nick Petalas's [PR #6038](https://github.com/CrocSwap/integer-mult-bounds/pull/6038) +(`research/conjugate-pair-every-group`) at exact head +`0cee0e104b68ce6f06bf84af03f46ac30680e64c`. In the rank-one-idempotent +register model of Wentao Li's +[#4089](https://github.com/CrocSwap/integer-mult-bounds/pull/4089), #6038 claims +that `diag([xy],[yx],[e],…,[e])` needs exactly four paid calls, for every group, +field and width `r ≥ 2`. The package does not read #6038's files and imports no +code from #6038 or #4089. + +## Results + +**1. Audit of #6038's PROOF.md: no error found.** I checked each step against +the model. The model and factor form match #4089's `research/a5-conjugate-any-registers/PROOF.md` +over `F2`. I checked the facts (F1)-(F3) by cancellation, the corner +identities, Lemmas 1-3 and all eight length-three patterns. For `xxy`, `yyx`, +`xyy` and `yxx` I also checked that no other subset can take the value `xy` or +`yx`. Two remarks, neither affecting correctness: + +* The last clause of (F3), "`x³, y³` cannot both equal `xy` and `yx`", is + weaker than the truth. `x³` equals neither, since `x³ = xy` or `x³ = yx` + gives `y = x²`. The weaker clause is enough for the `xxx` pattern. +* In the `xyx` case the "corner split and Lemma 2" are unnecessary. + `T_xy = P_12` follows directly, because `{1,2}` is the only subset with value + `xy`. + +An OpenAI Codex read-only adversarial review of the same PROOF.md and of this +verifier also reported no error. It is a second machine check, not human +review. + +**2. A stronger theorem with a shorter proof ([PROOF.md](PROOF.md)).** Fix +distinct `a, b ≠ e` and the target `diag([a],[b],[e],…,[e])`. If no label +equals `a` or `b`, no product of at most three paid calls reaches the target. +This holds for every label set, every coincidence among products of labels, +every field and every `r ≥ 2`. The proof uses only the coefficient equations at +`a`, `b` and `e`. It has two cases and needs neither #6038's facts (F2)/(F3) nor +its eight-pattern analysis. #6038's length-three step is the special case +`L = {x, y}`, `a = xy`, `b = yx`. + +**3. A group-free finite certificate ([verify.py](verify.py)).** #6038's +finite check covers 26 coincidence keys collected from S3, S4, S5, Q8 and the +free group. This check instead lets each subset word `g_U` of a length 0-3 word +over `{x, y}` take any class in `{e, xy, yx, other}` that the single equation +`g_U = class` allows when `xy ≠ yx`. Each of the 90 equations is decided by an +exact rule: + +* *allowed*: an explicit noncommuting witness pair in S3, S4 or S5 (38 + equations); +* *forbidden*: after cyclic free reduction of `g_U · class⁻¹`, one generator + occurs exactly once, or the relator is a cyclic conjugate of `[x,y]^{±1}`. + Either way `xy = yx` would follow (52 equations). + +The verifier fails if any equation is undecided. The search drops joint +consistency and the zero equations at "other" elements. Its feasible set +therefore contains the labeling of every actual group. It searches every tuple +of rank-one idempotents in two tiers. The *full* tier uses the table above. +The *singleton* tier constrains only the single letters, exactly as in +Theorem S. + +| width r | field | tuples at k = 3 | full tier | singleton tier | +|---:|---:|---:|---|---| +| 2 | F2 | 216 | no solution | no solution | +| 2 | F3 | 1,728 | no solution | no solution | +| 2 | F5 | 27,000 | no solution | no solution | +| 3 | F2 | 21,952 | no solution | no solution | +| 2 | F7 | 175,616 | no solution | no solution (local run, 87 s) | + +The first four rows are registered; the F7 row is a local run of the same verifier +(`--cases 2:7`). Lengths 0, 1 and 2 are also excluded in every row. + +Controls, all registered: + +* the direct word `D_{E00}(x) D_{E00}(y) D_{E11}(y) D_{E11}(x)` satisfies the + relaxation, and the search finds a length-four solution by itself; +* with every nonempty subset allowed in any class (pure linear algebra), a + length-two word fits; +* wrongly allowing one single label to equal `xy` (`y = xy`) reopens length + three (pattern `yxy`). + +The search confirms that the single-label facts are the essential ones. In a +local exploratory run at `r = 2` over `F2` (not registered), I flipped each of +the 32 forbidden equations with words of length at most three, one at a time. +Only the four that put `x` or `y` in the `xy` or `yx` class reopened a short +word. + +## What this does not cover + +* The finite tiers cover only prime fields at the sizes in the table. Prime-power + fields such as F4 and widths `r ≥ 4` rely on the written proofs. +* Neither proof addresses native address operations, conversion, restoration, + a caller or any BIT supplier. The selected κ (#6030) is unchanged. +* No independent human or proof-kernel review is claimed. + +## Reproduce + +From the repository root, standard-library CPython 3.12: + +```sh +python3.12 -B -W error research/conjugate-pair-group-free-audit/verify.py +python3.12 -O -B -W error research/conjugate-pair-group-free-audit/verify.py +python3.12 -B research/conjugate-pair-group-free-audit/verify.py --cases 2:7 # optional, about 90 s +python3.12 -B scripts/research_package.py --package research/conjugate-pair-group-free-audit +``` + +Expected marker: `PASS_CONJUGATE_PAIR_GROUP_FREE_AUDIT`, in about 30 s per mode. + +## Open next questions + +1. **Longer diagonal pair targets (#6038 open question 1).** Theorem S is a + uniform floor of 4 for any pair target whose entries are not labels. Does a + corner argument give `≥ 6` for `diag([g],[h])` when neither `g` nor `h` is a + product of at most two labels, for example `diag([xyx],[yxy])`? *Why:* it + would replace per-group pair censuses with one argument. *First step:* + extend the singleton tier so that every subset of size at most two is also + barred from the target classes, then search lengths 4 and 5 at `r = 2` over + `F2`. *Blocker:* the per-class mask enumeration here costs + `2^(allowed subsets)`, which is too slow at length five. It needs a + linear-algebra search over the subset sums instead. +2. **Formalization.** Theorem S involves only rank-one matrices over a field + and suits a proof assistant. No Lean build was attempted. + +## Credit + +Nick Petalas (#6038) supplied the all-group theorem, the corner-sandwich +method, the expansion and the direct word that this package audits and builds +on. Wentao Li (#4089, #4093) supplied the model and the A5 and PSL(2,7) +results; Cinna Davis (#2246) supplied the original A5 target. Their cited +statements were not re-audited beyond what is described above. Theorem S, its +two-case proof, the group-free relaxation and the verifier are new here. +Source pins are in [SOURCES.json](SOURCES.json). diff --git a/research/conjugate-pair-group-free-audit/SOURCES.json b/research/conjugate-pair-group-free-audit/SOURCES.json new file mode 100644 index 0000000000..508b3dd13b --- /dev/null +++ b/research/conjugate-pair-group-free-audit/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/a5-conjugate-any-registers/PROOF.md", + "usage": "provenance", + "git_blob": "a72b89bdd2428b78c6424d2d2299bdb1ac2981d3", + "sha256": "921a84d24148d27932aad24a9a5d74bd235de0c1b2f27c2b9bfc5d37fcf51dcf" + } + ] +} diff --git a/research/conjugate-pair-group-free-audit/TASK.json b/research/conjugate-pair-group-free-audit/TASK.json new file mode 100644 index 0000000000..3df775803b --- /dev/null +++ b/research/conjugate-pair-group-free-audit/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Independent audit of Nick Petalas's PR #6038 (research/conjugate-pair-every-group, head 0cee0e104b68ce6f06bf84af03f46ac30680e64c): line-by-line check of its written all-group four-call theorem; a stronger written theorem (Theorem S: any label set avoiding the two target entries, any coincidences, any field, r >= 2) with a two-case proof; and a group-free finite certificate over small prime fields and widths.", + "scope_change_reason": "The chooser drew independent-verification. independent-moment on the selected #6030 word already has two audits (maintainer review and #6043), and no open PR claims a higher kappa. #6038 is a fresh unreviewed all-group theorem that answers #4089's open question 2. Its finite check depends on coincidence keys from five named groups. An independent proof check plus a check free of group-specific inputs is the missing implication for that claim. formal-interface-lemma is the closest card: this binds a theorem to a certificate, without a proof-assistant build.", + "bottleneck_link": "Side result for the BIT register-model line. It confirms that the conjugate-pair alphabet offers no call saving in any group. Theorem S extends this to every label set that avoids the target entries, so a nonabelian-alphabet BIT proposal must find its gain elsewhere. No kappa effect.", + "budget_minutes": 60, + "stop_rule": "Stop at the first error in #6038's proof or the first relaxed solution at length <= 3; otherwise stop after the written strengthening and the registered finite tiers.", + "outcome": "completed", + "evidence": "PROOF.md (Theorem S, two-case proof); README audit notes on #6038 PROOF.md; verify.py, a stdlib group-free relaxation over r,q = (2,2),(2,3),(2,5),(3,2) with full and singleton tiers and positive/negative controls; local run at (2,7).", + "author": "Josie Elliston", + "ai_assistance": "Claude (Anthropic) assisted with the audit, the proof, the code and the writing. An OpenAI Codex read-only adversarial review of #6038's PROOF.md and of verify.py reported no error.", + "open_questions": [ + { + "question": "Does a corner argument give a uniform floor of 6 calls for diag([g],[h]) when neither entry is a product of at most two labels, e.g. diag([xyx],[yxy])? (#6038 open question 1)", + "why_it_matters": "It would replace per-group pair censuses with one uniform argument.", + "first_step": "Bar subsets of size <= 2 from the target classes in the singleton tier; search lengths 4-5 at r = 2 over F2.", + "blocked_by": "The per-class mask enumeration is 2^(allowed subsets); length five needs a linear-algebra search over subset sums." + }, + { + "question": "Formalize Theorem S in a proof assistant.", + "why_it_matters": "It is a short statement about rank-one matrices over a field and would give a kernel-checked floor.", + "first_step": "State the three class equations and the corner rules for k = 3 over an arbitrary field.", + "blocked_by": "No Lean build was attempted; it needs a separate proof-assistant budget." + } + ] +} diff --git a/research/conjugate-pair-group-free-audit/VERIFY.json b/research/conjugate-pair-group-free-audit/VERIFY.json new file mode 100644 index 0000000000..b66ecee969 --- /dev/null +++ b/research/conjugate-pair-group-free-audit/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a5-conjugate-any-registers/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Group-free relaxation excludes every word of length 0..3 at widths/fields (r,q) = (2,2),(2,3),(2,5),(3,2) under both the full single-equation consistency table and the singleton-only table; every one of 90 equations decided by an S3/S4/S5 witness or a sound cancellation rule; positive controls: direct four-call word and an independent length-4 hit; failure controls: unrestricted linear algebra fits at length 2, one wrong singleton bit reopens length 3." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same as the normal run under -O (no assert-dependent checks are skipped: the verifier raises SystemExit on failure paths that matter and asserts only on controls)." + } + ] +} diff --git a/research/conjugate-pair-group-free-audit/verify.py b/research/conjugate-pair-group-free-audit/verify.py new file mode 100644 index 0000000000..fa9bc7931d --- /dev/null +++ b/research/conjugate-pair-group-free-audit/verify.py @@ -0,0 +1,356 @@ +#!/usr/bin/env python3 +"""Group-free independent check of the PR6038 conjugate-pair four-call floor. + +Standard library only. Imports nothing from PR6038 or #4089. + +Model (PR6038 / #4089): paid factor D_N(g) = [g] N + (I - N), g in {x, y}, +N a rank-one idempotent of M_r(F_q); target T = diag([xy], [yx], [e], ..., [e]). +A word D_{N_1}(g_1) ... D_{N_k}(g_k) expands as sum_U [g_U] P_U. + +Relaxation (the point of this check): instead of fixing a group, each subset +word g_U may be put in any class among {e, xy, yx, other} that is *individually* +consistent with xy != yx. Joint consistency of several coincidences, and the +requirement that every "other" group element gets coefficient zero separately, +are dropped. Every actual group G and pair x, y with xy != yx therefore gives +one of the allowed labelings, so infeasibility of the relaxation for a field +and width excludes the word for *every* group at once. + +Consistency of a single equation g_U = c is decided by exact rules only: + * consistent -> an explicit noncommuting witness pair in S3, S4 or S5; + * inconsistent -> after cyclic free reduction of g_U c^-1, either one + generator occurs exactly once (so it lies in the cyclic + group of the other and the pair commutes), or the relator + is a cyclic conjugate of the commutator [x, y]^(+-1). +Any equation decided by neither rule makes the verifier fail. + +Two tiers are searched. "full" uses the table above. "singleton" keeps only +the facts about single letters (x, y not in {e, xy, yx}) and lets every subset +of size >= 2 join any class; this is exactly the relaxed system of Theorem S +in PROOF.md. +""" + +from __future__ import annotations + +import argparse +import itertools +import sys +import time + +MARKER = "PASS_CONJUGATE_PAIR_GROUP_FREE_AUDIT" + +def require(cond, msg): + """Explicit check that also runs under python -O.""" + if not cond: + raise SystemExit(f"FAIL {msg}") + + +# ---------------------------------------------------------------- free words +INV = {"x": "X", "X": "x", "y": "Y", "Y": "y"} + + +def free_reduce(word: str) -> str: + out: list[str] = [] + for ch in word: + if out and out[-1] == INV[ch]: + out.pop() + else: + out.append(ch) + return "".join(out) + + +def cyclic_reduce(word: str) -> str: + w = free_reduce(word) + while len(w) >= 2 and w[0] == INV[w[-1]]: + w = w[1:-1] + return w + + +def inverse(word: str) -> str: + return "".join(INV[ch] for ch in reversed(word)) + + +def forces_commutation(relator: str) -> bool: + """Sound sufficient test: some generator occurs exactly once cyclically.""" + w = cyclic_reduce(relator) + if w == "": + return False # trivial relation, no information + commutators = {c[i:] + c[:i] for c in ("xyXY", "yxYX") for i in range(4)} + if w in commutators: + return True # the relation is xy = yx itself + for gen in "xy": + if sum(ch in (gen, INV[gen]) for ch in w) == 1: + return True + return False + + +# ------------------------------------------------------- permutation witnesses +def perm_mul(p, q): + """Composition (p*q)[i] = p[q[i]]. Any fixed associative convention gives a + group, and only equalities of word values are tested.""" + return tuple(p[i] for i in q) + + +def perm_inv(p): + inv = [0] * len(p) + for i, pi in enumerate(p): + inv[pi] = i + return tuple(inv) + + +def evaluate(word: str, x, y): + ident = tuple(range(len(x))) + table = {"x": x, "y": y, "X": perm_inv(x), "Y": perm_inv(y)} + acc = ident + for ch in word: + acc = perm_mul(acc, table[ch]) + return acc + + +def witness_pairs(): + for n in (3, 4, 5): + elems = list(itertools.permutations(range(n))) + for x in elems: + for y in elems: + if perm_mul(x, y) != perm_mul(y, x): + yield n, x, y + + +TARGET_WORDS = {"E": "", "XY": "xy", "YX": "yx"} + + +def classify_equations(words: list[str]): + """Return {(word, cls): bool consistent} and evidence counts.""" + pending = {(w, c) for w in words for c in TARGET_WORDS} + result: dict[tuple[str, str], bool] = {} + evidence = {"witness": 0, "forced_commutation": 0} + for (w, c) in list(pending): + if forces_commutation(w + inverse(TARGET_WORDS[c])): + result[(w, c)] = False + evidence["forced_commutation"] += 1 + pending.discard((w, c)) + for _n, x, y in witness_pairs(): + if not pending: + break + for (w, c) in list(pending): + if evaluate(w, x, y) == evaluate(TARGET_WORDS[c], x, y): + result[(w, c)] = True + evidence["witness"] += 1 + pending.discard((w, c)) + if pending: + raise SystemExit(f"FAIL undecided equations: {sorted(pending)}") + return result, evidence + + +# ------------------------------------------------------------- field algebra +def mat_mul(a, b, q): + r = len(a) + return tuple( + tuple(sum(a[i][t] * b[t][j] for t in range(r)) % q for j in range(r)) + for i in range(r) + ) + + +def mat_add(a, b, q): + return tuple(tuple((u + v) % q for u, v in zip(ra, rb)) for ra, rb in zip(a, b)) + + +def identity(r): + return tuple(tuple(1 if i == j else 0 for j in range(r)) for i in range(r)) + + +def zero(r): + return tuple(tuple(0 for _ in range(r)) for _ in range(r)) + + +def unit(r, a): + return tuple(tuple(1 if i == j == a else 0 for j in range(r)) for i in range(r)) + + +def rank_one_idempotents(r, q): + out = set() + vecs = [v for v in itertools.product(range(q), repeat=r) if any(v)] + for u in vecs: + for v in vecs: + if sum(a * b for a, b in zip(u, v)) % q == 1: + out.add(tuple(tuple(ui * vj % q for vj in v) for ui in u)) + return sorted(out) + + +def subset_products(ns, q, r): + """P_U for every U (bitmask over positions 0..k-1), chronological order.""" + ident = identity(r) + bars = [tuple(tuple((ident[i][j] - n[i][j]) % q for j in range(r)) for i in range(r)) for n in ns] + k = len(ns) + level = {0: ident} + for pos in range(k): + nxt = {} + for mask, m in level.items(): + nxt[mask | (1 << pos)] = mat_mul(m, ns[pos], q) + nxt[mask] = mat_mul(m, bars[pos], q) + level = nxt + return level + + +# ------------------------------------------------------------ the relaxation +def label_word(pattern: str, mask: int) -> str: + return "".join(ch for i, ch in enumerate(pattern) if mask >> i & 1) + + +def allowed_labels(pattern: str, consistent): + k = len(pattern) + allowed = {} + for mask in range(1 << k): + w = label_word(pattern, mask) + if mask == 0: + allowed[mask] = {"E"} # the empty subset has value e + else: + allowed[mask] = {c for c in TARGET_WORDS if consistent[(w, c)]} + return allowed + + +def sub_masks(items): + for n in range(len(items) + 1): + for combo in itertools.combinations(items, n): + yield combo + + +def relaxed_feasible(prods, allowed, r, q, everything_allowed=False): + t_xy = unit(r, 0) + t_yx = unit(r, 1) + t_e = identity(r) + t_e = tuple(tuple((t_e[i][j] - t_xy[i][j] - t_yx[i][j]) % q for j in range(r)) for i in range(r)) + masks = list(prods) + z = zero(r) + + def candidates(cls, target, forced=()): + pool = [m for m in masks if m not in forced and (everything_allowed and m != 0 or cls in allowed[m])] + if cls == "E": + pool = [m for m in pool if m != 0] + hits = [] + for combo in sub_masks(pool): + s = z + for m in forced: + s = mat_add(s, prods[m], q) + for m in combo: + s = mat_add(s, prods[m], q) + if s == target: + hits.append(frozenset(combo) | frozenset(forced)) + return hits + + xy_sets = candidates("XY", t_xy) + if not xy_sets: + return None + yx_sets = candidates("YX", t_yx) + if not yx_sets: + return None + e_sets = candidates("E", t_e, forced=(0,)) + for a in xy_sets: + for b in yx_sets: + if a & b: + continue + for c in e_sets: + if not (c & a) and not (c & b): + return (a, b, c) + return None + + +def run_case(k, r, q, consistent, everything_allowed=False, stop_at_first=True): + idem = rank_one_idempotents(r, q) + patterns = ["".join(p) for p in itertools.product("xy", repeat=k)] + allowed = {p: allowed_labels(p, consistent) for p in patterns} + found = [] + tuples = 0 + for ns in itertools.product(idem, repeat=k): + tuples += 1 + prods = subset_products(ns, q, r) + for p in patterns: + hit = relaxed_feasible(prods, allowed[p], r, q, everything_allowed) + if hit is not None: + found.append((p, ns, hit)) + if stop_at_first: + return len(idem), tuples, found + return len(idem), tuples, found + + +def main(argv=None): + ap = argparse.ArgumentParser() + ap.add_argument("--cases", default="2:2,2:3,2:5,3:2", + help="comma list r:q of width:prime for the length<=3 exclusion") + args = ap.parse_args(argv) + t0 = time.time() + + # all positive subwords of words of length <= 4 over {x, y} + words = sorted({label_word("".join(p), m) + for k in range(5) for p in itertools.product("xy", repeat=k) + for m in range(1, 1 << k)}) + consistent, evidence = classify_equations(words) + + # spot-check the rules against facts that are known independently + must_be_false = [("x", "E"), ("x", "XY"), ("xx", "XY"), ("yy", "YX"), ("xxx", "XY"), + ("xxy", "XY"), ("xyx", "XY"), ("xyx", "YX"), ("xy", "YX")] + must_be_true = [("xx", "E"), ("xxy", "YX"), ("yyx", "XY"), ("xyy", "YX"), ("yxx", "XY"), + ("xxx", "E"), ("xy", "XY")] + for key in must_be_false: + require(consistent[key] is False, f"expected inconsistent {key}") + for key in must_be_true: + require(consistent[key] is True, f"expected consistent {key}") + # x^3 can equal neither xy nor yx (y would be x^2); PR6038's (F3) states a weaker form + require(not consistent[("xxx", "XY")] and not consistent[("xxx", "YX")], "x^3 rule") + + # singleton-only table: keep only the facts that a single label x or y + # is not e, xy or yx; every subset of size >= 2 may join any class. + singleton_only = {key: (val if len(key[0]) <= 1 else True) for key, val in consistent.items()} + + summary = [] + for spec in args.cases.split(","): + r, q = (int(s) for s in spec.split(":")) + for k in range(0, 4): + for name, table in (("full", consistent), ("singleton", singleton_only)): + n_idem, tuples, found = run_case(k, r, q, table) + if found: + raise SystemExit(f"FAIL length {k} {name} relaxed solution at r={r} q={q}: {found[0]}") + summary.append(f"r{r}q{q}k{k}:{tuples}") + + # positive control 1: the direct four-call word satisfies the relaxation + r, q = 2, 2 + e00, e11 = unit(r, 0), unit(r, 1) + pattern = "xyyx" + prods = subset_products((e00, e00, e11, e11), q, r) + require(relaxed_feasible(prods, allowed_labels(pattern, consistent), r, q) is not None, "direct word") + # and the search finds length-4 solutions on its own + _, _, found4 = run_case(4, 2, 2, consistent) + require(found4, "length-4 search found nothing") + + # control 2: without the group-theoretic labels (pure linear algebra, + # every nonempty subset may join any class) some length <= 3 word fits, + # so the exclusion above really uses the support facts. + control_k = None + for k in range(1, 4): + _, _, f = run_case(k, 2, 2, consistent, everything_allowed=True) + if f: + control_k = k + break + require(control_k is not None, "unrestricted control found no short solution") + + # control 3: one wrong consistency bit (allow y = xy, which forces x = e) + # must reopen a length <= 3 word at r=2, q=2. + bad = dict(consistent) + bad[("y", "XY")] = True + reopened = None + for k in range(1, 4): + _, _, f = run_case(k, 2, 2, bad) + if f: + reopened = (k, f[0][0]) + break + require(reopened is not None, "mutated consistency table did not reopen") + + n_true = sum(consistent.values()) + print(f"{MARKER} equations={len(consistent)} consistent={n_true} " + f"witnessed={evidence['witness']} forced={evidence['forced_commutation']} " + f"cases={' '.join(summary)} length4_found=1 unrestricted_control_k={control_k} " + f"mutated_reopens={reopened[0]}:{reopened[1]} seconds={time.time() - t0:.1f}") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) From 88551f6db3e5217e868b815e735c8547cd652421 Mon Sep 17 00:00:00 2001 From: josie Date: Tue, 27 Oct 2026 23:13:15 -0400 Subject: [PATCH 03/10] Fix -O check description --- research/conjugate-pair-group-free-audit/VERIFY.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/conjugate-pair-group-free-audit/VERIFY.json b/research/conjugate-pair-group-free-audit/VERIFY.json index b66ecee969..9a6f5df2f2 100644 --- a/research/conjugate-pair-group-free-audit/VERIFY.json +++ b/research/conjugate-pair-group-free-audit/VERIFY.json @@ -28,7 +28,7 @@ "{package}/verify.py" ], "timeout_seconds": 300, - "checks": "Same as the normal run under -O (no assert-dependent checks are skipped: the verifier raises SystemExit on failure paths that matter and asserts only on controls)." + "checks": "Same checks under python -O. Every check raises SystemExit explicitly (no assert statements), so -O skips nothing." } ] } From 467f434d10b4d2b7aa02d1a14d38b483b41b7a6f Mon Sep 17 00:00:00 2001 From: josie Date: Tue, 27 Oct 2026 23:14:09 -0400 Subject: [PATCH 04/10] Record second review --- research/conjugate-pair-group-free-audit/README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/research/conjugate-pair-group-free-audit/README.md b/research/conjugate-pair-group-free-audit/README.md index c1e9d01910..2822ed7c2c 100644 --- a/research/conjugate-pair-group-free-audit/README.md +++ b/research/conjugate-pair-group-free-audit/README.md @@ -30,7 +30,8 @@ identities, Lemmas 1-3 and all eight length-three patterns. For `xxy`, `yyx`, `xy`. An OpenAI Codex read-only adversarial review of the same PROOF.md and of this -verifier also reported no error. It is a second machine check, not human +verifier also reported no error. A second Codex review of this package's +Theorem S proof reported no error either. These are machine checks, not human review. **2. A stronger theorem with a shorter proof ([PROOF.md](PROOF.md)).** Fix From 093535bf4f3f2a2d8f21c27bd0f33a500af9d879 Mon Sep 17 00:00:00 2001 From: josie Date: Tue, 27 Oct 2026 23:16:15 -0400 Subject: [PATCH 05/10] Record that the support-only analogue fails for longer pair targets (local probe) --- .../conjugate-pair-group-free-audit/README.md | 24 ++++++++++++------- .../conjugate-pair-group-free-audit/TASK.json | 6 ++--- 2 files changed, 19 insertions(+), 11 deletions(-) diff --git a/research/conjugate-pair-group-free-audit/README.md b/research/conjugate-pair-group-free-audit/README.md index 2822ed7c2c..eda15df05b 100644 --- a/research/conjugate-pair-group-free-audit/README.md +++ b/research/conjugate-pair-group-free-audit/README.md @@ -113,15 +113,23 @@ Expected marker: `PASS_CONJUGATE_PAIR_GROUP_FREE_AUDIT`, in about 30 s per mode. ## Open next questions 1. **Longer diagonal pair targets (#6038 open question 1).** Theorem S is a - uniform floor of 4 for any pair target whose entries are not labels. Does a - corner argument give `≥ 6` for `diag([g],[h])` when neither `g` nor `h` is a + uniform floor of 4 for any pair target whose entries are not labels. Is + there a uniform floor of 6 for `diag([g],[h])` when neither entry is a product of at most two labels, for example `diag([xyx],[yxy])`? *Why:* it - would replace per-group pair censuses with one argument. *First step:* - extend the singleton tier so that every subset of size at most two is also - barred from the target classes, then search lengths 4 and 5 at `r = 2` over - `F2`. *Blocker:* the per-class mask enumeration here costs - `2^(allowed subsets)`, which is too slow at length five. It needs a - linear-algebra search over the subset sums instead. + would replace per-group pair censuses with one argument. *What fails + already (local probe, not registered):* the support-only analogue of + Theorem S does not hold. I kept `∅` in the `e` class, kept the singletons out + of all three classes and let only subsets of size at least three carry `g` + or `h`. A NumPy subset-sum search at `r = 2` over `F2` then finds solutions + at length 4 (20 of 1,296 idempotent tuples) and at length 5 (938 of + 7,776). The control with threshold two reproduces Theorem S: no solution + up to length 3, and 264 at length 4. So a floor of 6, if true, must use + relations among the labels, not just support sizes. *First step:* use this + package's full tier for the labels `{x, y}` and the target `(xyx, yxy)`. + That needs sound rules for when a single equation forces `xyx = yxy`; the + commutation rule used here does not imply that. Then check whether the + length-4 relaxed solutions survive. *Blocker:* the consistency rules + for the new hypothesis. 2. **Formalization.** Theorem S involves only rank-one matrices over a field and suits a proof assistant. No Lean build was attempted. diff --git a/research/conjugate-pair-group-free-audit/TASK.json b/research/conjugate-pair-group-free-audit/TASK.json index 3df775803b..da8df950f9 100644 --- a/research/conjugate-pair-group-free-audit/TASK.json +++ b/research/conjugate-pair-group-free-audit/TASK.json @@ -86,10 +86,10 @@ "ai_assistance": "Claude (Anthropic) assisted with the audit, the proof, the code and the writing. An OpenAI Codex read-only adversarial review of #6038's PROOF.md and of verify.py reported no error.", "open_questions": [ { - "question": "Does a corner argument give a uniform floor of 6 calls for diag([g],[h]) when neither entry is a product of at most two labels, e.g. diag([xyx],[yxy])? (#6038 open question 1)", + "question": "Is there a uniform floor of 6 calls for diag([g],[h]) when neither entry is a product of at most two labels, e.g. diag([xyx],[yxy])? (#6038 open question 1)", "why_it_matters": "It would replace per-group pair censuses with one uniform argument.", - "first_step": "Bar subsets of size <= 2 from the target classes in the singleton tier; search lengths 4-5 at r = 2 over F2.", - "blocked_by": "The per-class mask enumeration is 2^(allowed subsets); length five needs a linear-algebra search over subset sums." + "first_step": "The support-only analogue of Theorem S fails. A local probe at r=2 over F2, with only size>=3 subsets allowed to carry g or h, finds relaxed solutions at length 4 (20/1296 tuples) and 5 (938/7776). Next, add the label relations: a full-tier table for labels {x,y} and target (xyx, yxy), then test whether those length-4 solutions survive.", + "blocked_by": "Sound single-equation rules for the hypothesis xyx != yxy; the commutation rule used here does not imply it." }, { "question": "Formalize Theorem S in a proof assistant.", From 9890ec457cee1d541724527951c1c677d6f33944 Mon Sep 17 00:00:00 2001 From: josie Date: Tue, 27 Oct 2026 23:17:32 -0400 Subject: [PATCH 06/10] Note the exact free-group probe for diag([xyx],[yxy]) --- research/conjugate-pair-group-free-audit/README.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/research/conjugate-pair-group-free-audit/README.md b/research/conjugate-pair-group-free-audit/README.md index eda15df05b..3b57432762 100644 --- a/research/conjugate-pair-group-free-audit/README.md +++ b/research/conjugate-pair-group-free-audit/README.md @@ -124,7 +124,12 @@ Expected marker: `PASS_CONJUGATE_PAIR_GROUP_FREE_AUDIT`, in about 30 s per mode. at length 4 (20 of 1,296 idempotent tuples) and at length 5 (938 of 7,776). The control with threshold two reproduces Theorem S: no solution up to length 3, and 264 at length 4. So a floor of 6, if true, must use - relations among the labels, not just support sizes. *First step:* use this + relations among the labels, not just support sizes. A second local probe + (stdlib, not registered) solves the exact equations in the free group on + `x, y`: no word of length at most 5 reaches `diag([xyx],[yxy])` at `r = 2` + over `F2`. The same code finds the four-call words for `(xy, yx)`. A + free-group solution would map to every group, so any saving below 6 needs + a relation among the labels. *First step:* use this package's full tier for the labels `{x, y}` and the target `(xyx, yxy)`. That needs sound rules for when a single equation forces `xyx = yxy`; the commutation rule used here does not imply that. Then check whether the From 518cd2a7880f94b80c9c93aad304a7f041def647 Mon Sep 17 00:00:00 2001 From: josie Date: Tue, 27 Oct 2026 23:29:40 -0400 Subject: [PATCH 07/10] Record local r=3 F3 run --- research/conjugate-pair-group-free-audit/README.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/research/conjugate-pair-group-free-audit/README.md b/research/conjugate-pair-group-free-audit/README.md index 3b57432762..c0ae47bf6c 100644 --- a/research/conjugate-pair-group-free-audit/README.md +++ b/research/conjugate-pair-group-free-audit/README.md @@ -70,9 +70,12 @@ Theorem S. | 2 | F5 | 27,000 | no solution | no solution | | 3 | F2 | 21,952 | no solution | no solution | | 2 | F7 | 175,616 | no solution | no solution (local run, 87 s) | +| 3 | F3 | 1,601,613 | no solution | no solution (local run, 1,124 s) | -The first four rows are registered; the F7 row is a local run of the same verifier -(`--cases 2:7`). Lengths 0, 1 and 2 are also excluded in every row. +The first four rows are registered. The last two are local runs of the same +verifier (`--cases 2:7`, `--cases 3:3`). Lengths 0, 1 and 2 are also excluded +in every row. A local `--cases 4:2` run hit its 1,500 s timeout before +finishing and is not claimed. Controls, all registered: @@ -105,6 +108,7 @@ From the repository root, standard-library CPython 3.12: python3.12 -B -W error research/conjugate-pair-group-free-audit/verify.py python3.12 -O -B -W error research/conjugate-pair-group-free-audit/verify.py python3.12 -B research/conjugate-pair-group-free-audit/verify.py --cases 2:7 # optional, about 90 s +python3.12 -B research/conjugate-pair-group-free-audit/verify.py --cases 3:3 # optional, about 19 min python3.12 -B scripts/research_package.py --package research/conjugate-pair-group-free-audit ``` From 2e6a8bf3f16a249e22cb1b8d97c7e87056543a31 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 23:06:01 -0700 Subject: [PATCH 08/10] Prove scoped six-call floor by joint group-word collision refutation --- .../PROOF.md | 128 ++++++++++++++ .../README.md | 67 +++++++ .../SOURCES.json | 46 +++++ .../TASK.json | 70 ++++++++ .../VERIFY.json | 32 ++++ .../verify.py | 165 ++++++++++++++++++ 6 files changed, 508 insertions(+) create mode 100644 research/diagonal-pair-five-call-collisions/PROOF.md create mode 100644 research/diagonal-pair-five-call-collisions/README.md create mode 100644 research/diagonal-pair-five-call-collisions/SOURCES.json create mode 100644 research/diagonal-pair-five-call-collisions/TASK.json create mode 100644 research/diagonal-pair-five-call-collisions/VERIFY.json create mode 100644 research/diagonal-pair-five-call-collisions/verify.py diff --git a/research/diagonal-pair-five-call-collisions/PROOF.md b/research/diagonal-pair-five-call-collisions/PROOF.md new file mode 100644 index 0000000000..265d90a647 --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/PROOF.md @@ -0,0 +1,128 @@ +# A cancellation certificate for the five-call diagonal-pair obstruction + +## Statement and scope + +Let G be any group, L any set of group labels, and a,b distinct elements, +neither expressible as a product of zero, one or two labels from L. Over +F2[G], let D_N(g) = (I-N) + [g]N, where N is a rank-one idempotent 2 by 2 +matrix over F2 and g belongs to L. Then **no product of at most five calls is +diag([a],[b])**. + +This is a computer-assisted theorem: the written argument below proves that +an actual realization survives the finite collision relaxation; the registered +exact verifier exhausts and rejects that relaxation. It is not a handwritten +classification of all projector tuples, a proof-kernel result, a finite-group +sample, or a theorem for other fields or widths. + +In particular, when a=xyx and b=yxy satisfy the stated shortest-word and +distinctness hypotheses for L={x,y}, the minimum is exactly six. The upper +bound is D_E00(x) D_E00(y) D_E00(x) D_E11(y) D_E11(x) D_E11(y). +This is the formal register model of Wentao Li (#4089), as used by Nick +Petalas (#6038) and Josie Elliston (#6048). No native tariff, supplier or +multiplication bound is inferred. + +## The missing group implication + +Write the chronological labels of a k-call candidate as g_1,...,g_k. They +are positional symbols, not presumed distinct. For a subset U of positions, +let w_U be its increasing sequence and g_U its group product. If two such +sequences have a common prefix p, then + + g_(pu) = g_(pv) if and only if g_u = g_v. + +The same equivalence holds for a common suffix. These are cancellation and +multiplication in G; they hold in every group, including groups with torsion +and arbitrary relations. In particular inserting one nonidentity letter +between a fixed prefix and suffix cannot preserve the group element. +The certificate uses both implications, only when all sequences involved +are chronological subsets of the candidate. It does not presume that these +rules decide the word problem. + +A concrete five-call survivor of the separate scalar-pairing relaxation has +projectors, in row-major bit encoding, + + (1,5,5,3,10) = (E00, [[1,0],[1,0]], [[1,0],[1,0]], + [[1,1],[0,0]], [[0,1],[0,1]]). + +Its matrix coefficients are + + T00 = [g1 g2 g3 g4] + T01 = [g1 g2 g3 g4] + [g1 g2 g3 g5] + T10 = [g4] + [g2 g3 g4] + T11 = [g4] + [g2 g3 g5] + [g2 g3 g4]. + +The required zero T10 forces g4=g2 g3 g4, hence g2 g3=e. Consequently +T00=[g1 g4], so a has a two-label expression, contrary to the hypothesis. +Separate choices of cancellation classes for different coefficients miss +this shared implication. The finite certificate propagates it jointly. + +## Why the finite relaxation contains every realization + +Drop identity-labelled calls first. Therefore all remaining g_i are +nonidentity and k is still at most five. Expand the product exactly as + + product_i D_Ni(gi) = sum_U [g_U] P_U, + P_U = product_i (N_i if i in U else I-N_i), + +with every product in increasing position order. Each of the four matrix +entries gives an equation over F2[G]. Move [a] into the 00 equation and [b] +into the 11 equation. Every equation must now be zero. + +The solver has one node for each subset U and two extra nodes A,B for a,b. +A partition stores only equalities forced or chosen so far. Initially all +nodes are separate. A genuine realization supplies a coarser partition by +actual group value. Every solver step preserves at least one branch +compatible with that realization: + +1. **Cancellation closure.** For every common-prefix or common-suffix rule, + if its premise nodes have been equated, equate its conclusion nodes. + The group equivalences above justify this. The reverse rules are valid + multiplication by the common prefix or suffix. +2. **Forbidden equalities.** Reject if the empty subset equals a singleton, + if A=B, or if A or B equals a subset of size at most two. These contradict + respectively g_i != e, a != b, or the shortest-label hypothesis. +3. **Parity equations.** Replace each equation node by its current partition + class, retaining precisely classes with odd multiplicity. An actual + group-value class must occur evenly because the elements [g] form a + basis of F2[G]. If exactly two classes remain, their equality is forced. + If an odd number remain, no partition into even multiplicities exists. +4. **Exhaustive partner branching.** Otherwise choose the first class in a + shortest nonempty residual equation. In any actual completion its + group-value class has even multiplicity, so at least one of the other + remaining classes has that same value. Branch over every such partner + and equate them. At least one branch retains the actual realization. + +Every branch strictly merges two classes; closure also only merges classes. +Thus the search terminates. It may accept partitions unrealizable by groups, +because it omits many group implications, but this only weakens a rejection. +If every branch rejects, no actual realization of that projector tuple +exists. The node cap fails the verifier rather than declaring a rejection. + +## Finite coverage + +A nonzero rank-one idempotent over F2 is u v^T with v^T u=1. The six 2 by 2 +possibilities have row-major bit encodings 1,3,5,8,10,12. The verifier obtains +them by idempotence and trace one, then independently checks the outer-product +inventory. It evaluates all 6^k tuples for each k=0,...,5, without identifying +or omitting symmetry classes. There are 9,331 tuples in total. + +Every label sequence, in every group and every label set, is covered by the +positional-symbol argument for its projector tuple. No assignment of x,y, +no finite group, and no determinant/degree invariant is enumerated. The +computed zero survivors, together with the sound relaxation argument, +establish the scoped theorem. + +## Controls and remaining proof obligations + +The six-call direct construction is checked by exact free-word coefficients. +Removing cancellation reopens the four-call tuple (1,5,1,10), demonstrating +that support and coefficient parity alone do not prove the result. Relaxing +the target length hypothesis reopens the two-call tuple (E00,E11). The +explicit five-call example above is checked by the same refutation engine. +The verifier uses explicit checks, which remain active under Python -O. + +The proof still depends on the correctness and successful completion of the +small Python certificate. Independent human or proof-assistant review has +not been claimed. The six-projector inventory and characteristic-two parity +are essential scope restrictions; extension to other fields or widths +requires new reasoning. diff --git a/research/diagonal-pair-five-call-collisions/README.md b/research/diagonal-pair-five-call-collisions/README.md new file mode 100644 index 0000000000..f2db67b9ad --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/README.md @@ -0,0 +1,67 @@ +# Five-call diagonal-pair collision obstruction + +**All-group computer-assisted obstruction, restricted to width two over F2. +No new kappa.** In the formal rank-one-idempotent call model, a diagonal pair +of distinct targets, each requiring at least three labels, needs at least six +calls. For (xyx,yxy) satisfying these hypotheses, the direct six-call word +meets the bound. + +[PROOF.md](PROOF.md) gives the exact scope, a symbolic five-call cancellation +example, and the soundness argument for the exhaustive finite refutation. +[verify.py](verify.py) checks every one of the 9,331 projector tuples of +length zero through five. It propagates common-prefix/suffix cancellation +jointly through the four group-algebra coefficient equations. The groups +and label alphabets remain arbitrary; this is not evidence extrapolated +from a finite group census. + +This resolves the width-two/F2 portion of Josie Elliston's #6048 open +question 1. That package's support-only relaxation admitted 20 four-call +and 938 five-call projector tuples. Its arbitrary subset-class assignment +omitted joint group-word consistency. This successor adds cancellation and +all coefficient equations, rather than repeating the free-group degree +control. Nick Petalas's #6038 established the earlier four-call xy/yx result. + +## Reproduce + +Standard-library Python 3.12; approximately two seconds per direct run: + +```sh +python3 -B research/diagonal-pair-five-call-collisions/verify.py +python3 -O -B research/diagonal-pair-five-call-collisions/verify.py +python3 -B scripts/research_package.py --package research/diagonal-pair-five-call-collisions +``` + +Expected marker: `PASS_DIAGONAL_PAIR_FIVE_CALL_COLLISIONS`, with zero survivors +at every length. Registered controls include the six-call exact endpoint, +a reopened four-call support-only instance when cancellation is removed, +and a reopened two-call instance when short targets are allowed. + +The package has no runtime source dependencies. Exact predecessor proof and +README pins are provenance in SOURCES.json; their bytes are not imported or +modified. The verifier also runs directly in a Git-free source export. + +## Open next questions + +1. Does the six-call floor hold at larger widths over F2? It would remove the + two-register restriction. First inspect whether the parity refutation can + be replaced by a rank/corner argument; the six-projector inventory does + not cover larger matrices. +2. Does it hold in odd characteristic or F4? It would address the remaining + field scope of #6048's question. First derive coefficient-class constraints + with nonbinary weights; even pairing is specific to F2 and is not valid + unchanged over those fields. + +Neither question authorizes another construction round or certifies a native +implementation. Conversion, restoration, tariffs, whole callers and the +selected multiplication frontier are outside this result. + +## Credit + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance, Apache-2.0. +Josie Elliston (#6048, substantial Claude assistance) supplied the longer-pair +question, support-only counterexamples and group-free proof approach; Nick +Petalas (#6038) supplied the preceding all-group xy/yx theorem and corner +method; Wentao Li (#4089/#4093) supplied the rank-one-idempotent group-algebra +model, following Cinna Davis's A5 target (#2246). Their broader results are +not re-audited here. Source heads are pinned, and no frozen predecessor is +changed. diff --git a/research/diagonal-pair-five-call-collisions/SOURCES.json b/research/diagonal-pair-five-call-collisions/SOURCES.json new file mode 100644 index 0000000000..c2b6406a81 --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/SOURCES.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/conjugate-pair-group-free-audit/README.md", + "usage": "provenance", + "pin": "head:518cd2a7880f94b80c9c93aad304a7f041def647:research/conjugate-pair-group-free-audit/README.md", + "git_blob": "c0ae47bf6c566c69466e150661641d61fd9ff636", + "sha256": "3adf65a79d27ea7a60ec8978fa6b45f75d65c07c3aed019080b64431078f28f3" + }, + { + "path": "research/conjugate-pair-group-free-audit/PROOF.md", + "usage": "provenance", + "pin": "head:518cd2a7880f94b80c9c93aad304a7f041def647:research/conjugate-pair-group-free-audit/PROOF.md", + "git_blob": "a92cbe6f25408cd5ff1e4f820963d44cabc9f362", + "sha256": "a37a1bc0bd306a94c148c703c43e41ee4f8d90fcf009cfeb7cee8b2a31fa600a" + }, + { + "path": "research/conjugate-pair-every-group/README.md", + "usage": "provenance", + "pin": "head:0cee0e104b68ce6f06bf84af03f46ac30680e64c:research/conjugate-pair-every-group/README.md", + "git_blob": "47bb74c1399e2bed48afd5be200e53223bb7e4c0", + "sha256": "9ddac65a112890de4d098a5387209927d753cbdb68fa3a5d064d6dfe717b9a1a" + }, + { + "path": "research/conjugate-pair-every-group/PROOF.md", + "usage": "provenance", + "pin": "head:0cee0e104b68ce6f06bf84af03f46ac30680e64c:research/conjugate-pair-every-group/PROOF.md", + "git_blob": "46d33fc3b993a53435bf8c450421a5310e20a8a0", + "sha256": "414b5f88f7fd24d7066b03efa371bdf7a28fbed22a8c36fd78a1073b469aafd2" + } + ] +} diff --git a/research/diagonal-pair-five-call-collisions/TASK.json b/research/diagonal-pair-five-call-collisions/TASK.json new file mode 100644 index 0000000000..da30f03b65 --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove or refute the five-call diagonal-pair obstruction using genuine group-word collisions, initially width two over F2.", + "scope_change_reason": "Explicit preclaimed handoff #6048 open question 1 replaces the generic register-model task; formal group-algebra obstruction only, no native implementation.", + "bottleneck_link": "A scoped lower bound on sharing longer noncommutative diagonal targets; no primitive saving or complete BIT supplier is claimed.", + "budget_minutes": 30, + "stop_rule": "One written collision lemma or exact counterexample; bounded exhaustive projector certificate only, no finite-group inference.", + "outcome": "completed", + "evidence": "PROOF.md and registered verify.py: all 9331 tuples at lengths 0 through 5 rejected; exact six-call endpoint and weakened-hypothesis controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Does the six-call floor extend to larger widths over F2?", + "why_it_matters": "Removes the two-register restriction.", + "first_step": "Replace the six-projector case split by a rank/corner argument.", + "blocked_by": "Finite projector inventory only covers width two." + }, + { + "question": "Does the six-call floor extend to odd characteristic or F4?", + "why_it_matters": "Addresses remaining field scope of predecessor question.", + "first_step": "Derive weighted coefficient-class constraints.", + "blocked_by": "Even pairing is specific to F2." + } + ] +} diff --git a/research/diagonal-pair-five-call-collisions/VERIFY.json b/research/diagonal-pair-five-call-collisions/VERIFY.json new file mode 100644 index 0000000000..35e9a200ff --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All 9331 projector tuples, common-prefix/suffix collision closure, exact six-call endpoint, missing-cancellation and short-target controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All 9331 projector tuples, common-prefix/suffix collision closure, exact six-call endpoint, missing-cancellation and short-target controls." + } + ] +} diff --git a/research/diagonal-pair-five-call-collisions/verify.py b/research/diagonal-pair-five-call-collisions/verify.py new file mode 100644 index 0000000000..dba96ff06e --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/verify.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +"""Exact all-group collision refutation; standard library, no group sampling.""" +import itertools +import json + +IDENTITY = 9 + + +def require(condition, message): + if not condition: + raise SystemExit('FAIL ' + message) + + +def multiply(a, b): + return sum((sum(((a >> (2*i+t)) & 1) * ((b >> (2*t+j)) & 1) + for t in range(2)) % 2) << (2*i+j) + for i in range(2) for j in range(2)) + + +PROJECTORS = tuple(n for n in range(16) + if multiply(n, n) == n and ((n & 1) ^ ((n >> 3) & 1))) + + +def expand(projectors): + terms = {0: IDENTITY} + for position, n in enumerate(projectors): + terms = {mask: product for old, coefficient in terms.items() + for mask, product in ((old, multiply(coefficient, IDENTITY ^ n)), + (old | (1 << position), multiply(coefficient, n)))} + return terms + + +def cancellation_rules(k): + words = [tuple(i for i in range(k) if mask >> i & 1) for mask in range(1 << k)] + index = {word: mask for mask, word in enumerate(words)} + rules = set() + for a, u in enumerate(words): + for b, v in enumerate(words[:a]): + prefix = suffix = 0 + while prefix < min(len(u), len(v)) and u[prefix] == v[prefix]: + prefix += 1 + while suffix < min(len(u), len(v)) and u[-1-suffix] == v[-1-suffix]: + suffix += 1 + for left, right in ((u[prefix:], v[prefix:]), + (u[:-suffix], v[:-suffix]) if suffix else (u, v)): + c, d = index[left], index[right] + if (a, b) != (c, d): + rules.add((a, b, c, d)) + rules.add((c, d, a, b)) + return tuple(sorted(rules)) + + +class CollisionProblem: + def __init__(self, k, cancellation=True, minimum=3): + self.k = k + self.target_a = 1 << k + self.target_b = self.target_a + 1 + self.rules = cancellation_rules(k) if cancellation else () + self.short = tuple(mask for mask in range(1 << k) if mask.bit_count() < minimum) + self.nodes = 0 + + def solve(self, projectors): + require(len(projectors) == self.k, 'wrong word length') + terms = expand(projectors) + equations = tuple(tuple(mask for mask, value in terms.items() if value >> entry & 1) + + ((self.target_a,) if entry == 0 else + (self.target_b,) if entry == 3 else ()) for entry in range(4)) + return self.search(equations, list(range((1 << self.k) + 2))) + + def search(self, equations, partition): + self.nodes += 1 + require(self.nodes <= 200000, 'explicit search-node cap exceeded') + parent = partition[:] + + def root(a): + while parent[a] != a: + a = parent[a] + return a + + def union(a, b): + a, b = root(a), root(b) + if a == b: + return False + parent[max(a, b)] = min(a, b) + return True + + while True: + changed = False + for a, b, c, d in self.rules: + if root(a) == root(b): + changed = union(c, d) or changed + if any(root(0) == root(1 << i) for i in range(self.k)): + return None + if root(self.target_a) == root(self.target_b): + return None + if any(root(target) == root(mask) for target in (self.target_a, self.target_b) + for mask in self.short): + return None + residual = [] + for equation in equations: + odd = set() + for node in equation: + node = root(node) + odd.symmetric_difference_update((node,)) + if len(odd) % 2: + return None + if len(odd) == 2: + changed = union(*odd) or changed + elif odd: + residual.append(tuple(sorted(odd))) + if not changed: + break + if not residual: + return parent + equation = min(residual, key=lambda item: (len(item), item)) + first = equation[0] + # Every true equality class has even parity, so first has a partner. + for partner in equation[1:]: + branch = parent[:] + a, b = root(first), root(partner) + branch[max(a, b)] = min(a, b) + witness = self.search(equations, branch) + if witness is not None: + return witness + return None + + +def exact_endpoint(pattern, projectors): + coefficients = {} + for mask, coefficient in expand(projectors).items(): + word = ''.join(label for i, label in enumerate(pattern) if mask >> i & 1) + coefficients[word] = coefficients.get(word, 0) ^ coefficient + return {word: value for word, value in coefficients.items() if value} + + +def main(): + require(PROJECTORS == (1, 3, 5, 8, 10, 12), 'rank-one projector inventory') + # Independent outer-product characterization, not a second trace filter. + outer = {sum(((u >> i) & 1)*((v >> j) & 1) << (2*i+j) + for i in range(2) for j in range(2)) + for u in (1, 2, 3) for v in (1, 2, 3) if (u & v).bit_count() % 2} + require(set(PROJECTORS) == outer, 'outer-product inventory mismatch') + require(multiply(3, 5) != multiply(5, 3), 'matrix order control') + require(exact_endpoint('xyxyxy', (1, 1, 1, 8, 8, 8)) == {'xyx': 1, 'yxy': 8}, + 'six-call positive endpoint') + relaxed = CollisionProblem(4, cancellation=False) + require(relaxed.solve((1, 5, 1, 10)) is not None, 'missing-cancellation control did not reopen') + shortened = CollisionProblem(2, minimum=1) + require(shortened.solve((1, 8)) is not None, 'short-target control did not reopen') + require(CollisionProblem(5).solve((1, 5, 5, 3, 10)) is None, + 'written five-call collision example') + results = [] + for k in range(6): + problem = CollisionProblem(k) + tested = 0 + for projectors in itertools.product(PROJECTORS, repeat=k): + require(problem.solve(projectors) is None, 'surviving collision relaxation ' + str(projectors)) + tested += 1 + require(tested == 6**k, 'incomplete projector enumeration') + results.append({'calls': k, 'tuples': tested, 'nodes': problem.nodes, 'survivors': 0}) + print('PASS_DIAGONAL_PAIR_FIVE_CALL_COLLISIONS ' + json.dumps(results, sort_keys=True)) + + +if __name__ == '__main__': + main() From 3c6876196d006fd5757ae3e55f93b5ae1ae0f845 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 23:06:30 -0700 Subject: [PATCH 09/10] Validate collision rules and preserve known feasible endpoints --- .../PROOF.md | 5 ++++- .../README.md | 4 +++- .../verify.py | 20 +++++++++++++++++++ 3 files changed, 27 insertions(+), 2 deletions(-) diff --git a/research/diagonal-pair-five-call-collisions/PROOF.md b/research/diagonal-pair-five-call-collisions/PROOF.md index 265d90a647..d3b230f214 100644 --- a/research/diagonal-pair-five-call-collisions/PROOF.md +++ b/research/diagonal-pair-five-call-collisions/PROOF.md @@ -119,7 +119,10 @@ Removing cancellation reopens the four-call tuple (1,5,1,10), demonstrating that support and coefficient parity alone do not prove the result. Relaxing the target length hypothesis reopens the two-call tuple (E00,E11). The explicit five-call example above is checked by the same refutation engine. -The verifier uses explicit checks, which remain active under Python -O. +The verifier independently authenticates every generated cancellation rule as a +single common-context law, checks the displayed coefficient expansion, and +accepts the actual four- and six-call constructions in the collision solver. +It uses explicit checks, which remain active under Python -O. The proof still depends on the correctness and successful completion of the small Python certificate. Independent human or proof-assistant review has diff --git a/research/diagonal-pair-five-call-collisions/README.md b/research/diagonal-pair-five-call-collisions/README.md index f2db67b9ad..7eea39a8e5 100644 --- a/research/diagonal-pair-five-call-collisions/README.md +++ b/research/diagonal-pair-five-call-collisions/README.md @@ -34,7 +34,9 @@ python3 -B scripts/research_package.py --package research/diagonal-pair-five-cal Expected marker: `PASS_DIAGONAL_PAIR_FIVE_CALL_COLLISIONS`, with zero survivors at every length. Registered controls include the six-call exact endpoint, a reopened four-call support-only instance when cancellation is removed, -and a reopened two-call instance when short targets are allowed. +and a reopened two-call instance when short targets are allowed. Independent +controls authenticate every generated context rule and require the collision +solver itself to accept the known four- and six-call constructions. The package has no runtime source dependencies. Exact predecessor proof and README pins are provenance in SOURCES.json; their bytes are not imported or diff --git a/research/diagonal-pair-five-call-collisions/verify.py b/research/diagonal-pair-five-call-collisions/verify.py index dba96ff06e..8710e77059 100644 --- a/research/diagonal-pair-five-call-collisions/verify.py +++ b/research/diagonal-pair-five-call-collisions/verify.py @@ -141,6 +141,26 @@ def main(): for u in (1, 2, 3) for v in (1, 2, 3) if (u & v).bit_count() % 2} require(set(PROJECTORS) == outer, 'outer-product inventory mismatch') require(multiply(3, 5) != multiply(5, 3), 'matrix order control') + # Independently authenticate every generated rule as a single context law. + for k in range(7): + words = [tuple(i for i in range(k) if mask >> i & 1) for mask in range(1 << k)] + for a, b, c, d in cancellation_rules(k): + valid = False + for u, v, s, t in ((words[a], words[b], words[c], words[d]), + (words[c], words[d], words[a], words[b])): + for split in range(len(u) + 1): + context = u[:split] + valid |= u == context + s and v == context + t + context = u[split:] + valid |= u == s + context and v == t + context + require(valid, 'invalid cancellation rule') + require(CollisionProblem(6).solve((1, 1, 1, 8, 8, 8)) is not None, + 'solver rejected six-call true endpoint') + require(CollisionProblem(4, minimum=2).solve((1, 1, 8, 8)) is not None, + 'solver rejected preceding four-call true endpoint') + require({m: v for m, v in expand((1, 5, 5, 3, 10)).items() if v} + == {8: 12, 14: 12, 15: 3, 22: 8, 23: 2}, + 'written collision example coefficients') require(exact_endpoint('xyxyxy', (1, 1, 1, 8, 8, 8)) == {'xyx': 1, 'yxy': 8}, 'six-call positive endpoint') relaxed = CollisionProblem(4, cancellation=False) From 0a24101a977a652a306dd252b009d54840e4fdc9 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 23:08:02 -0700 Subject: [PATCH 10/10] Close the free scalar basis-change normalization obligation --- .../PROOF.md | 24 +++++++++++++++++-- .../README.md | 4 ++-- 2 files changed, 24 insertions(+), 4 deletions(-) diff --git a/research/diagonal-pair-five-call-collisions/PROOF.md b/research/diagonal-pair-five-call-collisions/PROOF.md index d3b230f214..75a4586f3a 100644 --- a/research/diagonal-pair-five-call-collisions/PROOF.md +++ b/research/diagonal-pair-five-call-collisions/PROOF.md @@ -21,6 +21,27 @@ This is the formal register model of Wentao Li (#4089), as used by Nick Petalas (#6038) and Josie Elliston (#6048). No native tariff, supplier or multiplication bound is inferred. +## Free scalar changes of basis + +The stated product form also covers arbitrary invertible scalar basis changes +between paid calls. Write such a circuit as + + S0 D_N1(g1) S1 ... D_Nk(gk) Sk, + Si in GL_2(F2). + +Let Ci=S0 ... S_(i-1). The identity S D_N(g) S^-1 = D_(S N S^-1)(g) +moves each scalar factor to the right, giving + + D_(C1 N1 C1^-1)(g1) ... D_(Ck Nk Ck^-1)(gk) S, + S=S0 ... Sk. + +Conjugation preserves rank-one idempotence, so every resulting projector is +in the six-element inventory. The group-algebra augmentation [g] -> 1 sends +every paid factor to I and sends diag([a],[b]) to I. Thus any successful +circuit has S=I. Free scalar changes of basis therefore add no missing +terminal factor or extra cases. This normalization does not admit free +address-dependent maps, clean auxiliary registers, COPY or ERASE. + ## The missing group implication Write the chronological labels of a k-call candidate as g_1,...,g_k. They @@ -38,8 +59,7 @@ The certificate uses both implications, only when all sequences involved are chronological subsets of the candidate. It does not presume that these rules decide the word problem. -A concrete five-call survivor of the separate scalar-pairing relaxation has -projectors, in row-major bit encoding, +A concrete five-call tuple has projectors, in row-major bit encoding, (1,5,5,3,10) = (E00, [[1,0],[1,0]], [[1,0],[1,0]], [[1,1],[0,0]], [[0,1],[0,1]]). diff --git a/research/diagonal-pair-five-call-collisions/README.md b/research/diagonal-pair-five-call-collisions/README.md index 7eea39a8e5..cebd2e061c 100644 --- a/research/diagonal-pair-five-call-collisions/README.md +++ b/research/diagonal-pair-five-call-collisions/README.md @@ -10,8 +10,8 @@ meets the bound. example, and the soundness argument for the exhaustive finite refutation. [verify.py](verify.py) checks every one of the 9,331 projector tuples of length zero through five. It propagates common-prefix/suffix cancellation -jointly through the four group-algebra coefficient equations. The groups -and label alphabets remain arbitrary; this is not evidence extrapolated +jointly through the four group-algebra coefficient equations. Free invertible scalar basis changes are normalized by conjugation and +augmentation in the proof. The groups and label alphabets remain arbitrary; this is not evidence extrapolated from a finite group census. This resolves the width-two/F2 portion of Josie Elliston's #6048 open