Audit #6038 and prove a group-free four-call floor for diagonal pair targets (no new κ)

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.

research/conjugate-pair-group-free-audit/README.md

@@ -0,0 +1,153 @@
+# 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. 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
+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) |
+| 3 | F3 | 1,601,613 | no solution | no solution (local run, 1,124 s) |
+
+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:
+
+* 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 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
+```
+
+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. 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. *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. 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
+   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.
+
+## 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).

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