Prove the conjugate-pair target needs four calls in every group (no new κ)

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 κ.

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).

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}