Attain the mixed-negative Q8 bound for t <= 2

research/q8-min-length-census/PROOF.md

@@ -0,0 +1,113 @@
+# Attainment of the mixed-negative Q8 bound for t <= 2
+
+## Model
+
+Unchanged from PR3570/PR3578/PR3589. Work in the full formal group algebra
+`R = F2[Q8]` with distinct elements `1` and `z` and relations
+
+```text
+i^2 = j^2 = z,   z^2 = 1,   ji = z ij.
+```
+
+Every role carries independent arbitrary dirty input. Binary scalar `GL`
+mixing is free. A **paid factor** is
+
+```text
+D_l = I + (1 + [g_l]) u_l v_l^T,     g_l in {i, j},     v_l^T u_l = 1.
+```
+
+A **word** is an ordered sequence of paid factors acting on a `roles x roles`
+matrix over `R`. The **endpoint** is diagonal, with `t_i` copies of `zi`,
+`t_j` copies of `zj` and the identity on every other role. Write `t = t_i + t_j`
+and `n` for the number of paid factors. Any finite restored dirty workspace is
+permitted.
+
+## Inherited lower bound and parity
+
+PR3589 proves, for every exact word,
+
+```text
+2n + n_i >= 6t - t_i,        2n + n_j >= 6t - t_j,        hence 5n >= 11t.
+```
+
+It also records the inherited trace parity
+
+```text
+n_i = t_i mod 2,   n_j = t_j mod 2,   hence n = t mod 2.
+```
+
+These are **necessary** conditions. Neither is re-proved here.
+
+## Statement
+
+**Theorem.** For every mixed-negative endpoint with `t = 1` or `t = 2`, the
+minimum number of paid factors over all role counts and all finite restored
+dirty workspace is
+
+```text
+t = 1: 3        t = 2: 6.
+```
+
+**Proof.** Lower bound: PR3589 gives `5n >= 11t`. For `t = 1` this is
+`n >= 11/5`, so `n >= 3` with no parity input needed. For `t = 2` it is
+`n >= 22/5`, so `n >= 5`; the parity `n = t mod 2` then forces `n >= 6`. These
+exclusions hold at every role count, because both premises of PR3589 are
+role-free.
+
+Upper bound: let `spine(g, a)` be the three paid factors with
+`u = v = e_a` and label `g`. Because `u = v = e_a` has `v^T u = 1`, the factor
+is legal. On the `a`-th role it acts as `I + (1 + [g])`, which multiplies that
+role by `[g]`; on every other role it is the identity. Hence
+
+```text
+spine(g, a) applied three times  multiplies role a by g^3.
+```
+
+Direct computation in `R` gives `i^3 = zi`, `j^3 = zj` and `z^2 = 1`. For a
+target list of length `t`, applying `spine` on the corresponding label to each
+target role in turn gives the exact diagonal endpoint in `3t` calls. For
+`t = 1` that is `3` and for `t = 2` that is `6`, matching the lower bound. ∎
+
+The minimum is therefore attained, and for `t <= 2` the parity-rounded
+`11t/5` constant cannot be improved.
+
+## Sharpness consequences
+
+- **The constant is sharp at `t = 1` and `t = 2`.** Any strictly stronger
+  necessary function of `t` fails at these two points. This answers PR3589's
+  open question "Is the uniform `11t/5` constant sharp?" in the affirmative for
+  `t <= 2` only.
+- **The bound is not attained for `t >= 3` by the witness family.**
+  `t = 3` admits bound value `7` against a `9`-call witness; `t = 4` balanced
+  admits `10` against a `12`-call witness. The minima stay in `{7,9}` and
+  `{10,12}`.
+
+## Independent finite cross-check
+
+The five complete breadth-first searches in `verify.py` enumerate **every**
+word on one and two roles up to lengths `2` and `5`, and find none reaching the
+corresponding endpoint. State counts are `6`, `6` and `56,084`. Because the
+theoretical lower bound is role-free, these receipts are an independent check
+of the model implementation and of the witnesses, not the source of the
+exclusion.
+
+The verifier also checks all `64` Q8 group products against an independent
+signed-unit table, so the group law used by the witnesses is not assumed from
+the product routine it is meant to test.
+
+## What is not claimed
+
+Nothing here excludes a shorter word at `t >= 3`, decides the `t = 3` or
+balanced `t = 4` minima, re-proves PR3589, supplies a physical implementation
+or invoice, or improves the selected kappa `0.001672660197076918`. The
+ten-call balanced four-target question remains open. A randomised search over
+`4` to `8` roles is recorded in VALIDATION.md as a **search failure**: its
+failure to find a word proves nothing.
+
+## Credit
+
+Nick Petalas/PR3589 supplies the bound and the parity; PR3570 the mixed cubic
+identity; PR3578 the two-orientation boundary-rank method; PR3536 the
+sign-sensitive quadratic chronology; PR3558 the cyclic subspace argument. Only
+the witnesses, the complete small-case census and the sharpness consequence
+are new here.

