From f78a9d4912308264b2c7c04c54d1db76c51d6a6f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 00:30:21 +0000 Subject: [PATCH] feat(research): classify mixed Q8 call-space shear identities The degree-three compression calculus has exactly the seven coefficient equations as identities. Four shears survive, no product of two is an identity, and every pair of shear images meets on a three-call word. Records the four-image span conjecture that would give n >= 3t. --- .../q8-mixed-shear-identity-space/PROOF.md | 177 ++++ .../q8-mixed-shear-identity-space/README.md | 121 +++ .../SOURCES.json | 36 + .../q8-mixed-shear-identity-space/TASK.json | 76 ++ .../q8-mixed-shear-identity-space/VERIFY.json | 18 + .../WITNESS.json | 844 ++++++++++++++++++ .../q8-mixed-shear-identity-space/verify.py | 413 +++++++++ 7 files changed, 1685 insertions(+) create mode 100644 research/q8-mixed-shear-identity-space/PROOF.md create mode 100644 research/q8-mixed-shear-identity-space/README.md create mode 100644 research/q8-mixed-shear-identity-space/SOURCES.json create mode 100644 research/q8-mixed-shear-identity-space/TASK.json create mode 100644 research/q8-mixed-shear-identity-space/VERIFY.json create mode 100644 research/q8-mixed-shear-identity-space/WITNESS.json create mode 100644 research/q8-mixed-shear-identity-space/verify.py diff --git a/research/q8-mixed-shear-identity-space/PROOF.md b/research/q8-mixed-shear-identity-space/PROOF.md new file mode 100644 index 0000000000..02fe029a47 --- /dev/null +++ b/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. diff --git a/research/q8-mixed-shear-identity-space/README.md b/research/q8-mixed-shear-identity-space/README.md new file mode 100644 index 0000000000..359313f6ac --- /dev/null +++ b/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. diff --git a/research/q8-mixed-shear-identity-space/SOURCES.json b/research/q8-mixed-shear-identity-space/SOURCES.json new file mode 100644 index 0000000000..155f306c72 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/q8-mixed-shear-identity-space/TASK.json b/research/q8-mixed-shear-identity-space/TASK.json new file mode 100644 index 0000000000..8f165dc66c --- /dev/null +++ b/research/q8-mixed-shear-identity-space/TASK.json @@ -0,0 +1,76 @@ +{ + "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": "Inside the existing F2[Q8] dirty-register model with positive i/j calls: the complete space of linear identities among active compressions X M Y of label-block monomials of degree at most three is exactly the 7-dimensional span of the coefficient equations; exactly four unitriangular shears of degree at most two satisfy X(I+h)Y=0 and no degree-at-most-three product of two of them does; every pair of their images meets on an exact one-role three-call word. Conjecture: the four images together span at least 2t, which would imply n>=3t for every mixed shape. The (4,1) minimum is not decided. No new alphabet and no new kappa.", + "scope_change_reason": "The card asks whether a new alphabet escapes the three-register obstruction. This package stays inside the specified F2[Q8] model and addresses the method question behind PR #4378's open (4,1) length: whether the cyclic two-identity subspace proof of n>=3t has a mixed analogue. A scoped negative method result is retained without a supplier; no construction round is started.", + "bottleneck_link": "Side result in the nonabelian register model. It does not change the selected conditional kappa, and no physical caller or supplier admission is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop once the degree-three identity space, the shear classification and the six pair witnesses are certified, and the four-image conjecture is recorded with its complete small censuses. Do not search 13-call (4,1) words.", + "outcome": "partial", + "evidence": "PROOF.md, WITNESS.json and verify.py: exact endpoints of 25 witness words with compression rank 25 of 32; exhaustive check of 4095 strict block polynomials and 12 shear products; six one-role pair witnesses; complete meet-in-the-middle censuses (1 role length 3; 2 roles lengths 5-7, and 8 with --full) with the four-image span at least 2t on every mixed-label word; failure controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is dim(K1 U + K2 U + Q1 U + Q2 U) >= 2t for every exact mixed positive-Q8 word?", + "why_it_matters": "It implies n>=3t for every mixed shape, so the minima at (4,1) and (7,1) would be 15 and 24.", + "first_step": "Test three-role length-9 words with t=3, then seek a filtration argument using K2=K1+(ij+ji) and Q2=Q1+(ij+ji).", + "blocked_by": "No proof; the census here only reaches t<=2." + }, + { + "question": "Which compression identities exist at degree four and higher?", + "why_it_matters": "Theorem A stops at degree three; a higher identity could restore a cyclic-style argument.", + "first_step": "Build two- and three-role witness sets and explain any rank deficiency before trusting a relation seen only on two-role samples.", + "blocked_by": "Two-role length-8 samples leave a 16-dimensional annihilator at degree five, which may be small-dimension artefacts." + }, + { + "question": "Does an exact 13-call word exist at shape (4,1)?", + "why_it_matters": "It would refute Conjecture D and give the first mixed saving below 3t.", + "first_step": "Restrict to six-role scalar cores (PR3536 half-call core bound) and search the surviving splits (4,9), (6,7), (8,5), (10,3).", + "blocked_by": "Search size far beyond the census here." + } + ] +} diff --git a/research/q8-mixed-shear-identity-space/VERIFY.json b/research/q8-mixed-shear-identity-space/VERIFY.json new file mode 100644 index 0000000000..bfd86d9382 --- /dev/null +++ b/research/q8-mixed-shear-identity-space/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Q8 group law and the eight-element filtration basis; the seven coefficient equations of the degree-three compression calculus; exactness of the 25 witness words and rank 25 of their compression rows (identity space exactly the 7-dimensional equation span); all 4095 strict block polynomials of degree one or two, leaving exactly the shears K1, K2, Q1, Q2, and all 12 degree-at-most-three shear products rejected; six one-role three-call witnesses meeting every pair of shear images; complete meet-in-the-middle censuses at (1 role, length 3) and (2 roles, lengths 5, 6, 7) with the four-image span at least 2t on every mixed-label word. Failure controls reject iii as zj, reject the cyclic (I+L)^2 identity and an altered aaa equation through witness rows, and confirm disjoint K, K^2 images on a homogeneous direct word." + } + ] +} diff --git a/research/q8-mixed-shear-identity-space/WITNESS.json b/research/q8-mixed-shear-identity-space/WITNESS.json new file mode 100644 index 0000000000..42bb6c0fdf --- /dev/null +++ b/research/q8-mixed-shear-identity-space/WITNESS.json @@ -0,0 +1,844 @@ +{ + "description": "Exact mixed positive-Q8 words whose compression rows span the 25-dimensional row space. Calls are [label, u, v] with u, v role bitmasks; call 0 acts first.", + "identity_witnesses": [ + { + "target": [ + "zi" + ], + "calls": [ + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 1 + ] + ] + }, + { + "target": [ + "zi" + ], + "calls": [ + [ + "j", + 1, + 1 + ], + [ + "j", + 1, + 1 + ], + [ + "i", + 1, + 1 + ] + ] + }, + { + "target": [ + "zi" + ], + "calls": [ + [ + "i", + 1, + 1 + ], + [ + "j", + 1, + 1 + ], + [ + "j", + 1, + 1 + ] + ] + }, + { + "target": [ + "zj" + ], + "calls": [ + [ + "j", + 1, + 1 + ], + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 1 + ] + ] + }, + { + "target": [ + "zj" + ], + "calls": [ + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 1 + ], + [ + "j", + 1, + 1 + ] + ] + }, + { + "target": [ + "zj" + ], + "calls": [ + [ + "j", + 1, + 1 + ], + [ + "j", + 1, + 1 + ], + [ + "j", + 1, + 1 + ] + ] + }, + { + "target": [ + "1", + "zi" + ], + "calls": [ + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zi" + ], + "calls": [ + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zi" + ], + "calls": [ + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zi" + ], + "calls": [ + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zi" + ], + "calls": [ + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zi" + ], + "calls": [ + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zj" + ], + "calls": [ + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zj" + ], + "calls": [ + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zj" + ], + "calls": [ + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ] + ] + }, + { + "target": [ + "1", + "zj" + ], + "calls": [ + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ] + ] + }, + { + "target": [ + "zi", + "zi" + ], + "calls": [ + [ + "i", + 3, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 3 + ] + ] + }, + { + "target": [ + "zi", + "zi" + ], + "calls": [ + [ + "i", + 2, + 3 + ], + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 1 + ], + [ + "i", + 3, + 1 + ] + ] + }, + { + "target": [ + "zi", + "zj" + ], + "calls": [ + [ + "i", + 1, + 1 + ], + [ + "j", + 2, + 3 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 1 + ], + [ + "j", + 2, + 3 + ] + ] + }, + { + "target": [ + "zi", + "zj" + ], + "calls": [ + [ + "j", + 2, + 2 + ], + [ + "i", + 1, + 3 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 1, + 1 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 1, + 3 + ] + ] + }, + { + "target": [ + "zj", + "zj" + ], + "calls": [ + [ + "j", + 3, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 1, + 1 + ], + [ + "i", + 1, + 1 + ], + [ + "j", + 1, + 3 + ] + ] + }, + { + "target": [ + "1", + "zi" + ], + "calls": [ + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "i", + 2, + 2 + ] + ] + }, + { + "target": [ + "zi", + "zi" + ], + "calls": [ + [ + "j", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 3, + 2 + ], + [ + "j", + 1, + 3 + ], + [ + "i", + 1, + 3 + ], + [ + "j", + 1, + 3 + ], + [ + "j", + 1, + 1 + ], + [ + "j", + 1, + 1 + ] + ] + }, + { + "target": [ + "zi", + "zi" + ], + "calls": [ + [ + "i", + 2, + 2 + ], + [ + "i", + 3, + 1 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "i", + 2, + 3 + ], + [ + "i", + 3, + 1 + ], + [ + "i", + 3, + 1 + ] + ] + }, + { + "target": [ + "zi", + "zi" + ], + "calls": [ + [ + "i", + 2, + 3 + ], + [ + "i", + 3, + 1 + ], + [ + "j", + 2, + 3 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 2, + 2 + ], + [ + "j", + 1, + 1 + ], + [ + "i", + 2, + 2 + ], + [ + "j", + 3, + 1 + ] + ] + } + ] +} \ No newline at end of file diff --git a/research/q8-mixed-shear-identity-space/verify.py b/research/q8-mixed-shear-identity-space/verify.py new file mode 100644 index 0000000000..4dc91e09ce --- /dev/null +++ b/research/q8-mixed-shear-identity-space/verify.py @@ -0,0 +1,413 @@ +"""Exact identity space of mixed positive-Q8 call-space compressions. + +Standard library only. Prints PASS_Q8_MIXED_SHEAR_IDENTITY_SPACE on success. +""" +import itertools +import json +import pathlib +import sys + +HERE = pathlib.Path(__file__).resolve().parent +UNITS = "1ijk" +UNIT_TABLE = { # (left, right) -> (sign bit, unit) + "11": (0, "1"), "1i": (0, "i"), "1j": (0, "j"), "1k": (0, "k"), + "i1": (0, "i"), "ii": (1, "1"), "ij": (0, "k"), "ik": (1, "j"), + "j1": (0, "j"), "ji": (1, "k"), "jj": (1, "1"), "jk": (0, "i"), + "k1": (0, "k"), "ki": (0, "j"), "kj": (1, "i"), "kk": (1, "1"), +} +ONE, I_EL, J_EL = 1, 1 << 1, 1 << 2 +ZI, ZJ = 1 << 5, 1 << 6 # group elements -i and -j (index 4*sign+unit) +TARGET_CODE = {"zi": ZI, "zj": ZJ, "1": ONE} +LABEL = {"i": I_EL, "j": J_EL} +DEG = 3 # monomials E L E ... L E with at most DEG factors L + + +def check(cond, msg): + if not cond: + raise SystemExit("FAIL: " + msg) + + +def gmul(a, b): + sa, ua = divmod(a, 4) + sb, ub = divmod(b, 4) + s, u = UNIT_TABLE[UNITS[ua] + UNITS[ub]] + return 4 * ((sa + sb + s) % 2) + UNITS.index(u) + + +def amul(x, y): + """Product in F2[Q8]; elements are 8-bit masks over group indices.""" + r = 0 + for a in range(8): + if x >> a & 1: + for b in range(8): + if y >> b & 1: + r ^= 1 << gmul(a, b) + return r + + +ALPHA, BETA = ONE ^ I_EL, ONE ^ J_EL + + +def word_element(w): + r = ONE + for c in w: + r = amul(r, ALPHA if c == "i" else BETA) + return r + + +BASIS_NAMES = ["1", "a", "b", "aa", "ab", "aaa", "aab", "aaab"] +BASIS = [word_element(w) for w in ("", "i", "j", "ii", "ij", "iii", "iij", "iiij")] + + +def coords(x): + for mask in range(256): + y = 0 + for t in range(8): + if mask >> t & 1: + y ^= BASIS[t] + if y == x: + return mask + raise SystemExit("FAIL: element outside basis span") + + +MONS = ["".join(p) for d in range(1, DEG + 2) for p in itertools.product("ij", repeat=d)] +COLS = MONS + ["Pi", "Pj"] +NCOL = len(COLS) + + +def coefficient_equations(): + """Basis coefficient e of the endpoint: sum_w [x_w]_e X M_w Y = [target]_e.""" + eqs = {} + for e in range(1, 8): + c = 0 + for k, m in enumerate(MONS): + if coords(word_element(m)) >> e & 1: + c |= 1 << k + if coords(ZI) >> e & 1: + c |= 1 << len(MONS) + if coords(ZJ) >> e & 1: + c |= 1 << (len(MONS) + 1) + eqs[BASIS_NAMES[e]] = c + return eqs + + +def dot(a, b): + return bin(a & b).count("1") & 1 + + +def endpoint(target_len, calls): + """Exact matrix product D_{n-1}...D_0 over F2[Q8].""" + r = target_len + w = [[ONE if p == q else 0 for q in range(r)] for p in range(r)] + for g, u, v in calls: + check(dot(u, v) == 1, "call is not an idempotent projector") + x = ONE ^ LABEL[g] + new = [row[:] for row in w] + for p in range(r): + if u >> p & 1: + for q in range(r): + acc = 0 + for s in range(r): + if v >> s & 1: + acc ^= w[s][q] + new[p][q] ^= amul(x, acc) + w = new + return w + + +def is_exact(target, calls): + diag = [TARGET_CODE[c] for c in target] + w = endpoint(len(diag), calls) + return all(w[p][q] == (diag[p] if p == q else 0) + for p in range(len(diag)) for q in range(len(diag))) + + +def compression_rows(target, calls): + """One row per active (p,q): bits of (X M Y)_{pq} per monomial, then Pi, Pj.""" + act = [p for p, c in enumerate(target) if c != "1"] + n = len(calls) + labs = [c[0] for c in calls] + ymask = [sum(((calls[l][2] >> q) & 1) << k for k, q in enumerate(act)) for l in range(n)] + chain = {} + for m in sorted(MONS, key=len): + if len(m) == 1: + chain[m] = [ymask[l] if labs[l] == m else 0 for l in range(n)] + continue + sub = chain[m[1:]] + vals = [] + for l in range(n): + x = 0 + if labs[l] == m[0]: + for a in range(l): + if dot(calls[l][2], calls[a][1]): + x ^= sub[a] + vals.append(x) + chain[m] = vals + rows = [] + for p in act: + ent = [0] * len(MONS) + for k, m in enumerate(MONS): + for l in range(n): + if calls[l][1] >> p & 1: + ent[k] ^= chain[m][l] + for kq, q in enumerate(act): + row = sum(((ent[k] >> kq) & 1) << k for k in range(len(MONS))) + if p == q: + row |= 1 << (len(MONS) + (0 if target[p] == "zi" else 1)) + rows.append(row) + return rows + + +def rref(vectors, basis=None): + basis = dict(basis or {}) + for v in vectors: + for piv in sorted(basis, reverse=True): + if v >> piv & 1: + v ^= basis[piv] + if v: + piv = v.bit_length() - 1 + for k in list(basis): + if basis[k] >> piv & 1: + basis[k] ^= v + basis[piv] = v + return basis + + +def in_span(v, basis): + for piv in sorted(basis, reverse=True): + if v >> piv & 1: + v ^= basis[piv] + return v == 0 + + +# ---- polynomials in the label blocks E_a L E_b (sets of label words) ---- +IDENT = frozenset({"i", "j"}) + + +def pmul(p, q): + out = set() + for u in p: + for v in q: + if u[-1] == v[0]: + out ^= {u + v[1:]} + return frozenset(out) + + +def padd(*ps): + out = set() + for p in ps: + out ^= set(p) + return frozenset(out) + + +def pvec(p): + """Compression vector of X p Y, or None if p leaves the degree-DEG calculus.""" + if any(len(w) > DEG + 1 for w in p): + return None + return sum(1 << MONS.index(w) for w in p) + + +def check_identity_space(eqs, witnesses): + rows = [] + for item in witnesses: + check(is_exact(item["target"], item["calls"]), "witness word is not exact") + rows.extend(compression_rows(item["target"], item["calls"])) + for name, c in eqs.items(): + check(all(dot(c, r) == 0 for r in rows), "equation %s fails on a witness" % name) + eq_basis = rref(eqs.values()) + row_basis = rref(rows) + check(len(eq_basis) == 7, "coefficient equations are not independent") + check(len(row_basis) == NCOL - 7, "witness rank is %d" % len(row_basis)) + return eq_basis, rows + + +def shear_classes(eq_basis): + strict = [m for m in MONS if 2 <= len(m) <= 3] + shears = [] + for k in range(1, len(strict) + 1): + for sub in itertools.combinations(strict, k): + h = frozenset(sub) + if in_span(pvec(padd(IDENT, h)), eq_basis): + shears.append(h) + products = 0 + for m1, m2 in itertools.product(shears, repeat=2): + v = pvec(pmul(padd(IDENT, m1), padd(IDENT, m2))) + if v is None: + continue + products += 1 + check(not in_span(v, eq_basis), "a shear product is an identity") + return shears, products + + +def block_matrix(calls, poly): + """Call-space operator for a block polynomial, as row bitmasks.""" + n = len(calls) + labs = [c[0] for c in calls] + lmat = [[dot(calls[l][2], calls[a][1]) if l > a else 0 for a in range(n)] for l in range(n)] + out = [0] * n + for w in poly: + for chain in itertools.combinations(range(n - 1, -1, -1), len(w)): + if all(labs[chain[k]] == w[k] for k in range(len(w))) and \ + all(lmat[chain[k]][chain[k + 1]] for k in range(len(w) - 1)): + out[chain[0]] ^= 1 << chain[-1] + return out + + +def rank(vs): + return len(rref(vs)) + + +def images(target, calls, polys): + act = [p for p, c in enumerate(target) if c != "1"] + n = len(calls) + ucols = [sum(((calls[l][2] >> q) & 1) << l for l in range(n)) for q in act] + xrows = [sum(((calls[l][1] >> p) & 1) << l for l in range(n)) for p in act] + out = {} + for name, poly in polys.items(): + mat = block_matrix(calls, poly) + img = [sum((dot(mat[l], u)) << l for l in range(n)) for u in ucols] + check(rank(img) == len(act), "shear image lost rank") + check(all(dot(x, v) == 0 for x in xrows for v in img), "shear image not in ker X") + out[name] = img + return out + + +# ---- complete meet-in-the-middle census of exact words ---- +def ginv(a): + return next(b for b in range(8) if gmul(a, b) == 0) + + +def call_matrix(r, x, u, v): + return tuple(tuple(x if (u >> p & 1 and v >> q & 1) else 0 for q in range(r)) for p in range(r)) + + +def mat_mul(a, b, r): + out = [] + for p in range(r): + row = [] + for q in range(r): + acc = 0 + for s in range(r): + if a[p][s] and b[s][q]: + acc ^= amul(a[p][s], b[s][q]) + row.append(acc) + out.append(tuple(row)) + return tuple(out) + + +def factor(r, g, u, v, inverse): + elem = 1 << (ginv(LABEL[g].bit_length() - 1) if inverse else LABEL[g].bit_length() - 1) + m = call_matrix(r, ONE ^ elem, u, v) + return tuple(tuple(m[p][q] ^ (ONE if p == q else 0) for q in range(r)) for p in range(r)) + + +def census(r, n1, n2): + """All exact words of length n1+n2 on r roles, every diagonal target in {zi,zj,1}^r.""" + opts = [(g, u, v) for g in "ij" for u in range(1, 1 << r) for v in range(1, 1 << r) if dot(u, v)] + ident = tuple(tuple(ONE if p == q else 0 for q in range(r)) for p in range(r)) + targets = {} + for diag in itertools.product(["zi", "zj", "1"], repeat=r): + if diag.count("1") == r: + continue + targets[diag] = tuple(tuple(TARGET_CODE[diag[p]] if p == q else 0 for q in range(r)) + for p in range(r)) + tabs = {d: {} for d in targets} + for w in itertools.product(opts, repeat=n1): + pinv = ident + for g, u, v in w: # D_0^-1 D_1^-1 ... D_{n1-1}^-1 + pinv = mat_mul(pinv, factor(r, g, u, v, True), r) + for d, t in targets.items(): + tabs[d].setdefault(mat_mul(t, pinv, r), []).append(w) + found = {d: [] for d in targets} + for w2 in itertools.product(opts, repeat=n2): + s2 = ident + for g, u, v in w2: + s2 = mat_mul(factor(r, g, u, v, False), s2, r) + for d in targets: + for w1 in tabs[d].get(s2, []): + found[d].append(list(w1 + w2)) + return found + + +SHEARS = { + "K1": padd(IDENT, {"ii", "ji", "jj"}), + "K2": padd(IDENT, {"ii", "ij", "jj"}), + "Q1": padd(IDENT, {"iii", "iij", "ijj", "jii", "jji", "jjj"}), + "Q2": padd(IDENT, {"ij", "ji", "iii", "iij", "ijj", "jii", "jji", "jjj"}), +} + + +def four_span_census(cases): + report = [] + for r, n1, n2 in cases: + found = census(r, n1, n2) + total = mixed = 0 + excess = {} + for d, ws in found.items(): + for w in ws: + check(is_exact(list(d), w), "census word is not exact") + total += 1 + if len({c[0] for c in w}) < 2: + continue + mixed += 1 + img = images(list(d), w, SHEARS) + e = rank(sum(img.values(), [])) - 2 * (r - list(d).count("1")) + check(e >= 0, "four shear images span less than 2t") + excess[e] = excess.get(e, 0) + 1 + report.append({"roles": r, "length": n1 + n2, "exact_words": total, + "mixed_label_words": mixed, "span_minus_2t": dict(sorted(excess.items()))}) + return report + + +def pair_witnesses(): + """Every pair of shear images meets on some exact one-role three-call word.""" + out = {} + for labs in itertools.product("ij", repeat=3): + calls = [[g, 1, 1] for g in labs] + for tgt in ("zi", "zj"): + if not is_exact([tgt], calls) or len(set(labs)) < 2: + continue + img = images([tgt], calls, SHEARS) + for a, b in itertools.combinations(sorted(SHEARS), 2): + if rank(img[a] + img[b]) < 2 and (a + "," + b) not in out: + out[a + "," + b] = {"target": tgt, "labels": "".join(labs)} + check(len(out) == 6, "some shear pair is disjoint on every three-call word") + return out + + +def controls(eqs, eq_basis, rows): + check(not is_exact(["zj"], [["i", 1, 1]] * 3), "control: iii accepted as zj") + check(is_exact(["zi"], [["i", 1, 1]] * 3), "control: direct iii rejected") + cyclic_k2 = pvec(padd(IDENT, {"".join(w) for w in itertools.product("ij", repeat=3)})) + check(not in_span(cyclic_k2, eq_basis), "control: cyclic K^2 identity entered the span") + check(any(dot(cyclic_k2, r) for r in rows), "control: cyclic K^2 identity not refuted") + broken = eqs["aaa"] ^ (1 << MONS.index("iji")) + check(any(dot(broken, r) for r in rows), "control: altered aaa equation not refuted") + homog = images(["zi", "zi"], [["i", 1, 1]] * 3 + [["i", 2, 2]] * 3, SHEARS) + check(rank(homog["K1"] + homog["Q1"]) == 4, "control: homogeneous K, K^2 images meet") + + +def main(argv): + full = "--full" in argv + eqs = coefficient_equations() + witnesses = json.loads((HERE / "WITNESS.json").read_text())["identity_witnesses"] + eq_basis, rows = check_identity_space(eqs, witnesses) + shears, products = shear_classes(eq_basis) + check(sorted(map(sorted, shears)) == sorted(sorted(p - IDENT) for p in SHEARS.values()), + "shear classification differs") + pairs = pair_witnesses() + controls(eqs, eq_basis, rows) + cases = [(1, 1, 2), (2, 2, 3), (2, 3, 3), (2, 3, 4)] + ([(2, 4, 4)] if full else []) + report = four_span_census(cases) + result = { + "monomial_columns": NCOL, "witness_rank": NCOL - 7, "identity_space_dim": 7, + "equations": {k: " + ".join(COLS[i] for i in range(NCOL) if c >> i & 1) for k, c in eqs.items()}, + "shears": {k: sorted(v - IDENT, key=lambda w: (len(w), w)) for k, v in SHEARS.items()}, + "shear_products_checked": products, "pair_witnesses": pairs, "census": report, + } + print(json.dumps(result, indent=1, sort_keys=True)) + print("PASS_Q8_MIXED_SHEAR_IDENTITY_SPACE") + + +if __name__ == "__main__": + main(sys.argv[1:])