Classify mixed Q8 call-space shear identities; no pair of shear images separates (no new κ)

research/q8-mixed-shear-identity-space/PROOF.md

@@ -0,0 +1,177 @@
+# Call-space identities for mixed positive-Q8 words
+
+## Model
+
+The model is the one in `research/q8-mixed-boundary-rank/PROOF.md` and
+`research/q8-square-iblock-obstruction/PROOF.md`. Work in the full formal
+group algebra `F2[Q8]`. Every role starts with independent arbitrary dirty
+input, and binary scalar GL mixing is free. A paid call is
+
+```text
+D_l = I + x_l u_l v_l^T,   x_l = 1 + [g_l],   g_l in {i, j},   v_l^T u_l = 1.
+```
+
+Call 0 acts first. The endpoint is diagonal: `t_i` roles carry `[zi]`,
+`t_j` roles carry `[zj]`, and every other role is restored to the identity.
+Any finite number of restored roles is allowed. After conjugating the free
+mixing through the calls (the PR3517 normal form), let `X` be the `t × n`
+active rows of the `u_l` columns and `Y` the `n × t` active columns of the
+`v_l^T` rows. Let `L` be the strictly lower part of the full-role Gram matrix
+`(v_l^T u_a)`. Dirty coordinates contribute to `L`. Let `E_i` and `E_j` be
+the diagonal projectors onto i-calls and j-calls, and let `P_i` and `P_j` be
+the active target projectors.
+
+For a label word `w = w_0 w_1 ... w_d`, define the block monomial
+
+```text
+M_w = E_{w_0} L E_{w_1} L ... L E_{w_d}.
+```
+
+The left label is the latest call. The calculus `C_3` consists of the 30
+monomials with `d <= 3`, together with `P_i` and `P_j`. An *identity* of
+`C_3` is a coefficient vector `c` in `F2^32` such that
+
+```text
+sum_w c_w X M_w Y + c_i P_i + c_j P_j = 0
+```
+
+holds for every exact word of every shape and every finite workspace.
+
+## The coefficient equations
+
+Put `a = 1+[i]` and `b = 1+[j]`. Then `a^2 = b^2 = 1+[z]`, and every product
+of five factors from `{a, b}` is zero. The eight elements
+
+```text
+1, a, b, aa, ab, aaa, aab, aaab
+```
+
+form a basis of `F2[Q8]`; the verifier checks this and every coordinate used
+below. Expanding the product in chronological order gives
+
+```text
+W = I + sum over chains l_0 > l_1 > ... > l_d of
+        x_{l_0} ... x_{l_d} u_{l_0}(v_{l_0}^T u_{l_1}) ... (v_{l_{d-1}}^T u_{l_d}) v_{l_d}^T.
+```
+
+Scalar matrices commute with group-algebra coefficients, and chains with
+`d >= 4` vanish. The active block of the label-`w` chains is `X M_w Y`.
+Equating each basis coordinate of the active block with the target
+coordinates gives seven equations. The coordinates of `[zi]` are
+`1, a, aa, aaa` and those of `[zj]` are `1, b, aa, aab`.
+
+```text
+a    : i + Pi = 0
+b    : j + Pj = 0
+aa   : ii + ji + jj + Pi + Pj = 0
+ab   : ij + ji = 0
+aaa  : ji + iii + iji + ijj + jij + jji + Pi = 0
+aab  : ji + iij + iji + jii + jij + jjj + Pj = 0
+aaab : ji + iji + jij + iiij + iiji + ijii + ijij + ijjj
+       + jiii + jiji + jijj + jjij + jjji = 0
+```
+
+Here a word `w` stands for `X M_w Y`. The quadratic pair is the
+`X(I+H)Y = 0` identity and its orientation-swapped partner from the
+mixed-boundary proof (Nick Petalas/PR3570). It is restated here, not claimed
+as new.
+
+## Theorem A: the identity space of `C_3`
+
+**The identities of `C_3` are exactly the span of the seven coefficient
+equations, a 7-dimensional subspace of `F2^32`.**
+
+*Proof.* Each coefficient equation holds for every exact word, so the span
+consists of identities. Conversely, `WITNESS.json` lists 25 exact words, on
+one or two roles, of lengths 3 to 8. Each active entry `(p, q)` of each word
+gives a row vector in `F2^32` that every identity annihilates. The verifier
+recomputes each endpoint exactly, forms these rows, and finds rank 25. The
+annihilator of the rows therefore has dimension 7. It contains the span of
+the seven independent equations, so the two spaces are equal. ∎
+
+So no further degree-three call-space identity holds for active
+compressions, whatever the shape and workspace. A cyclic-style identity
+such as `X(I+L)^2 Y = 0` is outside the span. The verifier finds an
+explicit witness row that refutes it.
+
+## Theorem B: the four shears
+
+Call `h` a *strict block polynomial* if it is a sum of monomials `M_w` with
+`d` equal to 1 or 2. Then `I + h` is unitriangular and invertible.
+
+**Exactly four strict block polynomials give an identity `X(I+h)Y = 0`:**
+
+```text
+K1 = I + ii + ji + jj
+K2 = I + ii + ij + jj
+Q1 = I + iii + iij + ijj + jii + jji + jjj
+Q2 = Q1 + ij + ji
+```
+
+**No product of two of them whose degree stays at most three gives an
+identity.** That covers 12 of the 16 ordered products. The four products
+`Q_a Q_b` reach degree four and lie outside `C_3`.
+
+*Proof.* By Theorem A, `X(I+h)Y = 0` is an identity exactly when its
+coefficient vector lies in the 7-dimensional span. The verifier checks all
+`2^12 - 1` nonempty strict block polynomials and all 12 products. ∎
+
+`K1` and `K2` are the two quadratic shears of PR3570. `Q1` is the sum of the
+`aaa` and `aab` equations. On a word that uses one label on each role,
+`K1 = K2 = I + L` and `Q1 = Q2 = I + L^2`. These are the cyclic `K` and `K^2`
+of `research/q8-cyclic-cubic-obstruction/PROOF.md`.
+
+## Theorem C: every pair of shear images can meet
+
+Let `U = im(Y)`, a `t`-dimensional subspace of the call space `F2^n`. Each
+of `K1 U`, `K2 U`, `Q1 U` and `Q2 U` is `t`-dimensional and lies in
+`ker(X)`, which has dimension `n - t`.
+
+**For each of the six pairs of these images, some exact one-role
+three-call word gives a nonzero intersection.**
+
+*Proof.* Each witness has `u = v = 1` for all three calls. Listed in
+chronological order (call 0 first), the label sequences are `ijj`, with
+endpoint `[j][j][i] = [zi]`, and `iij` and `jii`, with endpoint `[zj]`.
+Here `t = 1`, and for each pair the two images span only one dimension.
+The verifier searches all eight one-role label sequences and records one
+witness per pair. ∎
+
+The cyclic theorem proves `n >= 3t` from the disjointness of `KU` and
+`K^2 U`, which holds on every word. In the mixed model no pair of the four
+images is disjoint on every word, even at `t = 1`. A two-image argument of
+the PR3558 kind therefore cannot certify `n >= 3t` for mixed words. This
+also explains why PR3570 only obtains rank inequalities with a defect term.
+
+## Conjecture D: the four images together
+
+**Conjecture.** For every exact word,
+
+```text
+dim(K1 U + K2 U + Q1 U + Q2 U) >= 2t.
+```
+
+The sum lies in `ker(X)`, so the conjecture implies `n >= 3t` for every
+mixed shape. The direct word attains this bound. In particular, it would
+give exact minima of 15 at shape `(4,1)` and 24 at shape `(7,1)`. On words
+with one label per role the four images reduce to `KU + K^2 U`, so the
+conjecture holds there by the cyclic theorem.
+
+*Finite evidence, not a proof.* The verifier enumerates every exact word
+in these classes by meet-in-the-middle. The classes are one role at
+length 3, and two roles at lengths 5, 6 and 7, with every target in
+`{zi, zj, 1}^r`. With `--full` it also covers two roles at length 8.
+Every word meets the conjectured bound. The exact counts are in the
+README. Here `t <= 2`, where `n >= 3t` is already known, so this evidence
+decides no open length.
+
+## What is not claimed
+
+Theorem A is a statement about the degree-three compression calculus. It
+does not exclude identities involving degree-four or higher monomials. On
+words of length 8 those monomials are nonzero, even though their
+coefficients vanish in `W`. It also does not exclude non-linear rank
+arguments, arguments that use the dirty rows and columns of the endpoint,
+or arguments outside call space. The (4,1) and (7,1) minima remain open.
+Conjecture D is unproved. No physical caller, invoice, supplier or new
+kappa is claimed, and the selected frontier is unchanged.