research/q8-min-length-census/README.md

@@ -0,0 +1,102 @@
+# Minimum paid-call counts for small mixed-negative Q8 endpoints
+
+## Result
+
+In the mixed-negative Q8 bit-register model of PR3570/PR3578/PR3589, the
+minimum number of paid rank-one calls realizing a diagonal endpoint is
+**exactly** the parity-rounded uniform bound of PR3589 once `t <= 2`.
+
+```text
+PR3589 lower bound:   5n >= 11t,        inherited parity:  n = t mod 2
+                      n >= ceil(11t/5) rounded up to a parity t value
+
+t = 1   (zi)          minimum 3   attained
+t = 1   (zj)          minimum 3   attained
+t = 2   (zi, zi)      minimum 6   attained
+t = 2   (zi, zj)      minimum 6   attained
+t = 2   (zj, zj)      minimum 6   attained
+```
+
+Each minimum is attained by an explicit word. Three calls on one role
+multiply that role by the cube of its label, and `i^3 = zi`, `j^3 = zj`, so
+the witnesses are the `3t`-call disjoint construction, which happens to sit
+exactly on the bound for `t = 1, 2`.
+
+Two consequences.
+
+- **The uniform constant is sharp in the sense PR3589 left open.** No strictly
+  stronger function of `t` can hold at `t = 1` or `t = 2`, because the bound
+  is met there. This settles open question 2 of that package for `t <= 2`.
+- **The bound is not attained for `t >= 3` by these witnesses.**
+  `t = 3` admits the bound value `7` but the best witness here has `9` calls;
+  `t = 4` balanced admits `10` and the best witness has `12`. Those minima
+  remain `{7,9}` and `{10,12}` respectively, exactly as PR3589 left them.
+
+This is a mathematical side result for the nonabelian bit-register model. It
+does **not** claim a new kappa, a physical supplier, an improved selected
+result, or a complete multiplication theorem. The selected frontier is
+unchanged.
+
+## Reproduce
+
+Use CPython 3.12 from a repository root:
+
+```sh
+python3.12 -Werror -B scripts/research_package.py --package research/q8-min-length-census
+```
+
+Direct scientific and control replay also work without Git or network:
+
+```sh
+python3.12 -I -Werror -B research/q8-min-length-census/verify.py
+python3.12 -I -O -Werror -B research/q8-min-length-census/verify.py
+python3.12 -I -O -Werror -B research/q8-min-length-census/test_package.py
+```
+
+The package is self-contained: standard library only, no Git objects, no
+network, no third-party dependency. `RESULT.json` is the exact finite
+receipt; [VALIDATION.md](VALIDATION.md) states coverage and limits.
+
+## Evidence
+
+- All 64 Q8 products agree between an independent signed-unit table and the
+  basis product, and `i^3 = zi`, `j^3 = zj`, `z^2 = 1` are checked directly.
+- Eight explicit witnesses are replayed to their exact diagonal endpoints.
+- Five **complete** breadth-first searches exhaust every word on 1 and 2 roles
+  up to the lengths `2` and `5`, over `7` and `56,084` distinct states
+  respectively, and find none. These are a cross-check: for `t <= 2` the
+  PR3589 bound plus parity already excludes every shorter length at *every*
+  role count, so the census is not the source of the lower bound.
+
+## Sources and limits
+
+The model, the notation and the `5n >= 11t` bound are inherited unchanged from
+Nick Petalas/PR3570, PR3578 and PR3589. No predecessor mathematics is
+re-derived here; this package supplies attainment witnesses and a complete
+small-case census.
+
+Full group-algebra finite fields, longer-word classification, the sharp
+constant for `t >= 3`, physical execution, scalar/routing/restoration/
+hosting/precision costs, a complete supplier, an improved kappa, independent
+human review and formal proof-kernel acceptance are all **out of scope and
+unrun**. A randomised search for a ten-call balanced four-target word is
+recorded in [VALIDATION.md](VALIDATION.md) as a **search failure only**; it is
+not an exclusion and not evidence of novelty.
+
+## Open next questions
+
+- Is the balanced four-target minimum ten or twelve? PR3589's bound admits
+  ten and no witness below twelve is known. A complete bounded census, not a
+  randomised search, would decide it.
+- Is the `t = 3` minimum seven or nine? This is the smallest case where the
+  parity-rounded bound is not already attained by the `3t` construction.
+- What is the sharp uniform constant for `t >= 3`? Attainment at `t <= 2`
+  does not settle this.
+
+## Credit
+
+Nick Petalas/PR3589 for the mixed-negative boundary-rank bound, with
+PR3570/PR3578 for the cubic identities and the two-orientation method,
+PR3536 for the sign-sensitive chronology and PR3558 for the cyclic subspace
+argument. Their retained lineage includes Tuafo/PR2900, ywz65/PR2587,
+Aaron Wang/PR2318, Cinna Davis and steph4n-gh.