research/q8-mixed-shear-identity-space/README.md

@@ -0,0 +1,121 @@
+# Call-space identities for mixed positive-Q8 words
+
+**Scoped proof with an exact finite certificate, plus a conjecture. No new κ.**
+The selected frontier is unchanged.
+
+## Question
+
+unpaidmoon's [PR #4378](https://github.com/CrocSwap/integer-mult-bounds/pull/4378)
+(`research/q8-square-iblock-obstruction`) leaves open whether four `[zi]`
+targets and one `[zj]` target need 13 or 15 positive i/j calls. For words that
+use a single label, `research/q8-cyclic-cubic-obstruction` (PR3558) proves
+`n >= 3t` from two call-space identities, `X K Y = 0` and `X K^2 Y = 0`. Can
+the mixed coefficient equations supply a pair of the same kind?
+
+## Result
+
+[PROOF.md](PROOF.md) has the definitions and proofs.
+
+- **Theorem A (identity space).** Take active compressions `X M_w Y` of the 30
+  label-block monomials `E L E ... L E` with at most three factors `L`,
+  together with the target projectors `P_i`, `P_j`. The linear identities
+  that hold for every exact word, of every shape and every finite dirty
+  workspace, are exactly the span of the seven `F2[Q8]` coefficient
+  equations. This span has dimension 7. The 25 explicit exact words in
+  [WITNESS.json](WITNESS.json) give compression rows of rank 25 out of 32,
+  which refutes every other candidate.
+- **Theorem B (shears).** Exactly four unitriangular operators `I+h`, with
+  `h` of degree one or two, satisfy `X(I+h)Y = 0`. They are the two PR3570
+  shears `K1` and `K2` and two cubic shears `Q1` and `Q2`. None of the 12
+  products of two shears of degree at most three is an identity.
+- **Theorem C (pairs meet).** For each of the six pairs among `K1 U`,
+  `K2 U`, `Q1 U` and `Q2 U`, where `U = im Y`, some exact one-role
+  three-call word makes the two images intersect. The cyclic two-image
+  argument therefore has no mixed analogue in this calculus, even at `t = 1`.
+- **Conjecture D.** For every exact word,
+  `dim(K1 U + K2 U + Q1 U + Q2 U) >= 2t`. All four images lie in `ker X`, so
+  the conjecture would give `n >= 3t` for every mixed shape. That would make
+  the exact minimum 15 at `(4,1)` and 24 at `(7,1)`. The conjecture is
+  unproved. In complete meet-in-the-middle censuses it holds on every exact
+  mixed-label word:
+
+  | roles | length | exact words | mixed-label | span − 2t: count |
+  |---:|---:|---:|---:|---|
+  | 1 | 3 | 6 | 4 | 0: 4 |
+  | 2 | 5 | 24 | 24 | 1: 24 |
+  | 2 | 6 | 12,368 | 9,824 | 0: 9,824 |
+  | 2 | 7 | 68,512 | 52,592 | 0: 44,884; 1: 7,708 |
+  | 2 | 8 (`--full`) | 407,296 | 407,296 | 1: 359,836; 2: 47,460 |
+
+  Targets range over `{zi, zj, 1}^r`, excluding the all-identity target.
+  These censuses have `t <= 2`, where `n >= 3t` is already known. They are
+  evidence for the conjecture, not a new length bound.
+
+The (4,1) question is not decided. For the next contributor, the result
+means that a mixed `n >= 3t` proof cannot come from one more linear
+compression identity of degree at most three, or from disjointness of a
+single pair of shear images. It needs a joint four-image (or larger)
+argument, monomials of degree four or higher, the dirty endpoint blocks,
+or a non-compression method.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library only:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/q8-mixed-shear-identity-space
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/q8-mixed-shear-identity-space/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/q8-mixed-shear-identity-space/verify.py --full
+```
+
+The registered command takes about 15 seconds and prints
+`PASS_Q8_MIXED_SHEAR_IDENTITY_SPACE` with a JSON summary. The `--full` run
+adds the two-role length-8 census (about 3 minutes locally) and is opt-in.
+Neither run writes files.
+
+Not run: Lean, Docker and the selected full cold replay. This package
+changes none of their inputs.
+
+## Limitations
+
+Theorem A covers the degree-three compression calculus only. It does not
+exclude identities with degree-four or higher monomials, rank arguments
+that are not linear identities, arguments that use dirty rows and columns,
+or methods outside call space. The census proves Theorems A and C by
+explicit witnesses; for Conjecture D it is finite evidence only. Nothing
+here prices a physical caller, routing, restoration, hosting, precision or
+a supplier. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+Structured versions are in [TASK.json](TASK.json).
+
+1. **Prove Conjecture D.** A proof gives `n >= 3t` for every mixed shape and
+   closes both open lengths of PR #4378. First step: test it on three-role
+   words of length 9 with `t = 3`, where PR3536 already gives the minimum 9.
+   Then look for a filtration argument that uses `K2 = K1 + (ij + ji)` and
+   `Q2 = Q1 + (ij + ji)`.
+2. **Which identities appear at degree four?** Theorem A stops at degree
+   three. Higher monomials have zero coefficients in `W` but are nonzero
+   compressions. First step: build two- and three-role witness sets with
+   rank deficiency explained, before trusting any apparent degree-four
+   relation found on two-role samples. Two-role samples can produce
+   small-dimension relations.
+3. **Does a 13-call word exist at shape (4,1)?** A counterexample to
+   Conjecture D at `t = 5` would be the place to look. First step: a
+   meet-in-the-middle search restricted to six-role cores (PR3536's
+   half-call scalar core bounds the core at `floor(13/2)`). This is far
+   beyond the census here.
+
+## Credit
+
+Produced by Nick Petalas. The model, the PR3517 normal form, the PR3570
+mixed quadratic identities and the PR3558 cyclic subspace theorem are
+earlier work of Nick Petalas, credited and not re-audited. The open (4,1)
+question is from unpaidmoon's PR #4378. The register-model lineage in those
+packages (Tuafo/PR2900, ywz65/PR2587, Aaron Wang/PR2318, Cinna Davis,
+steph4n-gh and others) keeps its credit. New here: the complete identity
+space of the degree-three calculus, the classification of the four shears,
+the six pair-intersection witnesses, and Conjecture D with its census.
+
+Apache-2.0.

research/q8-mixed-shear-identity-space/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/q8-cyclic-cubic-obstruction/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c10246b660b166d2a38d2acc554631ec69d72204",
+      "sha256": "79f4e73015c64360fcf635ce0b4288738f73a46bd95178dde3d26807d6de294e"
+    },
+    {
+      "path": "research/q8-mixed-boundary-rank/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "771efad64c1a7930d6e68d55ace64357d27fdcc0",
+      "sha256": "331c45cd80d563bf956caa029db241014dc66235b41f6fa83833e3c7ee5f4294"
+    },
+    {
+      "path": "research/q8-square-iblock-obstruction/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c67d14c6e6399d49ecc2cf725b44e9390e4b4dd5",
+      "sha256": "a56ddbc7ef070222dbfc9959bc28b73cd804d8b52b382446bac136a1265fa24c"
+    }
+  ]
+}