research/q8-min-length-census/RESULT.json

@@ -0,0 +1,175 @@
+{
+ "algebra": {
+  "i3_zi": true,
+  "j3_zj": true,
+  "q8_products": 64
+ },
+ "census": {
+  "t1-zi": {
+   "cap_reached": false,
+   "exhausted": true,
+   "roles": 1,
+   "searched_length": null,
+   "states": 6,
+   "targets": [
+    32
+   ],
+   "witness": null
+  },
+  "t1-zj": {
+   "cap_reached": false,
+   "exhausted": true,
+   "roles": 1,
+   "searched_length": null,
+   "states": 6,
+   "targets": [
+    64
+   ],
+   "witness": null
+  },
+  "t2-zi-zi": {
+   "cap_reached": false,
+   "exhausted": true,
+   "roles": 2,
+   "searched_length": null,
+   "states": 56084,
+   "targets": [
+    32,
+    32
+   ],
+   "witness": null
+  },
+  "t2-zi-zj": {
+   "cap_reached": false,
+   "exhausted": true,
+   "roles": 2,
+   "searched_length": null,
+   "states": 56084,
+   "targets": [
+    32,
+    64
+   ],
+   "witness": null
+  },
+  "t2-zj-zj": {
+   "cap_reached": false,
+   "exhausted": true,
+   "roles": 2,
+   "searched_length": null,
+   "states": 56084,
+   "targets": [
+    64,
+    64
+   ],
+   "witness": null
+  }
+ },
+ "witnesses": {
+  "t1-zi": {
+   "attains_parity_bound": true,
+   "calls": 3,
+   "parity_bound": 3,
+   "roles": 1,
+   "t": 1,
+   "t_i": 1,
+   "t_j": 0,
+   "targets": [
+    32
+   ]
+  },
+  "t1-zj": {
+   "attains_parity_bound": true,
+   "calls": 3,
+   "parity_bound": 3,
+   "roles": 1,
+   "t": 1,
+   "t_i": 0,
+   "t_j": 1,
+   "targets": [
+    64
+   ]
+  },
+  "t2-zi-zi": {
+   "attains_parity_bound": true,
+   "calls": 6,
+   "parity_bound": 6,
+   "roles": 2,
+   "t": 2,
+   "t_i": 2,
+   "t_j": 0,
+   "targets": [
+    32,
+    32
+   ]
+  },
+  "t2-zi-zj": {
+   "attains_parity_bound": true,
+   "calls": 6,
+   "parity_bound": 6,
+   "roles": 2,
+   "t": 2,
+   "t_i": 1,
+   "t_j": 1,
+   "targets": [
+    32,
+    64
+   ]
+  },
+  "t2-zj-zj": {
+   "attains_parity_bound": true,
+   "calls": 6,
+   "parity_bound": 6,
+   "roles": 2,
+   "t": 2,
+   "t_i": 0,
+   "t_j": 2,
+   "targets": [
+    64,
+    64
+   ]
+  },
+  "t3-zi-zi-zi": {
+   "attains_parity_bound": false,
+   "calls": 9,
+   "parity_bound": 7,
+   "roles": 3,
+   "t": 3,
+   "t_i": 3,
+   "t_j": 0,
+   "targets": [
+    32,
+    32,
+    32
+   ]
+  },
+  "t3-zi-zi-zj": {
+   "attains_parity_bound": false,
+   "calls": 9,
+   "parity_bound": 7,
+   "roles": 3,
+   "t": 3,
+   "t_i": 2,
+   "t_j": 1,
+   "targets": [
+    32,
+    32,
+    64
+   ]
+  },
+  "t4-balanced": {
+   "attains_parity_bound": false,
+   "calls": 12,
+   "parity_bound": 10,
+   "roles": 4,
+   "t": 4,
+   "t_i": 2,
+   "t_j": 2,
+   "targets": [
+    32,
+    32,
+    64,
+    64
+   ]
+  }
+ }
+}