From 8a1000c09819b43ca9a8f2929788af4af40dab70 Mon Sep 17 00:00:00 2001 From: steph4n-gh <284007938+steph4n-gh@users.noreply.github.com> Date: Thu, 15 Oct 2026 20:27:09 -0400 Subject: [PATCH] research: exclude 15-call five-b UT4 splits across dirty workspaces --- research/ut4-fifteen-call-five-b/PROOF.md | 331 +++++++ research/ut4-fifteen-call-five-b/README.md | 151 +++ research/ut4-fifteen-call-five-b/RESULT.json | 861 ++++++++++++++++++ research/ut4-fifteen-call-five-b/SOURCES.json | 198 ++++ research/ut4-fifteen-call-five-b/TASK.json | 158 ++++ research/ut4-fifteen-call-five-b/VERIFY.json | 38 + research/ut4-fifteen-call-five-b/census.py | 775 ++++++++++++++++ research/ut4-fifteen-call-five-b/controls.py | 368 ++++++++ .../vendor/predecessor.py | 348 +++++++ research/ut4-fifteen-call-five-b/verify.py | 99 ++ 10 files changed, 3327 insertions(+) create mode 100644 research/ut4-fifteen-call-five-b/PROOF.md create mode 100644 research/ut4-fifteen-call-five-b/README.md create mode 100644 research/ut4-fifteen-call-five-b/RESULT.json create mode 100644 research/ut4-fifteen-call-five-b/SOURCES.json create mode 100644 research/ut4-fifteen-call-five-b/TASK.json create mode 100644 research/ut4-fifteen-call-five-b/VERIFY.json create mode 100644 research/ut4-fifteen-call-five-b/census.py create mode 100644 research/ut4-fifteen-call-five-b/controls.py create mode 100644 research/ut4-fifteen-call-five-b/vendor/predecessor.py create mode 100644 research/ut4-fifteen-call-five-b/verify.py diff --git a/research/ut4-fifteen-call-five-b/PROOF.md b/research/ut4-fifteen-call-five-b/PROOF.md new file mode 100644 index 0000000000..6779697709 --- /dev/null +++ b/research/ut4-fifteen-call-five-b/PROOF.md @@ -0,0 +1,331 @@ +# Complete 15-call five-b exclusion and the beta <= 3 min(alpha, gamma) price cone + +In the formal group-algebra register model over `R = F2[UT4(F2)]`, no fifteen-call +word with five `b` calls realizes `diag([z], [uz], I_rest)` on any finite number +`r >= 2` of arbitrary restored dirty roles. Every fifteen-call word therefore has +`n_b >= 6`, and every word with `n_b = 5` requires at least eleven outer (`a`/`c`) +calls (`n_a + n_c >= 11`, total length `L >= 16`). Consequently, the direct +fourteen-call `(4, 6, 4)` word is globally optimal on the expanded nonnegative +letter-price cone `beta <= 3 min(alpha, gamma)`, and at `(alpha, beta, gamma) = (1, 3, 1)` +cost `25` is impossible and `26` is the exact minimum. + +This package resolves the explicit 15-call `(1, 3, 1)` handoff formulated by +Gareth Davidson (`@bitplane`) in [PR #2314](https://github.com/CrocSwap/integer-mult-bounds/pull/2314) +(`research/ut4-mixed-weighted-boundary`) and [PR #2343](https://github.com/CrocSwap/integer-mult-bounds/pull/2343) +(`research/register-pairing-compression`), building on Nick Petalas's (`@petalas`) +[PR #2175](https://github.com/CrocSwap/integer-mult-bounds/pull/2175) +(`research/ut4-mixed-central-middle`). The quotient, span-excess, and profile-screen +infrastructure retains its full predecessor attribution to Gareth Davidson (PR #2027, +PR #2314, PR #2343), Nick Petalas (PR #2175), ToikY (PR #1662, PR #1680), +CinnaDavis / `1337isnot1337` (PR #1541), and Aaron Wang / `@navinor` (PR #1690). + +## 1. Formal model and inherited premises + +Let `G = UT4(F2)` and `R = F2[G]` with elementary generators and target elements + +``` +a = I + E12, b = I + E23, c = I + E34, +u = I + E13, z = I + E14. +``` + +On any finite number `r >= 2` of scalar roles `E = H direct-sum K` (`dim H = 2` +active roles and `dim K = r - 2` dirty roles), each paid call has the form +`D_N(g) = I + ([g] + 1) N` with `g in {a, b, c}` and `N = x y^T` a nonzero binary +rank-one matrix over `F2`. Both idempotent (`y^T x = 1`) and nilpotent (`y^T x = 0`) +couplings are permitted. Every occurrence of a generator call, including restoration, +is charged; invertible `GL_r(F2)` basis changes are free and normalized into the +couplings so that the target endpoint is `W = diag([z], [uz], I_K)` in `Mat_r(R)`. + +We use the retained 17-dimensional quotient algebra + +``` +Q = F2 / (A^2, B^2, C^2, AC - CA, all monomials of degree >= 4), +``` + +under the unital homomorphism `a, b, c |-> 1 + A, 1 + B, 1 + C`. In `Q`, + +``` +[u] |-> 1 + AB + BA + ABA + BAB, +[z] |-> 1 + ABC + ACB + BAC + CBA. +``` + +Writing `P = diag(1, 1, 0, ...)` and `S = diag(0, 1, 0, ...)`, the image of +`diag([z], [uz], I_K)` in `Mat_r(Q)` has coefficient `I_r` at `1`, `S` at +`AB, BA, ABA, BAB`, `P` at `ABC, ACB, BAC, CBA`, and `0` on the remaining eight +basis monomials `A, B, C, AC, BC, CB, BCB, CBC`. + +For each label `g in {a, b, c}`, let `X_g = span{x_j : g_j = g} <= E` and +`Y_g = span{y_j^T : g_j = g} <= E*`. By the retained span-containment and +mixed-middle rank inequalities (PR #2027, PR #2175, PR #2314, PR #2343), every +realizing word of length `L = n_a + n_b + n_c` on any finite `r >= 2` satisfies: + +1. `H <= X_g` and `H* <= Y_g` for all `g in {a, b, c}` (so `dim X_g = 2 + e_g^x` + and `dim Y_g = 2 + e_g^y` with integer excesses `e_g^x, e_g^y >= 0`); +2. `n_a >= 4 + e_a^x + e_a^y`, `n_c >= 4 + e_c^x + e_c^y`, and + `n_b >= 5 + e_b^x + e_b^y`; +3. `sum_{g in {a,b,c}} (e_g^x + e_g^y) <= L - 13`; +4. By PR #2175 and PR #2314, no word of length `L <= 14` with `n_b = 5` exists on + any finite number of roles `r >= 2` (splits `(4, 5, 4)`, `(5, 5, 4)`, and `(4, 5, 5)` + are completely excluded). +5. By PR #2343, any 15-call word with `n_b = 5` has count split `(6, 5, 4)`, + `(5, 5, 5)`, or `(4, 5, 6)`, satisfies `e_b^x = e_b^y = 0` (so every `b` call + is supported exclusively on `H x H`), and compresses via dirty-pairing + factorization `W' = diag(I_H, F) W diag(I_H, G)` to at most `r <= 3` roles + with exact letter counts `(n_a, n_b, n_c)` preserved (since deleting any + zero-projected factor would yield a five-`b` word of length `<= 14`, + contradicting premise 4). + +## 2. Two-role compression for (6, 5, 4) and (4, 5, 6) + +**Lemma 1 (Nilpotent same-label dirty compression).** *Every realizing word with +count split `(6, 5, 4)` or `(4, 5, 6)` on any finite number `r >= 2` of restored +dirty roles projects directly onto the two active roles `H` (`r = 2`) with all +fifteen couplings remaining nonzero rank-one `2 x 2` matrices.* + +*Proof.* Consider `(6, 5, 4)` (the case `(4, 5, 6)` follows identically by +interchanging `a` and `c`). From `n_b = 5 >= 5 + e_b^x + e_b^y` and +`n_c = 4 >= 4 + e_c^x + e_c^y`, we have + +``` +e_b^x = e_b^y = e_c^x = e_c^y = 0. +``` + +Thus `X_b = X_c = H` and `Y_b = Y_c = H*`, so every `b` call and every `c` call +has zero dirty column component (`u_j = 0`) and zero dirty row component (`v_j = 0`). +Only `a` calls can have nonzero `u_j` or `v_j`. + +Expand the full product `W = prod_{j=1..15} (I + lambda_j x_j y_j^T)` in `Mat_r(R)`, +where `lambda_j = [g_j] + 1 in R`. For any nonempty index subsequence `i_1 < ... < i_s`, +the corresponding product term is + +``` +lambda_{i_1} ... lambda_{i_s} x_{i_1} (y_{i_1}^T x_{i_2}) ... (y_{i_{s-1}}^T x_{i_s}) y_{i_s}^T. +``` + +Write `x_j = (tilde_x_j, u_j)` and `y_j^T = (tilde_y_j^T, v_j)` with respect to +`E = H direct-sum K`. Each interior scalar contraction splits over `F2` as + +``` +y_{i_m}^T x_{i_{m+1}} = tilde_y_{i_m}^T tilde_x_{i_{m+1}} + v_{i_m}(u_{i_{m+1}}). +``` + +Whenever `v_{i_m}(u_{i_{m+1}}) != 0`, both `v_{i_m}` and `u_{i_{m+1}}` must be +nonzero, which forces both factors `i_m` and `i_{m+1}` to be `a` calls. Then +`lambda_{i_m} = lambda_{i_{m+1}} = [a] + 1`. Because `a^2 = I` in `UT4(F2)`, +`([a] + 1)^2 = [a^2] + 1 = 0` in the full group algebra `R = F2[UT4(F2)]`, so the +ordered coefficient product `lambda_{i_1} ... lambda_{i_s}` contains the adjacent +square `([a] + 1)^2 = 0` and vanishes identically in `R`. + +Consequently, replacing every `x_j, y_j` by its active projection `tilde_x_j, tilde_y_j` +leaves every surviving interior contraction and the entire upper-left `2 x 2` +active block `P W P^T = diag([z], [uz])` unchanged in `Mat_2(R)`. No projected +coupling `tilde_N_j = tilde_x_j tilde_y_j^T` can vanish, because deleting an +identity factor would produce a two-role realizing word of length `<= 14` with +`n_b = 5`, which is impossible by PR #2175 and PR #2314. [] + +## 3. Three-role structure for (5, 5, 5) + +For `(5, 5, 5)`, `n_b = 5` forces `e_b^x = e_b^y = 0`, while `n_a = 5` and `n_c = 5` +give `e_a^x + e_a^y <= 1` and `e_c^x + e_c^y <= 1`. + +- If `e_a^x + e_c^x = 0`, then `u_j = 0` for all 15 factors (`P N_j = N_j`). +- If `e_a^y + e_c^y = 0`, then `v_j = 0` for all 15 factors (`N_j P = N_j`). +- If `e_a^x + e_a^y = 0` or `e_c^x + e_c^y = 0`, only one outer label has dirty + support, and Lemma 1 applies. + +In all those cases, active-corner projection compresses the word directly to two +roles (`r = 2`). The only remaining excess profiles are the two opposite-orientation +three-role cases (`E = H direct-sum K` with `dim K = 1`): + +- **Case I (`(e_a^x, e_a^y, e_c^x, e_c^y) = (1, 0, 0, 1)`):** `v_a = 0`, + `u_b = v_b = 0`, `u_c = 0`. In `3 x 3` block form on `H direct-sum K`: + ``` + N_a = [ tilde_N_a 0 ], N_b = [ N_b 0 ], N_c = [ tilde_N_c x_c d_c ] + [ d_a y_a^T 0 ] [ 0 0 ] [ 0 0 ] + ``` + with `tilde_N_a = x_a y_a^T`, `tilde_N_c = x_c y_c^T`, `d_a, d_c in F2`. +- **Case II (`(e_a^x, e_a^y, e_c^x, e_c^y) = (0, 1, 1, 0)`):** `u_a = 0`, + `u_b = v_b = 0`, `v_c = 0`, the transpose block pattern: + ``` + N_a = [ tilde_N_a x_a d_a ], N_b = [ N_b 0 ], N_c = [ tilde_N_c 0 ] + [ 0 0 ] [ 0 0 ] [ d_c y_c^T 0 ] + ``` + +**Lemma 2 (Exact 3-role quotient equations for `(5, 5, 5)`).** *In `Mat_3(Q)`, any +realizing `(5, 5, 5)` word in Case I or Case II satisfies the following exact +necessary conditions:* + +1. **Active-block decoupling outside `{AC, ACB, BAC}`:** *Every interior dirty + contraction `v_{i_m}(u_{i_{m+1}}) != 0` requires `(g_{i_m}, g_{i_{m+1}}) = (c, a)` + in Case I and `(a, c)` in Case II. Thus any subsequence contributing a dirty + interior contraction has adjacent `A` and `C` in its quotient monomial, which + can only belong to `{AC, ACB, BAC}` in `Q` (since `A^2 = C^2 = ACA = CAC = 0` + and degree `>= 4` vanishes). All 14 remaining basis monomials of `Q` (`1, A, B, C, + AB, BA, BC, CB, ABA, ABC, BAB, BCB, CBA, CBC`) on `W_HH` are identical to the + two-role quotient of the projected word `(tilde_N_a, N_b, tilde_N_c)`.* +2. **Active rank-sum and compatible profile restriction:** *On `W_HH`, the first-degree + equations give `sum tilde_N_a = sum N_b = sum tilde_N_c = 0`. Every `a` or `c` + call has `rank(tilde_N) in {0, 1}` (with `tilde_N = 0` only when the call is a + pure-dirty rank-one coupling `e_K y^T` or `x e_K^T`). Because the 14 non-adjacent-`{A,C}` + equations on `W_HH` match the 2-role quotient, the active prefix sums + `tilde_P_a, tilde_P_c in Mat_2(F2)^5` at the five `b` calls must belong to the + exact `5,664` compatible `(5, 5, 5)` profile pairs. In particular, every + compatible profile `P` has `sum_{g=0..5} rank(P_{g+1} + P_g) >= 4`, so at most + one `a` call has `tilde_N_a = 0` and at most one `c` call has `tilde_N_c = 0`.* +3. **Homogeneous off-diagonal `(K, H)` and `(H, K)` equations:** *No subsequence + of degree `<= 3` starting at `K` and ending at `H` (or starting at `H` and + ending at `K`) can visit `K` twice without containing `ACA = 0`, `CAC = 0`, or + degree `>= 4`. Hence `W_KH` and `W_HK` receive zero dirty interior contractions. + Letting `r_{a,j} = sum_{t < b_j} d_{a,t} y_{a,t}^T` and `q_{c,j} = sum_{t > b_j} x_{c,t} d_{c,t}` + in Case I (with `sum d_a y_a^T = 0` and `sum x_c d_c = 0` from `W_KH|_A = 0` + and `W_HK|_C = 0`), the off-diagonal blocks `W_KH = 0` and `W_HK = 0` enforce:* + - *Case I:* + ``` + sum_{j=1..5} r_{a,j} N_{b,j} = 0 (W_KH at AB), + sum_{j=1..5} r_{a,j} N_{b,j} tilde_P_{a,j} = 0 (W_KH at ABA), + sum_{j=1..5} r_{a,j} N_{b,j} tilde_P_{c,j} = 0 (W_KH at ABC), + sum_{j=1..5} N_{b,j} q_{c,j} = 0 (W_HK at BC), + sum_{j=1..5} tilde_P_{c,j} N_{b,j} q_{c,j} = 0 (W_HK at CBC), + sum_{j=1..5} tilde_P_{a,j} N_{b,j} q_{c,j} = 0 (W_HK at CBA). + ``` + - *Case II (transpose orientation, with `q_{a,j} = sum_{t < b_j} x_{a,t} d_{a,t}` + and `r_{c,j} = sum_{t > b_j} d_{c,t} y_{c,t}^T`):* + ``` + sum_{j=1..5} N_{b,j} q_{a,j} = 0 (W_HK at BA), + sum_{j=1..5} tilde_P_{a,j} N_{b,j} q_{a,j} = 0 (W_HK at ABA), + sum_{j=1..5} tilde_P_{c,j} N_{b,j} q_{a,j} = 0 (W_HK at CBA), + sum_{j=1..5} r_{c,j} N_{b,j} = 0 (W_KH at CB), + sum_{j=1..5} r_{c,j} N_{b,j} tilde_P_{c,j} = 0 (W_KH at CBC), + sum_{j=1..5} r_{c,j} N_{b,j} tilde_P_{a,j} = 0 (W_KH at ABC). + ``` +4. **Cross-role correction on `W_HH` at `{AC, ACB, BAC}`:** *On `W_HH`, the + coefficients of `AC`, `ACB`, and `BAC` equal their two-role active values + plus the rank-one dirty contractions across ordered pairs `(c_i < a_k)` in + Case I (where `CA = AC` in `Q` contributes `x_{c,i} d_{c,i} d_{a,k} y_{a,k}^T`) + or ordered pairs `(a_i < c_k)` in Case II (contributing `x_{a,i} d_{a,i} d_{c,k} y_{c,k}^T`), + multiplied on the right by `N_{b,j}` for `j > max(i, k)` in `ACB` and on the + left by `N_{b,j}` for `j < min(i, k)` in `BAC`.* + +## 4. Profile rank-sum characterization and complete censuses + +**Lemma 3 (5-gap profile rank-sum characterization).** *Let `P = (P_1, ..., P_5) in Mat_2(F2)^5` +be a 5-gap prefix profile with gap increments `S_g = P_{g+1} + P_g` for `g = 0, ..., 5` +(`P_0 = P_6 = 0`). Each `S_g in Mat_2(F2)` has rank `r_g in {0, 1, 2}` (`1` matrix +of rank `0`, `9` of rank `1`, and `6` of rank `2`), and can be written as a sum +of `k_g` nonzero rank-one matrices in `COUPLINGS` if and only if `k_g >= r_g` and +`(r_g, k_g) != (0, 1)`. Consequently, `P` is realizable by `n in {4, 5, 6}` nonzero +rank-one couplings distributed across the six gaps if and only if* + +``` +sum_{g=0..5} rank(S_g) <= n. +``` + +*(Any slack `n - sum rank(S_g) != 1` is absorbed by adding paired rank-one calls +`R + R = 0`, and if `n - sum rank(S_g) = 1`, at least one gap has `r_g >= 1` because +`n >= 4` and `r_g = 0` for all `g` has sum `0`, so a rank-one increment `R` can +be replaced by a 2-call sum `R_1 + R_2 = R` of two distinct rank-one matrices in +the same row or column space).* + +Across all `16^5 = 1,048,576` profiles in `Mat_2(F2)^5`, the exact rank-sum +distribution `sum_{g=0..5} rank(S_g) in {0, ..., 12}` is + +``` +[1, 0, 135, 720, 8865, 37800, 127149, 234360, 291690, 216720, 102240, 25920, 2976], +``` + +giving the complete two-role outer inventories: + +| Outer calls `n` | Zero-sum sequences | Gap placements `C(n+5, n)` | Total realizations | Distinct profiles (`sum rank <= n`) | +| ---: | ---: | ---: | ---: | ---: | +| 4 | 441 | 126 | 55,566 | 9,721 | +| 5 | 3,600 | 252 | 907,200 | 47,521 | +| 6 | 33,489 | 462 | 15,471,918 | 174,670 | + +### 4.1 Complete two-role quotient censuses + +For all `3,600` zero-sum five-`b` middle sequences, `census.py` evaluates every +realizable `a` and `c` prefix profile, filters by the exact necessary single-side +equations (`AB, BA, ABA, BAB` for `a` and `CB, BC, CBC, BCB` for `c`) and transported +`ABC = CBA = P` key compatibility, and then expands every realization and within-gap +interleaving across all six gaps to test `AC = 0`, `ACB = P`, and `BAC = P`: + +| Split `(n_a, n_b, n_c)` | `a` / `c` profile passes | Key pairs | Profile pairs | Expanded words | First fail `AC` | First fail `ACB` | `Q` survivors | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | +| `(4, 5, 4)` (retained PR #2175) | 89,052 / 1,201,320 | 68 | 152 | 5,536 | 1,480 | 4,056 | 0 | +| `(5, 5, 4)` (retained PR #2314) | 236,224 / 1,201,320 | 144 | 944 | 211,968 | 125,636 | 86,332 | 0 | +| `(4, 5, 5)` (retained PR #2314) | 89,052 / 2,899,368 | 136 | 912 | 209,920 | 117,308 | 92,612 | 0 | +| `(6, 5, 4)` (**new**) | 542,428 / 1,201,320 | 312 | 3,376 | 6,049,824 | 3,729,888 | 2,319,936 | **0** | +| `(5, 5, 5)` (**new**, 2-role) | 236,224 / 2,899,368 | 288 | 5,664 | 8,655,168 | 5,508,044 | 3,147,124 | **0** | +| `(4, 5, 6)` (**new**) | 89,052 / 5,883,552 | 312 | 3,280 | 5,874,848 | 3,496,252 | 2,378,596 | **0** | + +All `20,579,840` new 15-call two-role candidate words are rejected at `AC` or `ACB`. +By Lemma 1, this completely excludes `(6, 5, 4)` and `(4, 5, 6)` across all +finite dirty workspaces `r >= 2`, and excludes all two-role and common-orientation +`(5, 5, 5)` words. + +### 4.2 Complete three-role quotient censuses for `(5, 5, 5)` + +For each of the `5,664` compatible `(5, 5, 5)` active profile pairs `(N_b, tilde_P_a, tilde_P_c)` +and for each opposite-orientation mode (Case I and Case II), `census.py` enumerates +every dirty prefix profile `(r_1, ..., r_5)` and `(q_1, ..., q_5)` realized by + five `a` calls and five `c` calls (including pure-dirty calls with `tilde_N = 0` +and requiring at least one nonzero dirty bit on each side so `e^x = 1` and `e^y = 1`), +applies the exact homogeneous off-diagonal equations `W_KH = 0` and `W_HK = 0` from +Lemma 2(3), and then evaluates `W_HH` on `AC, ACB, BAC` across every gap split and +within-gap interleaving: + +| Three-role `(5, 5, 5)` mode | Active profile pairs | Dirty profile pairs passing `W_KH = W_HK = 0` | Expanded 3-role words | First fail `W_HH[AC]` | First fail `W_HH[ACB]` | `Mat_3(Q)` survivors | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | +| Case I (`e_a^x = e_c^y = 1`) | 5,664 | 17,864 | 42,447,616 | 25,294,720 | 17,152,896 | **0** | +| Case II (`e_a^y = e_c^x = 1`) | 5,664 | 17,864 | 42,447,616 | 25,294,720 | 17,152,896 | **0** | + +All `84,895,232` opposite-orientation three-role `(5, 5, 5)` words fail on `W_HH` +at `AC` or `ACB`. Together with the two-role census, this excludes `(5, 5, 5)` +across all finite dirty workspaces `r >= 2`. + +## 5. Main theorem and weighted price consequences + +**Theorem.** *In the formal rank-one group-algebra model over `F2[UT4(F2)]` for +`diag([z], [uz], I_rest)` on any finite number `r >= 2` of restored dirty roles:* + +1. *No 15-call word has `n_b = 5`: the count splits `(6, 5, 4)`, `(5, 5, 5)`, and + `(4, 5, 6)` are all impossible.* +2. *Every 15-call word satisfies `n_b >= 6`, and every word with `n_b = 5` (of any + total length `L` and on any finite number of roles `r >= 2`) satisfies + `n_a + n_c >= 11` and `L >= 16`.* +3. *For every nonnegative real letter-price triple `(alpha, beta, gamma) in R_{>= 0}^3`, + every realizing word has weighted cost at least* + ``` + min(4 alpha + 6 beta + 4 gamma, + 4 alpha + 5 beta + 4 gamma + 3 min(alpha, gamma)). + ``` +4. *Whenever `beta <= 3 min(alpha, gamma)`, the direct 14-call `(4, 6, 4)` word + (`abcbabcb` on `z` and `acbabc` on `uz`) attains this lower bound and is + therefore globally optimal across all word lengths `L` and all finite role + counts `r >= 2`. In particular, at `(alpha, beta, gamma) = (1, 3, 1)`, cost `25` + is impossible and `26` is the exact minimum.* + +*Proof.* Every realizing word satisfies `n_a >= 4`, `n_b >= 5`, `n_c >= 4`. If +`n_b = 5` and `n_a + n_c <= 10`, then `L = n_a + 5 + n_c <= 15`. Length `<= 14` is +excluded by PR #2175 and PR #2314, and length `15` (`(6, 5, 4)`, `(5, 5, 5)`, +`(4, 5, 6)`) is excluded by Lemmas 1–3 and the complete censuses in Section 4. +Thus `n_b = 5` implies `n_a + n_c >= 11` (`L >= 16`). + +For any `(alpha, beta, gamma) in R_{>= 0}^3`, a word with `n_b >= 6` costs at least +`4 alpha + 6 beta + 4 gamma`, while a word with `n_b = 5` has `n_a - 4 >= 0`, +`n_c - 4 >= 0`, and `(n_a - 4) + (n_c - 4) >= 3`, so it costs at least +`4 alpha + 5 beta + 4 gamma + 3 min(alpha, gamma)`. Comparing the two branches yields +`4 alpha + 6 beta + 4 gamma <= 4 alpha + 5 beta + 4 gamma + 3 min(alpha, gamma)` if +and only if `beta <= 3 min(alpha, gamma)`. At `(1, 3, 1)`, both branches equal `26`, +which is attained by the direct `(4, 6, 4)` word. [] + +## 6. Scope and limitations + +This result is a scoped formal register-model theorem and computer-assisted +necessary-quotient exclusion over `F2[UT4(F2)]`. It does not claim: + +- optimality outside the cone `beta <= 3 min(alpha, gamma)` (for instance at + `(alpha, beta, gamma) = (1, 4, 1)`, where the direct `(4, 6, 4)` word costs `32` + and the lower envelope is `31` via `L = 16` five-`b` candidates `(7, 5, 4)`, + `(6, 5, 5)`, `(5, 5, 6)`, `(4, 5, 7)`), +- a native bit-operation supplier, compiler lowering, or `kappa` bound change. diff --git a/research/ut4-fifteen-call-five-b/README.md b/research/ut4-fifteen-call-five-b/README.md new file mode 100644 index 0000000000..97fca0458a --- /dev/null +++ b/research/ut4-fifteen-call-five-b/README.md @@ -0,0 +1,151 @@ +# Complete 15-call five-b exclusion and the beta <= 3 min(alpha, gamma) price cone + +No fifteen-call word with five `b` calls realizes `diag([z], [uz], I_rest)` in +`F2[UT4(F2)]` on any finite number `r >= 2` of arbitrary restored dirty registers. +All three 15-call five-`b` count splits `(6, 5, 4)`, `(5, 5, 5)`, and `(4, 5, 6)` +explicitly handed off by Gareth Davidson (`@bitplane`) in +[PR #2314](https://github.com/CrocSwap/integer-mult-bounds/pull/2314) and +[PR #2343](https://github.com/CrocSwap/integer-mult-bounds/pull/2343) are excluded. + +Consequently, every 15-call word has `n_b >= 6`, and every word with `n_b = 5` +requires at least eleven outer (`a`/`c`) calls (`n_a + n_c >= 11`, total length +`L >= 16`). For nonnegative per-letter prices `(alpha, beta, gamma)`, the direct +fourteen-call `(4, 6, 4)` word is globally optimal throughout **`beta <= 3 min(alpha, gamma)`**, +with exact price `4 alpha + 6 beta + 4 gamma`. At `(alpha, beta, gamma) = (1, 3, 1)`, +cost `25` is impossible and `26` is the exact minimum. This is a formal register-model +theorem and does not provide a native bit supplier or improve `kappa`. + +## Model and evidence + +Work in the full group algebra `R = F2[UT4(F2)]` with adjacent generators +`a = I + E12`, `b = I + E23`, `c = I + E34` and targets `u = I + E13`, `z = I + E14`. +Each paid call is `I + ([g] + 1) x y^T` with `g in {a, b, c}` and `x y^T` a nonzero +binary rank-one coupling over `F2` (idempotent or nilpotent). Every occurrence, +including restoration, is charged; invertible `GL_r(F2)` mixing is normalized into +the couplings. Extra roles start arbitrary dirty and must be restored to identity +without contaminating the active outputs. + +[PROOF.md](PROOF.md) proves the uniform arbitrary-workspace reductions: + +1. **Two-role compression for `(6, 5, 4)` and `(4, 5, 6)` (Lemma 1):** Because + `n_b = 5` forces `e_b^x = e_b^y = 0` and `n_c = 4` (or `n_a = 4`) forces + `e_c^x = e_c^y = 0` (or `e_a^x = e_a^y = 0`), only one outer generator label + can have dirty row or column support. Any interior dirty contraction + `v_{i_m}(u_{i_{m+1}}) != 0` therefore occurs between two calls of the same + generator label, which vanishes identically in `R` by `([a] + 1)^2 = ([c] + 1)^2 = 0`. + Active-corner projection preserves the `2 x 2` active block over `R`, and + predecessor exclusions at length `<= 14` prevent any projected factor from + vanishing. +2. **Three-role active-plus-dirty decomposition for `(5, 5, 5)` (Lemma 2):** + All common-orientation excess profiles compress to two roles. The only remaining + 15-call five-`b` excess profiles are the two opposite-orientation three-role + cases (`Case I`: `(e_a^x, e_a^y, e_c^x, e_c^y) = (1, 0, 0, 1)`, and `Case II`: + `(0, 1, 1, 0)`). In `Mat_3(Q)`, the 14 basis monomials without adjacent `{A, C}` + decouple completely from the dirty role on `W_HH` (restricting the active projections + to the exact `5,664` compatible `(5, 5, 5)` profile pairs), the off-diagonal + blocks `W_KH = 0` and `W_HK = 0` have zero interior dirty contractions (yielding + exact homogeneous linear equations on the dirty prefix profiles), and `W_HH` on + `AC, ACB, BAC` receives only the rank-one cross-role contraction. +3. **Complete 5-gap rank-sum profile characterization (Lemma 3):** A 5-gap prefix + profile `P in Mat_2(F2)^5` with gap increments `S_g = P_{g+1} + P_g` is realizable + by `n in {4, 5, 6}` nonzero rank-one couplings if and only if + `sum_{g=0..5} rank(S_g) <= n`, yielding `9,721`, `47,521`, and `174,670` profiles + (`55,566`, `907,200`, and `15,471,918` realizations). + +### Complete two-role quotient censuses + +| Split `(a, b, c)` | `a` / `c` profile passes | Key pairs | Profile pairs | Expanded words | First fail `AC` | First fail `ACB` | `Q` survivors | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | +| `(4, 5, 4)`, retained PR #2175 control | 89,052 / 1,201,320 | 68 | 152 | 5,536 | 1,480 | 4,056 | 0 | +| `(5, 5, 4)`, retained PR #2314 control | 236,224 / 1,201,320 | 144 | 944 | 211,968 | 125,636 | 86,332 | 0 | +| `(4, 5, 5)`, retained PR #2314 control | 89,052 / 2,899,368 | 136 | 912 | 209,920 | 117,308 | 92,612 | 0 | +| `(6, 5, 4)`, **new** | 542,428 / 1,201,320 | 312 | 3,376 | 6,049,824 | 3,729,888 | 2,319,936 | **0** | +| `(5, 5, 5)`, **new** (2-role) | 236,224 / 2,899,368 | 288 | 5,664 | 8,655,168 | 5,508,044 | 3,147,124 | **0** | +| `(4, 5, 6)`, **new** | 89,052 / 5,883,552 | 312 | 3,280 | 5,874,848 | 3,496,252 | 2,378,596 | **0** | + +The three retained predecessor controls reproduce their exact counts and transcript +digests from PR #2175 and PR #2314. The new two-role total is **20,579,840 expanded +words**, with zero survivors. + +### Complete three-role `(5, 5, 5)` quotient censuses + +| Three-role `(5, 5, 5)` mode | Active profile pairs | Dirty profile pairs (`W_KH = W_HK = 0`) | Expanded 3-role words | First fail `W_HH[AC]` | First fail `W_HH[ACB]` | `Mat_3(Q)` survivors | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | +| Case I (`e_a^x = e_c^y = 1`) | 5,664 | 17,864 | 42,447,616 | 25,294,720 | 17,152,896 | **0** | +| Case II (`e_a^y = e_c^x = 1`) | 5,664 | 17,864 | 42,447,616 | 25,294,720 | 17,152,896 | **0** | + +The new three-role total is **84,895,232 expanded words**, with zero survivors. + +The separate [controls.py](controls.py) script checks: + +- all 4,096 literal `4 x 4` binary group products in `UT4(F2)` and all 20,440 words + of length `<= 3` against an independent subsequence-sum quotient oracle; +- the complete `16^5 = 1,048,576` profile rank-sum histogram and exact agreement + with the explicit 4-call (`55,566` realizations, `9,721` profiles) and 5-call + (`907,200` realizations, `47,521` profiles) gap catalogues; +- planted 15-call two-role word reconstruction and quotient evaluation across + `(6, 5, 4)`, `(5, 5, 5)`, and `(4, 5, 6)`; +- 50 same-label nilpotent dirty-compression pairs in `Mat_3(F2[UT4(F2)])` (confirming + Lemma 1 when both dirty rows and dirty columns are present on the same outer + generator label) and detection of a cross-label dirty contraction; +- an independent 3-role subsequence-sum quotient oracle `quotient_3role` in `Mat_3(Q)` + on planted 15-call three-role `(5, 5, 5)` words for both Case I and Case II, plus + perturbation negative controls where violating a single dirty bit breaks `W_KH = 0` + or `W_HK = 0`; +- all 28 span-rank profiles at `L <= 15` and 216 weighted price grid points, + including the `(1, 3, 1)` boundary minimum `26` and the outside-cone `(1, 4, 1)` + negative control (`31 < 32`). + +## Scope of the price result + +For all nonnegative letter prices `(alpha, beta, gamma)`, every word satisfies the +necessary lower bound + +``` +min(4 alpha + 6 beta + 4 gamma, + 4 alpha + 5 beta + 4 gamma + 3 min(alpha, gamma)). +``` + +The first branch is attained by the direct 14-call `(4, 6, 4)` word and is the +minimum whenever `beta <= 3 min(alpha, gamma)`. The second branch is a relaxed +count bound (`n_b = 5` implies `n_a + n_c >= 11`); whether any word with `n_b = 5` +exists at `L >= 16` remains open. + +## Reproduce + +From the repository root (standard library only): + +```sh +python3.12 -I -B scripts/research_package.py --package research/ut4-fifteen-call-five-b +# Direct commands: +python3 -I -O -B research/ut4-fifteen-call-five-b/verify.py +python3 -I -O -B research/ut4-fifteen-call-five-b/controls.py +``` + +Both commands complete in under 10 seconds total. `verify.py --write-result` +regenerates [RESULT.json](RESULT.json). + +## Open next questions + +1. Does any realizing word with `n_b = 5` exist at all in `F2[UT4(F2)]`, or is + `n_b >= 6` an unconditional structural invariant of `diag([z], [uz], I_rest)` + for every word length `L` and workspace size `r`? +2. At `L = 16` with `n_b = 5` (`(7, 5, 4)`, `(6, 5, 5)`, `(5, 5, 6)`, `(4, 5, 7)`), + the pairing bound from PR #2343 still restricts any realizing word to at most + `r <= 2 + floor((16 - 13) / 2) = 3` roles, and Lemma 1 compresses `(7, 5, 4)` + and `(4, 5, 7)` directly to `r = 2` roles. Can an algebraic invariant in `Q` + explain why `AC = 0` and `ACB = I_2` are incompatible with the 14 non-adjacent-`{A,C}` + equations whenever `n_b = 5`, without requiring a separate census at each outer + length `n_a + n_c`? + +## Credit + +Prepared by `steph4n-gh` with AI assistance (Antigravity). Apache-2.0. + +Full predecessor credit to Gareth Davidson (`@bitplane`, PR #2027, PR #2314, PR #2343) +for the mixed-root tariffs, 14-call weighted boundary, register-pairing compression, +and explicit 15-call `(1, 3, 1)` handoff; Nick Petalas (`@petalas`, PR #2175) for +the mixed-middle rank inequality, 13-call `(4, 5, 4)` census, and retained verifier +library; ToikY (PR #1662, PR #1680) and CinnaDavis / `1337isnot1337` (PR #1541) +for the degree-3 quotient and span-orientation compression; and Aaron Wang +(`@navinor`, PR #1690) for the gap-profile screening method. diff --git a/research/ut4-fifteen-call-five-b/RESULT.json b/research/ut4-fifteen-call-five-b/RESULT.json new file mode 100644 index 0000000000..262b33d273 --- /dev/null +++ b/research/ut4-fifteen-call-five-b/RESULT.json @@ -0,0 +1,861 @@ +{ + "algebra": { + "group_products": 4096, + "quotient_associativity": 4913 + }, + "domains": { + "4,5,4": { + "a_pass": 89052, + "c_pass": 1201320, + "first_differing_coefficient": { + "ac": 1480, + "acb": 4056 + }, + "key_pairs": 68, + "middles": 3600, + "profile_pair_digest_sha256": "441fc26dc79d854befefeaeaa1e27a97c2d9ad1b098b1b95d7e020323b277bdc", + "profile_pairs": 152, + "q_pass": 0, + "words": 5536 + }, + "4,5,5": { + "a_pass": 89052, + "c_pass": 2899368, + "first_differing_coefficient": { + "ac": 117308, + "acb": 92612 + }, + "key_pairs": 136, + "middles": 3600, + "profile_pair_digest_sha256": "9455792728ee0b4c067097898a58e65c9b9149dae2f4961583d932abbfb9e958", + "profile_pairs": 912, + "q_pass": 0, + "words": 209920 + }, + "4,5,6": { + "a_pass": 89052, + "c_pass": 5883552, + "first_differing_coefficient": { + "ac": 3496252, + "acb": 2378596 + }, + "key_pairs": 312, + "middles": 3600, + "profile_pair_digest_sha256": "2662a41ad8dc7d26eb65bd45699d1c667bd5dd6a2d7a1ca08cabde31c19c356d", + "profile_pairs": 3280, + "q_pass": 0, + "words": 5874848 + }, + "5,5,4": { + "a_pass": 236224, + "c_pass": 1201320, + "first_differing_coefficient": { + "ac": 125636, + "acb": 86332 + }, + "key_pairs": 144, + "middles": 3600, + "profile_pair_digest_sha256": "74b00f70775148bf5fa3805b09e20da3086b1d4fbfd1d2e6583db9f4deeff1fb", + "profile_pairs": 944, + "q_pass": 0, + "words": 211968 + }, + "5,5,5": { + "a_pass": 236224, + "c_pass": 2899368, + "first_differing_coefficient": { + "ac": 5508044, + "acb": 3147124 + }, + "key_pairs": 288, + "middles": 3600, + "profile_pair_digest_sha256": "d70d062fa08f5911c96118ea99d11945d62b45c707a4d1a4f17243fd3193f387", + "profile_pairs": 5664, + "q_pass": 0, + "words": 8655168 + }, + "6,5,4": { + "a_pass": 542428, + "c_pass": 1201320, + "first_differing_coefficient": { + "ac": 3729888, + "acb": 2319936 + }, + "key_pairs": 312, + "middles": 3600, + "profile_pair_digest_sha256": "cb305b4772c10bce66a2bfc1e7cccd00da5ebd4fff353930079179b8c0107bae", + "profile_pairs": 3376, + "q_pass": 0, + "words": 6049824 + } + }, + "outer_catalogues": { + "4": { + "profiles": 9721, + "realizations": 55566, + "zero_sequences": 441 + }, + "5": { + "profiles": 47521, + "realizations": 907200, + "zero_sequences": 3600 + }, + "6": { + "profiles": 174670, + "realizations": 15471918, + "zero_sequences": 33489 + } + }, + "planted_controls": { + "three_role_555": { + "case_II_row_a_col_c": { + "a_gap_counts": [ + 1, + 0, + 2, + 0, + 2, + 0 + ], + "a_profile": [ + 8, + 8, + 6, + 6, + 0 + ], + "c_gap_counts": [ + 1, + 0, + 0, + 2, + 0, + 2 + ], + "c_profile": [ + 8, + 8, + 8, + 14, + 14 + ], + "dirty_a_profile": [ + 0, + 0, + 1, + 1, + 0 + ], + "dirty_c_profile": [ + 0, + 0, + 0, + 1, + 1 + ], + "middle": [ + 2, + 10, + 8, + 8, + 8 + ], + "word_xy": [ + [ + "a", + 2, + 2 + ], + [ + "c", + 2, + 2 + ], + [ + "b", + 1, + 2 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 1, + 5 + ], + [ + "a", + 3, + 3 + ], + [ + "b", + 2, + 2 + ], + [ + "c", + 1, + 2 + ], + [ + "c", + 6, + 1 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 1, + 6 + ], + [ + "a", + 2, + 1 + ], + [ + "b", + 2, + 2 + ], + [ + "c", + 5, + 1 + ], + [ + "c", + 3, + 3 + ] + ] + }, + "case_I_col_a_row_c": { + "a_gap_counts": [ + 1, + 0, + 2, + 0, + 2, + 0 + ], + "a_profile": [ + 8, + 8, + 6, + 6, + 0 + ], + "c_gap_counts": [ + 1, + 0, + 0, + 2, + 0, + 2 + ], + "c_profile": [ + 8, + 8, + 8, + 14, + 14 + ], + "dirty_a_profile": [ + 0, + 0, + 1, + 1, + 0 + ], + "dirty_c_profile": [ + 0, + 0, + 0, + 1, + 1 + ], + "middle": [ + 2, + 10, + 8, + 8, + 8 + ], + "word_xy": [ + [ + "a", + 2, + 2 + ], + [ + "c", + 2, + 2 + ], + [ + "b", + 1, + 2 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 5, + 1 + ], + [ + "a", + 3, + 3 + ], + [ + "b", + 2, + 2 + ], + [ + "c", + 1, + 6 + ], + [ + "c", + 2, + 1 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 1, + 2 + ], + [ + "a", + 6, + 1 + ], + [ + "b", + 2, + 2 + ], + [ + "c", + 1, + 5 + ], + [ + "c", + 3, + 3 + ] + ] + } + }, + "two_role": { + "4,5,6": { + "a_profile": [ + 5, + 7, + 7, + 8, + 0 + ], + "a_realization": [ + [ + 5, + 2, + 15, + 8 + ], + [ + 0, + 1, + 3, + 4 + ] + ], + "c_profile": [ + 15, + 12, + 8, + 8, + 15 + ], + "c_realization": [ + [ + 15, + 3, + 4, + 2, + 5, + 15 + ], + [ + 0, + 1, + 2, + 4, + 4, + 5 + ] + ], + "middle": [ + 2, + 10, + 8, + 8, + 8 + ], + "word": [ + [ + "a", + 5 + ], + [ + "c", + 15 + ], + [ + "b", + 2 + ], + [ + "a", + 2 + ], + [ + "c", + 3 + ], + [ + "b", + 10 + ], + [ + "c", + 4 + ], + [ + "b", + 8 + ], + [ + "a", + 15 + ], + [ + "b", + 8 + ], + [ + "a", + 8 + ], + [ + "c", + 2 + ], + [ + "c", + 5 + ], + [ + "b", + 8 + ], + [ + "c", + 15 + ] + ] + }, + "5,5,5": { + "a_profile": [ + 8, + 8, + 6, + 6, + 0 + ], + "a_realization": [ + [ + 8, + 1, + 15, + 2, + 4 + ], + [ + 0, + 2, + 2, + 4, + 4 + ] + ], + "c_profile": [ + 8, + 8, + 8, + 14, + 14 + ], + "c_realization": [ + [ + 8, + 2, + 4, + 1, + 15 + ], + [ + 0, + 3, + 3, + 5, + 5 + ] + ], + "middle": [ + 2, + 10, + 8, + 8, + 8 + ], + "word": [ + [ + "a", + 8 + ], + [ + "c", + 8 + ], + [ + "b", + 2 + ], + [ + "b", + 10 + ], + [ + "a", + 1 + ], + [ + "a", + 15 + ], + [ + "b", + 8 + ], + [ + "c", + 2 + ], + [ + "c", + 4 + ], + [ + "b", + 8 + ], + [ + "a", + 2 + ], + [ + "a", + 4 + ], + [ + "b", + 8 + ], + [ + "c", + 1 + ], + [ + "c", + 15 + ] + ] + }, + "6,5,4": { + "a_profile": [ + 5, + 4, + 8, + 7, + 0 + ], + "a_realization": [ + [ + 5, + 1, + 12, + 15, + 2, + 5 + ], + [ + 0, + 1, + 2, + 3, + 4, + 4 + ] + ], + "c_profile": [ + 8, + 8, + 8, + 15, + 15 + ], + "c_realization": [ + [ + 8, + 2, + 5, + 15 + ], + [ + 0, + 3, + 3, + 5 + ] + ], + "middle": [ + 2, + 10, + 8, + 8, + 8 + ], + "word": [ + [ + "a", + 5 + ], + [ + "c", + 8 + ], + [ + "b", + 2 + ], + [ + "a", + 1 + ], + [ + "b", + 10 + ], + [ + "a", + 12 + ], + [ + "b", + 8 + ], + [ + "a", + 15 + ], + [ + "c", + 2 + ], + [ + "c", + 5 + ], + [ + "b", + 8 + ], + [ + "a", + 2 + ], + [ + "a", + 5 + ], + [ + "b", + 8 + ], + [ + "c", + 15 + ] + ] + } + } + }, + "positive": { + "formal_basis_columns": 192, + "formal_roles": 3, + "full_word": [ + [ + "a", + 1 + ], + [ + "b", + 1 + ], + [ + "c", + 1 + ], + [ + "b", + 1 + ], + [ + "a", + 1 + ], + [ + "b", + 1 + ], + [ + "c", + 1 + ], + [ + "b", + 1 + ], + [ + "a", + 8 + ], + [ + "c", + 8 + ], + [ + "b", + 8 + ], + [ + "a", + 8 + ], + [ + "b", + 8 + ], + [ + "c", + 8 + ] + ], + "omitted_call_controls": 14, + "wrong_letter_controls": 1 + }, + "profile_rank_sum_histogram": [ + 1, + 0, + 135, + 720, + 8865, + 37800, + 127149, + 234360, + 291690, + 216720, + 102240, + 25920, + 2976 + ], + "scope": "Formal F2[UT4(F2)] register-model theorem and complete necessary-quotient rejection for all 15-call five-b splits across arbitrary finite restored dirty workspaces; no native supplier or new kappa.", + "status": "PASS_UT4_FIFTEEN_CALL_FIVE_B", + "theorem": { + "all_fifteen_call_words_have_b_at_least_six": true, + "arbitrary_finite_restored_dirty_workspace": true, + "exact_price_in_region": "4 alpha+6 beta+4 gamma", + "excluded_fifteen_call_five_b_splits": [ + [ + 6, + 5, + 4 + ], + [ + 5, + 5, + 5 + ], + [ + 4, + 5, + 6 + ] + ], + "five_b_calls_require_at_least_eleven_outer_calls": true, + "five_b_calls_require_at_least_sixteen_total_calls": true, + "price_1_3_1_cost_25_impossible": true, + "price_1_3_1_exact_minimum": 26, + "sharp_price_region": "alpha,beta,gamma>=0 and beta<=3 min(alpha,gamma)", + "target": "diag([z],[uz],I_rest)", + "uniform_quantifiers_supplied_by": "PROOF.md, not finite role extrapolation", + "weighted_lower_bound": "min(4 alpha+6 beta+4 gamma, 4 alpha+5 beta+4 gamma+3 min(alpha,gamma))" + }, + "three_role_555": { + "case_II_row_a_col_c": { + "active_profile_pairs": 5664, + "dirty_pair_digest_sha256": "aeea3172d8c4fc8f6cb509ccf5ffc8ab0d849973caf05b3f7a8530e7b4fa8316", + "dirty_profile_pairs": 17864, + "first_differing_hh_coefficient": { + "ac": 25294720, + "acb": 17152896 + }, + "hh_q_pass": 0, + "words": 42447616 + }, + "case_I_col_a_row_c": { + "active_profile_pairs": 5664, + "dirty_pair_digest_sha256": "dda204f225684da589fa1a63a618c985e3e690619a32af70dd5128adca3970b6", + "dirty_profile_pairs": 17864, + "first_differing_hh_coefficient": { + "ac": 25294720, + "acb": 17152896 + }, + "hh_q_pass": 0, + "words": 42447616 + } + } +} diff --git a/research/ut4-fifteen-call-five-b/SOURCES.json b/research/ut4-fifteen-call-five-b/SOURCES.json new file mode 100644 index 0000000000..4896fda210 --- /dev/null +++ b/research/ut4-fifteen-call-five-b/SOURCES.json @@ -0,0 +1,198 @@ +{ + "schema_version": 1, + "base_commit": "da4f4fec60a88d9187f8ffa02f0f787b8b2da527", + "files": [ + { + "path": "AGENTS.md", + "usage": "provenance", + "git_blob": "00c96932e109c701310f4910057bae2d6cec0c0f", + "sha256": "2d47ee25f6900efa3bac76f66f59cc6d6e077ed1e7301497ab332668ad288d4c" + }, + { + "path": "CONTRIBUTING.md", + "usage": "provenance", + "git_blob": "e51435543687f1bd88ab22248082dc689ce8b853", + "sha256": "df5b5646602f42cb5da5844f04ac925182ddcd0f627b9de1c96a5095bb7a277a" + }, + { + "path": "autoresearch.md", + "usage": "provenance", + "git_blob": "0515a31cd888a18e5830987da12d4051f552c8cc", + "sha256": "e3e85885c27919c4f603954ef25339e9c1be4bd107f829921078b8134b366044" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "docs/research/community-efficient1000-review.md", + "usage": "provenance", + "git_blob": "fc9704487ccf5fbf0472950117741c219fe98151", + "sha256": "bac19ca28be781e7ac444e0666320ef77c0ac159467eafa3198e07b7c280442e" + }, + { + "path": "docs/research/research-family-status.md", + "usage": "provenance", + "git_blob": "1a2195004c5d681679279f0095b7964fb14a01e6", + "sha256": "c37c7e0f6a1134983990e1b3efef55e65239b38be780e8a4cc10f5aefdaf2df5" + }, + { + "path": "research/bit-gl3-mixed-targets-length10/README.md", + "usage": "provenance", + "git_blob": "59ac7008af69ffb41e10e6574308d68c33d44c48", + "sha256": "f1f88a618fa998baa2bb5e8bc69c225405b6106b4c0a5646d84c42166cd4aff5" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "provenance", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/register-pairing-compression/PROOF.md", + "usage": "input", + "git_blob": "f91d23a43002ac69e884af6d3fe485d0868d5b34", + "sha256": "f9c3c3f1363787ed0c92a65abba065d5debcb1e526a439cd3c82ad48d24f27bd" + }, + { + "path": "research/register-pairing-compression/RESULT.json", + "usage": "input", + "git_blob": "7f1f6600768fa704c96a160ce02d3ccc0479fd24", + "sha256": "151121844b1ada7462e0442ec1c5003c735c8e19bc1e1fdc1c1238ec950312dd" + }, + { + "path": "research/ut4-mixed-root-tariffs/PROOF.md", + "usage": "input", + "git_blob": "633a7d5137ad13fafe719cc042099977ad1f96e5", + "sha256": "c0def58338a69a57ac95f1d32a744993aa07656c46eba88a99354b276917bd8e" + }, + { + "path": "research/ut4-mixed-weighted-boundary/PROOF.md", + "usage": "input", + "git_blob": "d5ba9d06c0bb4e8553da56d504eb8d5f2ee0e1bd", + "sha256": "580fce5e5e460fd00afa8fa0231395859fdf5cf0998df9d21471b40a996665ef" + }, + { + "path": "research/ut4-mixed-weighted-boundary/RESULT.json", + "usage": "input", + "git_blob": "d08b7ff9bb0a68688ee6a981b2b2e21f7e95ecce", + "sha256": "631aaf146da1351246729984e8f7426125a1f91c68af99843e91b880e2f75e0f" + }, + { + "path": "research/ut4-one-slack-workspace/PROOF.md", + "usage": "input", + "git_blob": "4ca867ca780aff8bae8ab695959c89f35543586c", + "sha256": "a9e2c7e6f6841b0f9a53c65861c2e212c2bc126923d9e41f5723c530389e96cf" + } + ], + "vendor": { + "path": "vendor/predecessor.py", + "source_path": "research/ut4-mixed-central-middle/verify.py", + "head": "1d943bc9e0718c8a2f15e1d0a22b73ad528ef0ca", + "git_blob": "87eb17255d18450e3003108585f7d592f9879dce", + "sha256": "b7f8167aaf1fd41de03255d7b7048b82e527f2c9252b3245d5648e5d89afb342", + "author": "Nick Petalas / petalas", + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2175", + "reuse": "Unchanged finite quotient, group and profile/gap routines; original thirteen-call census retained as a control. No predecessor CLI or source checker is invoked." + }, + "predecessor_receipt": { + "source_path": "research/ut4-mixed-central-middle/EXPECTED.json", + "head": "1d943bc9e0718c8a2f15e1d0a22b73ad528ef0ca", + "git_blob": "a710e1e125f0b68242e1232a68b6f7e99540abd9", + "sha256": "722b533241ee0a18aa9af8944036084f64bd16acfbb94c9ffa7df31da1671d76", + "data": { + "algebra": { + "group_products": 4096, + "quotient_associativity": 4913 + }, + "census": { + "a_pass": 89052, + "c_pass": 1201320, + "expanded_transcript_sha256": "118ea0c1edc09d94b02e90dce7a6bf6168f917b5d10f78a9d59ef77dd04703a8", + "first_differing_coefficient": { + "ac": 1480, + "acb": 4056 + }, + "key_pairs": 68, + "middles": 3600, + "outer_zero_sequences": 441, + "profile_pairs": 152, + "profiles": 9721, + "q_pass": 0, + "words": 5536 + }, + "positive": { + "formal_basis_columns": 192, + "formal_roles": 3, + "full_word": [ + [ + "a", + 1 + ], + [ + "b", + 1 + ], + [ + "c", + 1 + ], + [ + "b", + 1 + ], + [ + "a", + 1 + ], + [ + "b", + 1 + ], + [ + "c", + 1 + ], + [ + "b", + 1 + ], + [ + "a", + 8 + ], + [ + "c", + 8 + ], + [ + "b", + 8 + ], + [ + "a", + 8 + ], + [ + "b", + 8 + ], + [ + "c", + 8 + ] + ], + "omitted_call_controls": 14, + "wrong_letter_controls": 1 + } + } + } +} diff --git a/research/ut4-fifteen-call-five-b/TASK.json b/research/ut4-fifteen-call-five-b/TASK.json new file mode 100644 index 0000000000..d0c1ceebe6 --- /dev/null +++ b/research/ut4-fifteen-call-five-b/TASK.json @@ -0,0 +1,158 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 5, + "base_commit": "da4f4fec60a88d9187f8ffa02f0f787b8b2da527", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "Resolve the explicit 15-call five-b weighted-tariff handoff (splits (6,5,4), (5,5,5), (4,5,6)) from PR #2314 and PR #2343 for diag([z],[uz],I_rest) over F2[UT4(F2)] across arbitrary finite restored dirty workspaces; expand the sharp price cone of the direct (4,6,4) word to beta <= 3 min(alpha,gamma) and prove cost 26 sharp (cost 25 impossible) at (alpha,beta,gamma) = (1,3,1).", + "scope_change_reason": "Follows the second card method ('Derive a target-specific relaxation bound for that same explicit alphabet') and resolves the explicit open handoff left by Gareth Davidson in PR #2314 and PR #2343 without starting a new native construction round. No physical conversion, new native alphabet or kappa improvement is claimed.", + "bottleneck_link": "Scoped formal-model weighted lower-bound screen for the nonabelian UT4(F2) bit mechanism: proves that five b calls require at least 11 outer calls (L >= 16) across arbitrary restored dirty workspaces, eliminating all cost-25 15-call candidates at letter prices (1,3,1). Physical native conversion remains separate and the selected complex side remains binding.", + "budget_minutes": 60, + "stop_rule": "Stop after proving two-role compression for (6,5,4) and (4,5,6), proving the three-role active-plus-dirty quotient decomposition for (5,5,5), and completing the exact 2-role and 3-role censuses for all three 15-call five-b splits.", + "outcome": "completed", + "evidence": "Complete two-role quotient censuses expand 20,579,840 new 15-call words across (6,5,4), (5,5,5), and (4,5,6) (0 survivors), while reproducing all three predecessor domains (4,5,4), (5,5,4), and (4,5,5) byte-for-byte. Complete three-role quotient censuses for the two opposite-orientation (5,5,5) modes expand 42,447,616 words per mode (84,895,232 total, 0 survivors). Separate algebra, 3-role subsequence quotient, nilpotent same-label dirty compression, rank-sum profile characterization, and weighted price controls pass in controls.py.", + "author": "steph4n-gh", + "ai_assistance": "Antigravity AI coding assistant used for mathematical analysis, census and control implementation, verification, and documentation.", + "selection": { + "seed": "09aa8c1ab0ddd939f9b2d42697e50a37", + "track": "bit-mechanisms", + "scope_key": "7084092dd726e7ba1f2f", + "draw_method": "Derive a target-specific relaxation bound for that same explicit alphabet.", + "rerolled": false + }, + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2019#discussioncomment-18961496", + "first_step": { + "command": "python3 -B scripts/research_baseline.py", + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "model_read": "Read Model section 1 of research/bit-three-register-lower-bound/README.md, research/ut4-mixed-weighted-boundary/PROOF.md, and research/register-pairing-compression/PROOF.md.", + "comparison": "Compared PR #2175 (13-call (4,5,4)), PR #2314 (14-call (5,5,4) and (4,5,5)), and PR #2343 (pairing compression to r <= 3 for 15-call (6,5,4), (5,5,5), (4,5,6)).", + "scope": "Orientation only; selected cold replay not rerun." + }, + "first_cost_screen": { + "prices": [ + 1, + 3, + 1 + ], + "credited_complete_direct_counts": [ + 4, + 6, + 4 + ], + "direct_cost": 26, + "hypothetical_changed_counts": [ + [ + 6, + 5, + 4 + ], + [ + 5, + 5, + 5 + ], + [ + 4, + 5, + 6 + ] + ], + "hypothetical_cost": 25, + "status": "The only candidate count splits that could beat the direct (4,6,4) cost 26 at prices (1,3,1); all three splits are completely excluded across arbitrary finite restored dirty workspaces." + }, + "predecessors": [ + { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2175", + "head": "1d943bc9e0718c8a2f15e1d0a22b73ad528ef0ca", + "author": "Nick Petalas / petalas", + "reused": "Retained vendor/predecessor.py verifier library, 13-call (4,5,4) control receipt, mixed-middle rank inequality, and direct (4,6,4) word." + }, + { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2314", + "head": "8be36b329ff225915024c28311b08e35334f0fa5", + "author": "Gareth Davidson / bitplane", + "reused": "14-call (5,5,4) and (4,5,5) control receipts and beta <= 2 min(alpha,gamma) weighted-boundary formulation." + }, + { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2343", + "head": "2b86d687b590cbdb09e33a5bb927f29e5a490226", + "author": "Gareth Davidson / bitplane", + "reused": "Register-pairing compression theorem reducing 15-call five-b words on arbitrary dirty workspace to at most three roles, and explicit (1,3,1) handoff." + } + ], + "validation": { + "python": "3.12.9", + "full_census": "PASS_UT4_FIFTEEN_CALL_FIVE_B", + "controls": "PASS_UT4_FIFTEEN_CALL_CONTROLS", + "receipt_sha256": "9b7ad621553bb1517c52128298e5ea66f3841f51cebed67dc9839d0b6ffb65bf", + "new_two_role_words": 20579840, + "three_role_555_words": 84895232, + "profile_rank_sum_total": 1048576, + "four_call_realizations": 55566, + "five_call_realizations": 907200, + "six_call_realizations": 15471918, + "short_quotient_words": 20440, + "literal_group_products": 4096, + "same_label_nilpotent_pairs": 50, + "span_profiles_15": 28, + "price_grids": 216, + "unrun": [ + "native/compiler realization", + "rational-frame conversion", + "global hosting and backward interface", + "recursive precision/reserves", + "selected cold replay", + "full multiplication theorem", + "proof-kernel verification", + "independent human review" + ] + }, + "open_questions": [ + { + "question": "Does any realizing word with n_b = 5 exist at all in F2[UT4(F2)], or is n_b >= 6 an unconditional invariant for diag([z],[uz],I_rest) across all lengths L and role counts r?", + "why_it_matters": "Controls weighted optimality outside the cone beta <= 3 min(alpha,gamma), such as at (alpha,beta,gamma) = (1,4,1).", + "first_step": "Test whether an algebraic invariant in the 17-dimensional quotient Q rules out AC = 0 and ACB = I_2 simultaneously for every outer length when n_b = 5, or examine the 16-call splits (7,5,4), (6,5,5), (5,5,6), (4,5,7) (which also compress to at most 3 roles by PR #2343).", + "blocked_by": "No length-independent proof that n_b = 5 forces an incompatibility between AC = 0, ACB = I_2, and the 14 non-adjacent-{A,C} quotient equations is known yet." + } + ] +} diff --git a/research/ut4-fifteen-call-five-b/VERIFY.json b/research/ut4-fifteen-call-five-b/VERIFY.json new file mode 100644 index 0000000000..001d31eef5 --- /dev/null +++ b/research/ut4-fifteen-call-five-b/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/register-pairing-compression/PROOF.md", + "research/register-pairing-compression/RESULT.json", + "research/ut4-mixed-root-tariffs/PROOF.md", + "research/ut4-mixed-weighted-boundary/PROOF.md", + "research/ut4-mixed-weighted-boundary/RESULT.json", + "research/ut4-one-slack-workspace/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Replays the retained PR #2175 algebra/positive controls and (4,5,4) receipt, the retained PR #2314 (5,5,4) and (4,5,5) receipts, the complete 2-role quotient censuses for (6,5,4), (5,5,5), and (4,5,6) (20,579,840 new words, 0 survivors), and the complete 3-role quotient censuses for both opposite-orientation (5,5,5) modes (84,895,232 words, 0 survivors) against RESULT.json." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/controls.py" + ], + "timeout_seconds": 120, + "checks": "Verifies literal 4x4 UT4(F2) group multiplication (4,096 products), an independent 2-role subsequence quotient oracle on 20,440 short words and planted 15-call words, the complete 16^5 profile rank-sum characterization, 50 same-label nilpotent dirty-compression pairs vs cross-label failure in Mat_3(F2[UT4(F2)]), an independent 3-role subsequence quotient oracle in Mat_3(Q) with perturbation negative controls, 28 span-rank profiles at L <= 15, and 216 weighted price grid points." + } + ] +} diff --git a/research/ut4-fifteen-call-five-b/census.py b/research/ut4-fifteen-call-five-b/census.py new file mode 100644 index 0000000000..0e7f64bef6 --- /dev/null +++ b/research/ut4-fifteen-call-five-b/census.py @@ -0,0 +1,775 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Complete 15-call five-b quotient census for diag([z],[uz],I_rest) over F2[UT4(F2)]. + +Extends Gareth Davidson's PR #2314 (ut4-mixed-weighted-boundary) and PR #2343 +(register-pairing-compression), and Nick Petalas's PR #2175 (ut4-mixed-central-middle), +to the three open 15-call five-b splits (6,5,4), (5,5,5) and (4,5,6) across +arbitrary finite restored dirty workspaces. + +The profile-screen method is credited to Aaron Wang (PR #1690), common-orientation +and span-excess compression to ToikY (PR #1662, PR #1680) and CinnaDavis / 1337isnot1337 +(PR #1541), the mixed-middle rank inequality to Nick Petalas (PR #2175), and the +mixed root tariffs, weighted boundary and pairing compression to Gareth Davidson +(PR #2027, PR #2314, PR #2343). No native bit supplier or new kappa is claimed. +""" +from collections import defaultdict +from hashlib import sha256 +from itertools import product +import importlib.util +import json +import math +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def load(): + source = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + vendor = source['vendor'] + require(sha256((HERE / vendor['path']).read_bytes()).hexdigest() == vendor['sha256'], + 'predecessor source hash') + for entry in source['files']: + if entry['usage'] == 'input': + require(sha256((ROOT / entry['path']).read_bytes()).hexdigest() == entry['sha256'], + 'proof input hash: ' + entry['path']) + spec = importlib.util.spec_from_file_location('ut4_retained_2175', HERE / vendor['path']) + result = importlib.util.module_from_spec(spec) + spec.loader.exec_module(result) + return result, source + + +def s_rank(P, s): + if s == 0: + return 0 + return 1 if s in P.COUPLINGS else 2 + + +def profile_gaps(p): + return (p[0], p[0] ^ p[1], p[1] ^ p[2], p[2] ^ p[3], p[3] ^ p[4], p[4]) + + +def build_two_role_gap_dp(P): + gap_dp = {(0, 0): {(0, 0, 0): 1}} + for total_k in range(1, 11): + for ka in range(total_k + 1): + kc = total_k - ka + if ka > 6 or kc > 6: + continue + cur = {} + if ka > 0 and (ka - 1, kc) in gap_dp: + for (sa, sc, qac), cnt in gap_dp[(ka - 1, kc)].items(): + for r in P.COUPLINGS: + key = (sa ^ r, sc, qac ^ P.MULT[sc][r]) + cur[key] = cur.get(key, 0) + cnt + if kc > 0 and (ka, kc - 1) in gap_dp: + for (sa, sc, qac), cnt in gap_dp[(ka, kc - 1)].items(): + for r in P.COUPLINGS: + key = (sa, sc ^ r, qac ^ P.MULT[sa][r]) + cur[key] = cur.get(key, 0) + cnt + gap_dp[(ka, kc)] = cur + + gap_qac = {} + for (ka, kc), d in gap_dp.items(): + by_s = {} + for (sa, sc, qac), cnt in d.items(): + by_s.setdefault((sa, sc), []).append((qac, cnt)) + for (sa, sc), lst in by_s.items(): + gap_qac[(ka, kc, sa, sc)] = tuple(sorted(lst)) + return gap_qac + + +def build_three_role_tables(P, srank): + a_choices_I = [] + c_choices_I = [] + a_choices_II = [] + c_choices_II = [] + for n in P.COUPLINGS: + x, y = P.SPLIT[n] + x_col = (x & 1) | ((x >> 1) << 2) + a_choices_I.append((n, 0, 0)) + a_choices_I.append((n, y, 1)) + c_choices_I.append((n, 0, 0)) + c_choices_I.append((n, x_col, 1)) + a_choices_II.append((n, 0, 0)) + a_choices_II.append((n, x_col, 1)) + c_choices_II.append((n, 0, 0)) + c_choices_II.append((n, y, 1)) + for v in (1, 2, 3): + v_col = (v & 1) | ((v >> 1) << 2) + a_choices_I.append((0, v, 1)) + c_choices_I.append((0, v_col, 1)) + a_choices_II.append((0, v_col, 1)) + c_choices_II.append((0, v, 1)) + + def build_gap_dirty(choices): + gap_d = {0: {0: ((0, 0, 1),)}} + dp_cur = {(0, 0, 0): 1} + for k in range(1, 4): + nxt = {} + for (s, w, hu), cnt in dp_cur.items(): + for n, dw, du in choices: + key = (s ^ n, w ^ dw, hu | du) + nxt[key] = nxt.get(key, 0) + cnt + dp_cur = nxt + by_s = {} + for (s, w, hu), cnt in dp_cur.items(): + by_s.setdefault(s, []).append((w, hu, cnt)) + gap_d[k] = {s: tuple(sorted(v)) for s, v in by_s.items()} + return gap_d + + def build_joint_dp(a_ch, c_ch, is_case_I): + joint_dp = {(0, 0): {(0, 0, 0, 0, 0): 1}} + for tot in range(1, 5): + for ka in range(tot + 1): + kc = tot - ka + if ka > 3 or kc > 3: + continue + cur = {} + if ka > 0 and (ka - 1, kc) in joint_dp: + for (sa, da, sc, dc, qac), cnt in joint_dp[(ka - 1, kc)].items(): + for na, dna, _ in a_ch: + extra = P.MULT[dc][dna] if is_case_I else 0 + key = (sa ^ na, da ^ dna, sc, dc, qac ^ P.MULT[sc][na] ^ extra) + cur[key] = cur.get(key, 0) + cnt + if kc > 0 and (ka, kc - 1) in joint_dp: + for (sa, da, sc, dc, qac), cnt in joint_dp[(ka, kc - 1)].items(): + for nc, dnc, _ in c_ch: + extra = 0 if is_case_I else P.MULT[da][dnc] + key = (sa, da, sc ^ nc, dc ^ dnc, qac ^ P.MULT[sa][nc] ^ extra) + cur[key] = cur.get(key, 0) + cnt + joint_dp[(ka, kc)] = cur + gap_qac3 = {} + for (ka, kc), d in joint_dp.items(): + by_s = {} + for (sa, da, sc, dc, qac), cnt in d.items(): + by_s.setdefault((sa, da, sc, dc), []).append((qac, cnt)) + for k, lst in by_s.items(): + gap_qac3[(ka, kc) + k] = tuple(sorted(lst)) + return gap_qac3 + + return { + 'I': (a_choices_I, c_choices_I, build_gap_dirty(a_choices_I), + build_gap_dirty(c_choices_I), build_joint_dp(a_choices_I, c_choices_I, True)), + 'II': (a_choices_II, c_choices_II, build_gap_dirty(a_choices_II), + build_gap_dirty(c_choices_II), build_joint_dp(a_choices_II, c_choices_II, False)), + } + + +def outer_inventories(P, srank): + dp = {0: 1} + zero_seqs = {} + for step in range(1, 7): + nxt = {} + for s, cnt in dp.items(): + for c in P.COUPLINGS: + nxt[s ^ c] = nxt.get(s ^ c, 0) + cnt + dp = nxt + if step in (4, 5, 6): + zero_seqs[step] = dp[0] + hist = [0] * 13 + for p0, p1, p2, p3, p4 in product(range(16), repeat=5): + r = (srank[p0] + srank[p0 ^ p1] + srank[p1 ^ p2] + + srank[p2 ^ p3] + srank[p3 ^ p4] + srank[p4]) + hist[r] += 1 + catalogues = {} + for n in (4, 5, 6): + catalogues[str(n)] = { + 'zero_sequences': zero_seqs[n], + 'profiles': sum(hist[:n + 1]), + 'realizations': zero_seqs[n] * math.comb(n + 5, n), + } + return catalogues, hist + + +def eval_base_2role(P, middle, sa_g, sc_g): + a = c = b = ac = ba = bc = acb = bac = 0 + for g in range(6): + sa, sc = sa_g[g], sc_g[g] + ac ^= P.MULT[a][sc] ^ P.MULT[c][sa] + bac ^= P.MULT[ba][sc] ^ P.MULT[bc][sa] + ba ^= P.MULT[b][sa] + bc ^= P.MULT[b][sc] + a ^= sa + c ^= sc + if g < 5: + nb = middle[g] + acb ^= P.MULT[ac][nb] + b ^= nb + return ac, acb, bac + + +def eval_base_3role_hh(P, middle, sa_g, da_g, sc_g, dc_g, is_case_I): + a = c = b = ac = ba = bc = acb = bac = 0 + d_pref = 0 + bd_pref = 0 + for g in range(6): + sa, da, sc, dc = sa_g[g], da_g[g], sc_g[g], dc_g[g] + cross_d = P.MULT[d_pref][da] if is_case_I else P.MULT[d_pref][dc] + b_cross_d = P.MULT[bd_pref][da] if is_case_I else P.MULT[bd_pref][dc] + ac ^= P.MULT[a][sc] ^ P.MULT[c][sa] ^ cross_d + bac ^= P.MULT[ba][sc] ^ P.MULT[bc][sa] ^ b_cross_d + ba ^= P.MULT[b][sa] + bc ^= P.MULT[b][sc] + bd_step = dc if is_case_I else da + bd_pref ^= P.MULT[b][bd_step] + a ^= sa + c ^= sc + d_pref ^= bd_step + if g < 5: + nb = middle[g] + acb ^= P.MULT[ac][nb] + b ^= nb + return ac, acb, bac + + +def first_2role_word_for_profile(P, middle, pa, pc, na, nc): + sa_g = profile_gaps(pa) + sc_g = profile_gaps(pc) + srank = tuple(s_rank(P, s) for s in range(16)) + valid_k = {0: (0, 2, 3, 4, 5, 6), 1: (1, 2, 3, 4, 5, 6), 2: (2, 3, 4, 5, 6)} + + def first_split(sg, n): + res = [] + def rec(g, rem): + if g == 6: + return rem == 0 + for k in valid_k[srank[sg[g]]]: + if k <= rem: + res.append(k) + if rec(g + 1, rem - k): + return True + res.pop() + return False + require(rec(0, n), 'split must exist') + return tuple(res) + + def first_seq_for_sum(k, target_s): + seq = [] + def rec(rem_k, cur_s): + if rem_k == 0: + return cur_s == target_s + for r in P.COUPLINGS: + seq.append(r) + if rec(rem_k - 1, cur_s ^ r): + return True + seq.pop() + return False + require(rec(k, 0), 'gap sequence must exist') + return tuple(seq) + + ka_tup = first_split(sa_g, na) + kc_tup = first_split(sc_g, nc) + a_ns, a_slots = [], [] + c_ns, c_slots = [], [] + word = [] + for g in range(6): + aseq = first_seq_for_sum(ka_tup[g], sa_g[g]) + cseq = first_seq_for_sum(kc_tup[g], sc_g[g]) + for r in aseq: + a_ns.append(r) + a_slots.append(g) + word.append(['a', r]) + for r in cseq: + c_ns.append(r) + c_slots.append(g) + word.append(['c', r]) + if g < 5: + word.append(['b', middle[g]]) + return { + 'middle': list(middle), + 'a_profile': list(pa), + 'c_profile': list(pc), + 'a_realization': [a_ns, a_slots], + 'c_realization': [c_ns, c_slots], + 'word': word, + } + + +def first_3role_word(P, middle, pa, pc, r_prof, ka_tup, q_prof, kc_tup, a_ch, c_ch, is_case_I): + sa_g = profile_gaps(pa) + sc_g = profile_gaps(pc) + da_g = profile_gaps(r_prof) + dc_g = profile_gaps(q_prof) + + def first_dirty_seq(k, target_s, target_d, choices): + seq = [] + def rec(rem, cs, cd): + if rem == 0: + return cs == target_s and cd == target_d + for n, d, ubit in choices: + seq.append((n, d, ubit)) + if rec(rem - 1, cs ^ n, cd ^ d): + return True + seq.pop() + return False + require(rec(k, 0, 0), 'dirty gap sequence must exist') + return tuple(seq) + + word = [] + for g in range(6): + aseq = first_dirty_seq(ka_tup[g], sa_g[g], da_g[g], a_ch) + cseq = first_dirty_seq(kc_tup[g], sc_g[g], dc_g[g], c_ch) + for n, d, ubit in aseq: + if n == 0: + x2, y2 = (0, d) if is_case_I else ((d & 1) | ((d >> 2) << 1), 0) + else: + x2, y2 = P.SPLIT[n] + x3 = (x2 | (ubit << 2)) if is_case_I else x2 + y3 = y2 if is_case_I else (y2 | (ubit << 2)) + word.append(['a', x3, y3]) + for n, d, vbit in cseq: + if n == 0: + x2, y2 = ((d & 1) | ((d >> 2) << 1), 0) if is_case_I else (0, d) + else: + x2, y2 = P.SPLIT[n] + x3 = x2 if is_case_I else (x2 | (vbit << 2)) + y3 = (y2 | (vbit << 2)) if is_case_I else y2 + word.append(['c', x3, y3]) + if g < 5: + xb, yb = P.SPLIT[middle[g]] + word.append(['b', xb, yb]) + return { + 'middle': list(middle), + 'a_profile': list(pa), + 'c_profile': list(pc), + 'dirty_a_profile': list(r_prof), + 'dirty_c_profile': list(q_prof), + 'a_gap_counts': list(ka_tup), + 'c_gap_counts': list(kc_tup), + 'word_xy': word, + } + + +def run(P, progress=False): + srank = tuple(s_rank(P, s) for s in range(16)) + catalogues, rank_hist = outer_inventories(P, srank) + gap_qac = build_two_role_gap_dp(P) + three_role_tabs = build_three_role_tables(P, srank) + + valid_k_for_type = {0: (0, 2, 3, 4, 5, 6), 1: (1, 2, 3, 4, 5, 6), 2: (2, 3, 4, 5, 6)} + splits_cache = {} + + def get_splits(stypes, n): + key = (stypes, n) + if key not in splits_cache: + res = [] + def rec(g, rem, cur): + if g == 6: + if rem == 0: + res.append(tuple(cur)) + return + for k in valid_k_for_type[stypes[g]]: + if k <= rem: + cur.append(k) + rec(g + 1, rem - k, cur) + cur.pop() + rec(0, n, []) + splits_cache[key] = tuple(res) + return splits_cache[key] + + def side_row(left, n): + right = left ^ n + row = [] + for p in range(16): + pn, np = P.MULT[p][n], P.MULT[n][p] + bab = P.MULT[P.MULT[left][p]][n] ^ P.MULT[np][right] + row.append(pn | (np << 4) | (P.MULT[pn][p] << 8) | (bab << 12)) + return tuple(row) + + key_int_tab = {} + for j in range(5): + for n in P.COUPLINGS: + x, y = P.SPLIT[n] + row = [] + for p in range(16): + px = ((p & 1) * (x & 1)) ^ (((p >> 1) & 1) * ((x >> 1) & 1)) + px |= ((((p >> 2) & 1) * (x & 1)) ^ (((p >> 3) & 1) * ((x >> 1) & 1))) << 1 + yp = ((y & 1) * (p & 1)) ^ (((y >> 1) & 1) * ((p >> 2) & 1)) + yp |= (((y & 1) * ((p >> 1) & 1)) ^ (((y >> 1) & 1) * ((p >> 3) & 1))) << 1 + val = (((px & 1) << j) | (((px >> 1) & 1) << (j + 5)) | + ((yp & 1) << (j + 10)) | (((yp >> 1) & 1) << (j + 15))) + row.append(val) + key_int_tab[(j, n)] = tuple(row) + + left_tab = {} + right_tab = {} + for n0 in P.COUPLINGS: + t0_r = side_row(0, n0) + k0_r = key_int_tab[(0, n0)] + for n1 in P.COUPLINGS: + t1_r = side_row(n0, n1) + k1_r = key_int_tab[(1, n1)] + for p2 in range(16): + lmap, lcnt = {}, {} + for p0 in range(16): + r0 = srank[p0] + v0, k0 = t0_r[p0], k0_r[p0] + for p1 in range(16): + rl = r0 + srank[p0 ^ p1] + srank[p1 ^ p2] + if rl <= 6: + vl = v0 ^ t1_r[p1] + lmap.setdefault(vl, []).append((p0, p1, rl, k0 | k1_r[p1])) + lcnt[vl] = lcnt.get(vl, 0) + (1 << (8 * rl)) + left_tab[(n0, n1, p2)] = (tuple(lmap.items()), lcnt) + + for n4 in P.COUPLINGS: + t4_r = side_row(n4, n4) + k4_r = key_int_tab[(4, n4)] + for n3 in P.COUPLINGS: + t3_r = side_row(n3 ^ n4, n3) + k3_r = key_int_tab[(3, n3)] + for p2 in range(16): + rmap, rcnt = {}, {} + for p3 in range(16): + r23 = srank[p2 ^ p3] + v3, k3 = t3_r[p3], k3_r[p3] + for p4 in range(16): + rr = r23 + srank[p3 ^ p4] + srank[p4] + if rr <= 6: + vr = v3 ^ t4_r[p4] + rmap.setdefault(vr, []).append((p3, p4, rr, k3 | k4_r[p4])) + rcnt[vr] = rcnt.get(vr, 0) + (1 << (8 * rr)) + right_tab[(n3, n4, p2)] = (rmap, rcnt) + + def unpack_valid_key(k): + u0, u1, w0, w1 = k & 31, (k >> 5) & 31, (k >> 10) & 31, (k >> 15) & 31 + if not (u0 and u1 and u0 != u1 and w0 and w1 and w0 != w1): + return None + return (u0, u1, w0, w1) + + def get_dirty_profs(p, gap_d, cache): + if p not in cache: + sg = profile_gaps(p) + res = set() + def rec(g, rem_k, cur_r, cur_hu, r_pref, k_tup): + if g == 6: + if rem_k == 0 and cur_r == 0 and cur_hu == 1: + res.add((tuple(r_pref), tuple(k_tup))) + return + s = sg[g] + for k in range(min(3, rem_k) + 1): + for w, hu, _ in gap_d[k].get(s, ()): + nr = cur_r ^ w + k_tup.append(k) + if g < 5: + r_pref.append(nr) + rec(g + 1, rem_k - k, nr, cur_hu | hu, r_pref, k_tup) + r_pref.pop() + else: + rec(g + 1, rem_k - k, nr, cur_hu | hu, r_pref, k_tup) + k_tup.pop() + rec(0, 5, 0, 0, [], []) + by_r = {} + for r_pref, k_tup in sorted(res): + by_r.setdefault(r_pref, []).append(k_tup) + cache[p] = tuple((r_pref, tuple(ktups)) for r_pref, ktups in sorted(by_r.items())) + return cache[p] + + dirty_caches = {'I': ({}, {}), 'II': ({}, {})} + + domains = { + '4,5,4': (4, 4), '5,5,4': (5, 4), '4,5,5': (4, 5), + '6,5,4': (6, 4), '5,5,5': (5, 5), '4,5,6': (4, 6), + } + counts = { + key: dict(middles=0, a_pass=0, c_pass=0, key_pairs=0, + profile_pairs=0, words=0, q_pass=0) + for key in domains + } + failures = {key: defaultdict(int) for key in domains} + digests = {key: sha256() for key in domains} + planted_2role = {} + + three_role_stats = { + mode: dict(active_profile_pairs=0, dirty_profile_pairs=0, + words=0, hh_q_pass=0, ac_fail=0, acb_fail=0, bac_fail=0) + for mode in ('case_I_col_a_row_c', 'case_II_row_a_col_c') + } + three_role_digests = { + mode: sha256() for mode in ('case_I_col_a_row_c', 'case_II_row_a_col_c') + } + planted_3role = {} + + for middle in product(P.COUPLINGS, repeat=5): + if P.total(middle): + continue + for key in domains: + counts[key]['middles'] += 1 + n0, n1, n2, n3, n4 = middle + t2_r = side_row(n0 ^ n1, n2) + k2_r = key_int_tab[(2, n2)] + a_by_n = {4: {}, 5: {}, 6: {}} + a_counts = [0] * 7 + c_counts = [0] * 7 + for p2 in range(16): + v2_base = t2_r[p2] + k2_base = k2_r[p2] + l_items, lcnt = left_tab[(n0, n1, p2)] + rmap, rcnt = right_tab[(n3, n4, p2)] + for vl, l_list in l_items: + lc = lcnt[vl] + rc = rcnt.get(vl ^ v2_base, 0) + if rc: + for rl in range(7): + c_l = (lc >> (8 * rl)) & 0xff + if c_l: + for rr in range(7 - rl): + c_counts[rl + rr] += c_l * ((rc >> (8 * rr)) & 0xff) + ra = rmap.get(vl ^ v2_base ^ 0x8888) + if ra: + for p0, p1, rl, kl in l_list: + kl2 = kl | k2_base + for p3, p4, rr, kr in ra: + rtot = rl + rr + if rtot <= 6: + a_counts[rtot] += 1 + pk = unpack_valid_key(kl2 | kr) + if pk is not None: + prof = (p0, p1, p2, p3, p4) + if rtot <= 4: + a_by_n[4].setdefault(pk, []).append(prof) + if rtot <= 5: + a_by_n[5].setdefault(pk, []).append(prof) + a_by_n[6].setdefault(pk, []).append(prof) + a_tots = {4: sum(a_counts[:5]), 5: sum(a_counts[:6]), 6: sum(a_counts[:7])} + c_tots = {4: sum(c_counts[:5]), 5: sum(c_counts[:6]), 6: sum(c_counts[:7])} + for key, (na, nc) in domains.items(): + counts[key]['a_pass'] += a_tots[na] + counts[key]['c_pass'] += c_tots[nc] + if not a_by_n[6]: + continue + max_nc = 6 if a_by_n[4] else (5 if a_by_n[5] else 4) + c_by_n = {4: {}, 5: {}, 6: {}} + for p2 in range(16): + v2_base = t2_r[p2] + k2_base = k2_r[p2] + l_items, _ = left_tab[(n0, n1, p2)] + rmap, _ = right_tab[(n3, n4, p2)] + for vl, l_list in l_items: + rc_list = rmap.get(vl ^ v2_base) + if rc_list: + for p0, p1, rl, kl in l_list: + if rl > max_nc: + continue + kl2 = kl | k2_base + for p3, p4, rr, kr in rc_list: + rtot = rl + rr + if rtot <= max_nc: + pk = unpack_valid_key(kl2 | kr) + if pk is not None: + prof = (p0, p1, p2, p3, p4) + if rtot <= 4: + c_by_n[4].setdefault(pk, []).append(prof) + if rtot <= 5 and max_nc >= 5: + c_by_n[5].setdefault(pk, []).append(prof) + if max_nc >= 6: + c_by_n[6].setdefault(pk, []).append(prof) + + for n in (4, 5, 6): + for k in a_by_n[n]: + a_by_n[n][k].sort() + for k in c_by_n[n]: + c_by_n[n][k].sort() + + b_pref = (0, middle[0], middle[0] ^ middle[1], + middle[0] ^ middle[1] ^ middle[2], + middle[0] ^ middle[1] ^ middle[2] ^ middle[3], 0) + + for key, (na, nc) in domains.items(): + if not a_by_n[na] or not c_by_n[nc]: + continue + counter = counts[key] + a_dict, c_dict = a_by_n[na], c_by_n[nc] + for ka, kc in sorted(P.compatible_keys(a_dict, c_dict)): + counter['key_pairs'] += 1 + for pa, pc in product(a_dict[ka], c_dict[kc]): + counter['profile_pairs'] += 1 + sa_g = profile_gaps(pa) + sc_g = profile_gaps(pc) + sa_t = tuple(srank[s] for s in sa_g) + sc_t = tuple(srank[s] for s in sc_g) + base_ac, base_acb, base_bac = eval_base_2role(P, middle, sa_g, sc_g) + pair_words = pair_ac = pair_acb = 0 + for ka_tup in get_splits(sa_t, na): + for kc_tup in get_splits(sc_t, nc): + g_lists = [gap_qac[(ka_tup[g], kc_tup[g], sa_g[g], sc_g[g])] for g in range(6)] + for q0, w0 in g_lists[0]: + for q1, w1 in g_lists[1]: + w01 = w0 * w1 + ac1 = base_ac ^ q0 ^ q1 + acb1 = base_acb ^ P.MULT[q1][b_pref[1]] + bac1 = base_bac ^ P.MULT[b_pref[1]][q1] + for q2, w2 in g_lists[2]: + w02 = w01 * w2 + ac2 = ac1 ^ q2 + acb2 = acb1 ^ P.MULT[q2][b_pref[2]] + bac2 = bac1 ^ P.MULT[b_pref[2]][q2] + for q3, w3 in g_lists[3]: + w03 = w02 * w3 + ac3 = ac2 ^ q3 + acb3 = acb2 ^ P.MULT[q3][b_pref[3]] + bac3 = bac2 ^ P.MULT[b_pref[3]][q3] + for q4, w4 in g_lists[4]: + w04 = w03 * w4 + ac4 = ac3 ^ q4 + acb4 = acb3 ^ P.MULT[q4][b_pref[4]] + bac4 = bac3 ^ P.MULT[b_pref[4]][q4] + for q5, w5 in g_lists[5]: + w = w04 * w5 + ac = ac4 ^ q5 + pair_words += w + if ac != 0: + pair_ac += w + elif acb4 != 9: + pair_acb += w + else: + require(bac4 != 9, 'unexpected 2-role quotient survivor: ' + key) + failures[key]['bac'] += w + counter['words'] += pair_words + failures[key]['ac'] += pair_ac + failures[key]['acb'] += pair_acb + digests[key].update( + P.canonical([list(middle), list(pa), list(pc), pair_words, pair_ac, pair_acb]) + b'\n' + ) + if key in ('6,5,4', '5,5,5', '4,5,6') and key not in planted_2role: + planted_2role[key] = first_2role_word_for_profile(P, middle, pa, pc, na, nc) + + if key == '5,5,5': + for tag, mode_name, is_case_I in ( + ('I', 'case_I_col_a_row_c', True), + ('II', 'case_II_row_a_col_c', False), + ): + a_ch, c_ch, gap_da, gap_dc, gap_qac3 = three_role_tabs[tag] + da_cache, dc_cache = dirty_caches[tag] + st3 = three_role_stats[mode_name] + st3['active_profile_pairs'] += 1 + valid_da = [] + for da_prof, ka_tups in get_dirty_profs(pa, gap_da, da_cache): + v1 = v2 = v3 = 0 + for j in range(5): + if is_case_I: + rn = P.MULT[da_prof[j]][middle[j]] + v1 ^= rn + v2 ^= P.MULT[rn][pa[j]] + v3 ^= P.MULT[rn][pc[j]] + else: + nq = P.MULT[middle[j]][da_prof[j]] + v1 ^= nq + v2 ^= P.MULT[pa[j]][nq] + v3 ^= P.MULT[pc[j]][nq] + if v1 == 0 and v2 == 0 and v3 == 0: + valid_da.append((da_prof, ka_tups)) + if not valid_da: + continue + valid_dc = [] + for dc_prof, kc_tups in get_dirty_profs(pc, gap_dc, dc_cache): + v1 = v2 = v3 = 0 + for j in range(5): + if is_case_I: + nq = P.MULT[middle[j]][dc_prof[j]] + v1 ^= nq + v2 ^= P.MULT[pc[j]][nq] + v3 ^= P.MULT[pa[j]][nq] + else: + rn = P.MULT[dc_prof[j]][middle[j]] + v1 ^= rn + v2 ^= P.MULT[rn][pc[j]] + v3 ^= P.MULT[rn][pa[j]] + if v1 == 0 and v2 == 0 and v3 == 0: + valid_dc.append((dc_prof, kc_tups)) + if not valid_dc: + continue + for da_prof, ka_tups in valid_da: + da_g = profile_gaps(da_prof) + for dc_prof, kc_tups in valid_dc: + dc_g = profile_gaps(dc_prof) + st3['dirty_profile_pairs'] += 1 + b_ac, b_acb, b_bac = eval_base_3role_hh( + P, middle, sa_g, da_g, sc_g, dc_g, is_case_I + ) + dp_words = dp_ac = dp_acb = 0 + for ka_tup in ka_tups: + for kc_tup in kc_tups: + g_lists = [ + gap_qac3[(ka_tup[g], kc_tup[g], sa_g[g], da_g[g], sc_g[g], dc_g[g])] + for g in range(6) + ] + for q0, w0 in g_lists[0]: + for q1, w1 in g_lists[1]: + w01 = w0 * w1 + ac1 = b_ac ^ q0 ^ q1 + acb1 = b_acb ^ P.MULT[q1][b_pref[1]] + bac1 = b_bac ^ P.MULT[b_pref[1]][q1] + for q2, w2 in g_lists[2]: + w02 = w01 * w2 + ac2 = ac1 ^ q2 + acb2 = acb1 ^ P.MULT[q2][b_pref[2]] + bac2 = bac1 ^ P.MULT[b_pref[2]][q2] + for q3, w3 in g_lists[3]: + w03 = w02 * w3 + ac3 = ac2 ^ q3 + acb3 = acb2 ^ P.MULT[q3][b_pref[3]] + bac3 = bac2 ^ P.MULT[b_pref[3]][q3] + for q4, w4 in g_lists[4]: + w04 = w03 * w4 + ac4 = ac3 ^ q4 + acb4 = acb3 ^ P.MULT[q4][b_pref[4]] + bac4 = bac3 ^ P.MULT[b_pref[4]][q4] + for q5, w5 in g_lists[5]: + w = w04 * w5 + ac = ac4 ^ q5 + dp_words += w + if ac != 0: + dp_ac += w + elif acb4 != 9: + dp_acb += w + else: + require(bac4 != 9, 'unexpected 3-role survivor') + st3['bac_fail'] += w + st3['words'] += dp_words + st3['ac_fail'] += dp_ac + st3['acb_fail'] += dp_acb + three_role_digests[mode_name].update( + P.canonical([ + list(middle), list(pa), list(pc), + list(da_prof), list(dc_prof), + dp_words, dp_ac, dp_acb, + ]) + b'\n' + ) + if mode_name not in planted_3role: + planted_3role[mode_name] = first_3role_word( + P, middle, pa, pc, da_prof, ka_tups[0], + dc_prof, kc_tups[0], a_ch, c_ch, is_case_I + ) + + if progress and counts['4,5,4']['middles'] % 900 == 0: + print('Checked middle sequences:', counts['4,5,4']['middles'], flush=True) + + for key in domains: + counts[key]['profile_pair_digest_sha256'] = digests[key].hexdigest() + counts[key]['first_differing_coefficient'] = dict(sorted(failures[key].items())) + + for mode_name, st3 in three_role_stats.items(): + st3['first_differing_hh_coefficient'] = {'ac': st3.pop('ac_fail'), 'acb': st3.pop('acb_fail')} + bac_f = st3.pop('bac_fail') + if bac_f: + st3['first_differing_hh_coefficient']['bac'] = bac_f + st3['dirty_pair_digest_sha256'] = three_role_digests[mode_name].hexdigest() + + return { + 'outer_catalogues': catalogues, + 'profile_rank_sum_histogram': rank_hist, + 'domains': counts, + 'three_role_555': three_role_stats, + 'planted_controls': { + 'two_role': planted_2role, + 'three_role_555': planted_3role, + }, + } diff --git a/research/ut4-fifteen-call-five-b/controls.py b/research/ut4-fifteen-call-five-b/controls.py new file mode 100644 index 0000000000..7cd482b3e1 --- /dev/null +++ b/research/ut4-fifteen-call-five-b/controls.py @@ -0,0 +1,368 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent algebra, 3-role quotient, and coverage controls for the 15-call five-b boundary. + +No predecessor scalar multiplication, reduction or group multiplication is +used by the dense/subsequence and literal-matrix oracles below. +""" +from collections import defaultdict +from itertools import combinations, combinations_with_replacement, product +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('ut4_fifteen_call_controls_census', HERE / 'census.py') +C = importlib.util.module_from_spec(spec) +spec.loader.exec_module(C) +P, source = C.load() +require = C.require + + +def matmul_r(a, b, r): + aa = [[(a >> (r * i + j)) & 1 for j in range(r)] for i in range(r)] + bb = [[(b >> (r * i + j)) & 1 for j in range(r)] for i in range(r)] + cc = [[sum(aa[i][k] * bb[k][j] for k in range(r)) % 2 for j in range(r)] for i in range(r)] + return sum(cc[i][j] << (r * i + j) for i in range(r) for j in range(r)) + + +def quotient_classes(): + words = [''.join(w) for n in range(4) for w in product('abc', repeat=n)] + result = {} + for word in words: + orbit, queue = {word}, [word] + for w in queue: + for i in range(len(w) - 1): + if w[i:i + 2] in ('ac', 'ca'): + changed = w[:i] + w[i:i + 2][::-1] + w[i + 2:] + if changed not in orbit: + orbit.add(changed) + queue.append(changed) + zero = any(any(w[i] == w[i + 1] for i in range(len(w) - 1)) for w in orbit) + result[word] = None if zero else min(orbit) + require(len(set(result.values()) - {None}) == 17, 'independent quotient dimension') + return result + + +CLASSES = quotient_classes() +MM2 = [[matmul_r(a, b, 2) for b in range(16)] for a in range(16)] + + +def quotient_2role(word): + result = {'': 9} + for degree in range(1, min(3, len(word)) + 1): + for indices in combinations(range(len(word)), degree): + name = CLASSES[''.join(word[i][0] for i in indices)] + if name is None: + continue + coefficient = 9 + for i in indices: + coefficient = MM2[coefficient][word[i][1]] + result[name] = result.get(name, 0) ^ coefficient + return {k: v for k, v in result.items() if v} + + +def quotient_3role(word): + ident3 = 1 | (1 << 4) | (1 << 8) + result = {'': ident3} + for degree in range(1, min(3, len(word)) + 1): + for indices in combinations(range(len(word)), degree): + name = CLASSES[''.join(word[i][0] for i in indices)] + if name is None: + continue + coefficient = ident3 + for i in indices: + coefficient = matmul_r(coefficient, word[i][1], 3) + result[name] = result.get(name, 0) ^ coefficient + return {k: v for k, v in result.items() if v} + + +def address(g): + a, b, c, d, e, f = [(g >> i) & 1 for i in range(6)] + return (1 | (a << 1) | (d << 2) | (f << 3), 2 | (b << 2) | (e << 3), 4 | (c << 3), 8) + + +def binary_product(a, b): + rows = [] + for row in a: + value = 0 + for j in range(4): + if (row >> j) & 1: + value ^= b[j] + rows.append(value) + return tuple(rows) + + +ADDRESSES = [address(g) for g in range(64)] +INDEX = {matrix: g for g, matrix in enumerate(ADDRESSES)} +GROUP = [[INDEX[binary_product(a, b)] for b in ADDRESSES] for a in ADDRESSES] +GENERATORS = dict(a=1, b=2, c=4) + + +def formal(word, roles): + result = [[{0} if i == j else set() for j in range(roles)] for i in range(roles)] + for letter, mask in word: + old = [[set(entry) for entry in row] for row in result] + for i, j, k in product(range(roles), repeat=3): + if (mask >> (roles * k + j)) & 1: + result[i][j].symmetric_difference_update(old[i][k]) + result[i][j].symmetric_difference_update(GROUP[g][GENERATORS[letter]] for g in old[i][k]) + return result + + +def outer(x, y, roles): + return sum(((x >> i) & (y >> j) & 1) << (roles * i + j) + for i in range(roles) for j in range(roles)) + + +def project_3to2(mask): + return sum(((mask >> (3 * i + j)) & 1) << (2 * i + j) for i in range(2) for j in range(2)) + + +def extract_kh_vec(mask3): + return ((mask3 >> (3 * 2 + 0)) & 1) | (((mask3 >> (3 * 2 + 1)) & 1) << 1) + + +def extract_hk_vec(mask3): + return ((mask3 >> (3 * 0 + 2)) & 1) | (((mask3 >> (3 * 1 + 2)) & 1) << 1) + + +def catalogue_explicit(n): + positions = tuple(combinations_with_replacement(range(6), n)) + result = defaultdict(list) + zeros = 0 + for ns in product(P.COUPLINGS, repeat=n): + if P.total(ns): + continue + zeros += 1 + prefix = [0] * (n + 1) + for index, item in enumerate(ns, 1): + prefix[index] = prefix[index - 1] ^ item + for slots in positions: + counts = [0] * 6 + for slot in slots: + counts[slot] += 1 + acc = 0 + profile = [] + for count in counts[:5]: + acc += count + profile.append(prefix[acc]) + result[tuple(profile)].append((ns, slots)) + return dict(result), zeros + + +def main(): + for g, h in product(range(64), repeat=2): + require(GROUP[g][h] == P.group_product(g, h), 'literal group law disagreement') + + alphabet = tuple(product('abc', P.COUPLINGS)) + short = 0 + for length in range(4): + for word in product(alphabet, repeat=length): + require(quotient_2role(word) == P.quotient(word), 'independent 2-role quotient disagreement') + short += 1 + require(short == 20440, 'short-word coverage') + + result = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + positive = [tuple(step) for step in result['positive']['full_word']] + require(quotient_2role(positive) == P.TARGET, 'positive quotient control') + + # 1. Verify rank-sum profile characterization across all 16^5 = 1,048,576 profiles + srank = tuple(C.s_rank(P, s) for s in range(16)) + cat4, z4 = catalogue_explicit(4) + cat5, z5 = catalogue_explicit(5) + require((cat4, z4) == P.gap_catalogue(), 'unchanged four-call catalogue control') + require(z4 == 441 and z5 == 3600, 'zero-sum outer sequence counts for n=4,5') + require(sum(map(len, cat4.values())) == 55566, 'four-call realization count') + require(sum(map(len, cat5.values())) == 907200, 'five-call realization count') + + rank_hist = [0] * 13 + by_max_rank = {4: set(), 5: set(), 6: set()} + for prof in product(range(16), repeat=5): + gaps = C.profile_gaps(prof) + r = sum(srank[s] for s in gaps) + rank_hist[r] += 1 + for n in (4, 5, 6): + if r <= n: + by_max_rank[n].add(prof) + require(rank_hist == result['profile_rank_sum_histogram'], 'rank-sum histogram mismatch') + require(set(cat4) == by_max_rank[4] and len(cat4) == 9721, 'n=4 rank-sum profile set mismatch') + require(set(cat5) == by_max_rank[5] and len(cat5) == 47521, 'n=5 rank-sum profile set mismatch') + require(len(by_max_rank[6]) == 174670, 'n=6 rank-sum profile count mismatch') + + # 2. Verify planted 2-role reconstruction controls across (6,5,4), (5,5,5), (4,5,6) + for key, fixture in result['planted_controls']['two_role'].items(): + word = tuple((step[0], step[1]) for step in fixture['word']) + middle = tuple(fixture['middle']) + na, _, nc = map(int, key.split(',')) + pa, pc = tuple(fixture['a_profile']), tuple(fixture['c_profile']) + ra = (tuple(fixture['a_realization'][0]), tuple(fixture['a_realization'][1])) + rc = (tuple(fixture['c_realization'][0]), tuple(fixture['c_realization'][1])) + require(len(ra[0]) == na and len(rc[0]) == nc, f'outer count mismatch in {key}') + require(pa in by_max_rank[na] and pc in by_max_rank[nc], f'planted profile rank-sum invalid in {key}') + require(word in P.expanded_words(middle, ra, rc), f'planted interleaving lost in {key}') + q2 = quotient_2role(word) + for cls in ('', 'a', 'b', 'c', 'ab', 'ba', 'bc', 'cb', 'aba', 'abc', 'bab', 'bcb', 'cba', 'cbc'): + require(q2.get(cls, 0) == P.TARGET.get(cls, 0), f'2-role non-adjacent-ac {cls} mismatch in {key}') + sa_g, sc_g = C.profile_gaps(pa), C.profile_gaps(pc) + b_ac, b_acb, b_bac = C.eval_base_2role(P, middle, sa_g, sc_g) + b_pref = (0, middle[0], middle[0] ^ middle[1], + middle[0] ^ middle[1] ^ middle[2], + middle[0] ^ middle[1] ^ middle[2] ^ middle[3], 0) + for g in range(6): + qg = P.MULT[sa_g[g]][sc_g[g]] + b_ac ^= qg + b_acb ^= P.MULT[qg][b_pref[g]] + b_bac ^= P.MULT[b_pref[g]][qg] + require(q2.get('ac', 0) == b_ac and q2.get('acb', 0) == b_acb and q2.get('bac', 0) == b_bac, + f'long-word 2-role oracle disagreement in {key}') + ka, kc = P.profile_key(middle, pa), P.profile_key(middle, pc) + require((ka, kc) in P.compatible_keys({ka: [pa]}, {kc: [pc]}), f'planted cross join lost in {key}') + + # 3. Verify same-label nilpotent dirty compression vs cross-label failure in M_3(F_2[UT_4(F_2)]) + same_label_pairs = 0 + dirty_col_mask = outer(1, 4, 3) # u=(1,0,0)^T, v=(0,0,1) + dirty_row_mask = outer(4, 1, 3) # u=(0,0,1)^T, v=(1,0,0) + both_dirty_masks = [ + outer(1, 5, 3), + outer(5, 1, 3), + outer(5, 5, 3), + dirty_col_mask, + dirty_row_mask, + ] + for letter in ('a', 'c'): + for m1, m2 in product(both_dirty_masks, repeat=2): + w3 = [(letter, m1), (letter, m2)] + actual = formal(w3, 3) + w2 = [(letter, project_3to2(m)) for _, m in w3 if project_3to2(m)] + compressed = formal(w2, 2) + require([row[:2] for row in actual[:2]] == compressed, + 'same-label nilpotent dirty compression failed') + same_label_pairs += 1 + mixed_ac = formal([('a', dirty_col_mask), ('c', dirty_row_mask)], 3) + require(mixed_ac[0][0] != {0}, 'cross-label dirty contraction failed to fire') + + # 4. Verify independent 3-role subsequence oracle against fast 3-role (5,5,5) formulas + non_adjacent_ac_classes = { + '', 'a', 'b', 'c', 'ab', 'ba', 'bc', 'cb', + 'aba', 'abc', 'bab', 'bcb', 'cba', 'cbc', + } + for mode, fixture in result['planted_controls']['three_role_555'].items(): + middle = tuple(fixture['middle']) + pa, pc = tuple(fixture['a_profile']), tuple(fixture['c_profile']) + da_prof = tuple(fixture['dirty_a_profile']) + dc_prof = tuple(fixture['dirty_c_profile']) + word_xy = fixture['word_xy'] + word3 = tuple((letter, outer(x3, y3, 3)) for letter, x3, y3 in word_xy) + word2 = tuple((letter, project_3to2(m3)) for letter, m3 in word3 if project_3to2(m3)) + q2 = quotient_2role(word2) + q3 = quotient_3role(word3) + for cls in non_adjacent_ac_classes: + require(project_3to2(q3.get(cls, 0)) == q2.get(cls, 0) == P.TARGET.get(cls, 0), + f'3-role non-adjacent-ac class {cls} disagreement in {mode}') + is_case_I = (mode == 'case_I_col_a_row_c') + if is_case_I: + for cls in ('a', 'ab', 'aba', 'abc'): + require(extract_kh_vec(q3.get(cls, 0)) == 0, f'Case I KH {cls} nonzero') + for cls in ('c', 'bc', 'cbc', 'cba'): + require(extract_hk_vec(q3.get(cls, 0)) == 0, f'Case I HK {cls} nonzero') + else: + for cls in ('a', 'ba', 'aba', 'cba'): + require(extract_hk_vec(q3.get(cls, 0)) == 0, f'Case II HK {cls} nonzero') + for cls in ('c', 'cb', 'cbc', 'abc'): + require(extract_kh_vec(q3.get(cls, 0)) == 0, f'Case II KH {cls} nonzero') + + # Recompute exact (H, H) AC, ACB, BAC via eval_base_3role_hh + within-gap joint qac + sa_g = C.profile_gaps(pa) + sc_g = C.profile_gaps(pc) + da_g = C.profile_gaps(da_prof) + dc_g = C.profile_gaps(dc_prof) + b_ac, b_acb, b_bac = C.eval_base_3role_hh(P, middle, sa_g, da_g, sc_g, dc_g, is_case_I) + # Because first_3role_word places all a-calls before all c-calls in each gap g, + # the within-gap q_ac contribution in gap g is sum_{c in gap g} (sa_g[g]*nc + extra) = sa_g[g]*sc_g[g] + (dc_g[g]*da_g[g] if not is_case_I else 0) + b_pref = (0, middle[0], middle[0] ^ middle[1], + middle[0] ^ middle[1] ^ middle[2], + middle[0] ^ middle[1] ^ middle[2] ^ middle[3], 0) + for g in range(6): + qg = P.MULT[sa_g[g]][sc_g[g]] ^ (0 if is_case_I else P.MULT[da_g[g]][dc_g[g]]) + b_ac ^= qg + b_acb ^= P.MULT[qg][b_pref[g]] + b_bac ^= P.MULT[b_pref[g]][qg] + require(project_3to2(q3.get('ac', 0)) == b_ac, f'3-role HH AC formula mismatch in {mode}') + require(project_3to2(q3.get('acb', 0)) == b_acb, f'3-role HH ACB formula mismatch in {mode}') + require(project_3to2(q3.get('bac', 0)) == b_bac, f'3-role HH BAC formula mismatch in {mode}') + + # Negative control: perturb the first a-call's dirty bit and verify off-diagonal violation + bad_xy = [list(step) for step in word_xy] + for idx, (letter, x3, y3) in enumerate(bad_xy): + if letter == 'a': + if is_case_I: + bad_xy[idx][1] = x3 ^ 4 + else: + bad_xy[idx][2] = y3 ^ 4 + break + bad_q3 = quotient_3role(tuple((l, outer(x, y, 3)) for l, x, y in bad_xy)) + if is_case_I: + require(any(extract_kh_vec(bad_q3.get(cls, 0)) != 0 for cls in ('a', 'ab', 'aba', 'abc')), + 'Case I perturbed dirty bit not detected by 3-role oracle') + else: + require(any(extract_hk_vec(bad_q3.get(cls, 0)) != 0 for cls in ('a', 'ba', 'aba', 'cba')), + 'Case II perturbed dirty bit not detected by 3-role oracle') + + # 5. Verify 15-call span-rank excess profiles and five-b classification + span_profiles_15 = [ + ranks for ranks in product(range(2, 6), repeat=6) + if 1 + sum(ranks) <= 15 + ] + require(len(span_profiles_15) == 28, '15-call span profile count mismatch') + five_b_exact_excess = [ + (eax, eay, ebx, eby, ecx, ecy) + for eax, eay, ebx, eby, ecx, ecy in product(range(3), repeat=6) + if ebx == 0 and eby == 0 and eax + eay + ecx + ecy == 2 + ] + require(len(five_b_exact_excess) == 10, 'five-b excess-2 profile count mismatch') + split_654 = [e for e in five_b_exact_excess if e[0] + e[1] == 2] + split_456 = [e for e in five_b_exact_excess if e[4] + e[5] == 2] + split_555 = [e for e in five_b_exact_excess if e[0] + e[1] == 1 and e[4] + e[5] == 1] + require(len(split_654) == 3 and len(split_456) == 3 and len(split_555) == 4, + 'five-b excess-2 split partition mismatch') + + # 6. Verify weighted price envelope and (1,3,1) sharpness + price_cases = 0 + for alpha, beta, gamma in product(range(6), repeat=3): + direct = 4 * alpha + 6 * beta + 4 * gamma + bound = min(direct, 4 * alpha + 5 * beta + 4 * gamma + 3 * min(alpha, gamma)) + relaxed = min( + a * alpha + b * beta + c * gamma + for a, b, c in product(range(4, 13), range(5, 13), range(4, 13)) + if b >= 6 or a + c >= 11 + ) + require(bound == relaxed, 'weighted lower-envelope arithmetic mismatch') + if beta <= 3 * min(alpha, gamma): + require(bound == direct, 'sharp price cone mismatch') + price_cases += 1 + require(4 * 1 + 6 * 3 + 4 * 1 == 26 and 4 * 1 + 5 * 3 + 4 * 1 + 3 * 1 == 26, + '(1,3,1) boundary equality failed') + require(min(4 + 24 + 4, 4 + 20 + 4 + 3) == 31 < 32, + 'outside-cone (1,4,1) false sharpness control failed') + + print('PASS_UT4_FIFTEEN_CALL_CONTROLS', json.dumps(dict( + literal_group_products=4096, + short_quotient_words=short, + profile_rank_sum_total=sum(rank_hist), + four_call_realizations=55566, + five_call_realizations=907200, + six_call_profiles=len(by_max_rank[6]), + planted_2role_domains=len(result['planted_controls']['two_role']), + same_label_nilpotent_pairs=same_label_pairs, + cross_label_dirty_detected=True, + planted_3role_modes=len(result['planted_controls']['three_role_555']), + span_profiles_15=len(span_profiles_15), + price_grids=price_cases, + price_1_3_1_minimum=26, + outside_cone_sharpness_rejected=True, + ), sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/ut4-fifteen-call-five-b/vendor/predecessor.py b/research/ut4-fifteen-call-five-b/vendor/predecessor.py new file mode 100644 index 0000000000..87eb17255d --- /dev/null +++ b/research/ut4-fifteen-call-five-b/vendor/predecessor.py @@ -0,0 +1,348 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact z/uz UT4 tariff census. No physical supplier or kappa claim. + +The profile-screen method is credited to Aaron Wang's PR1690. This implementation +uses concrete gap placements rather than its recursive profile reconstruction. +Every loop has a fixed finite domain: two roles, four outer calls, five middle +calls, the 64-element group and the degree-three quotient. +""" +from collections import defaultdict +from hashlib import sha256 +from itertools import combinations, combinations_with_replacement, product +import argparse +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASIS = ('', 'a', 'b', 'c', 'ab', 'ac', 'ba', 'bc', 'cb', + 'aba', 'abc', 'acb', 'bab', 'bac', 'bcb', 'cba', 'cbc') +TARGET = {'': 9, 'ab': 8, 'ba': 8, 'aba': 8, 'bab': 8, + 'abc': 9, 'acb': 9, 'bac': 9, 'cba': 9} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False).encode() + + +def mm(a, b): + """Binary 2x2 product, with bit 2*i+j encoding entry i,j.""" + return sum(((sum(((a >> (2 * i + k)) & 1) * ((b >> (2 * k + j)) & 1) + for k in range(2)) & 1) << (2 * i + j)) + for i in range(2) for j in range(2)) + + +MULT = tuple(tuple(mm(a, b) for b in range(16)) for a in range(16)) +OUTER = {(x, y): sum((((x >> i) & 1) * ((y >> j) & 1)) << (2 * i + j) + for i in range(2) for j in range(2)) + for x in range(1, 4) for y in range(1, 4)} +SPLIT = {n: pair for pair, n in OUTER.items()} +COUPLINGS = tuple(sorted(SPLIT)) + + +def total(sequence): + value = 0 + for n in sequence: + value ^= n + return value + + +def reduced(word): + if len(word) > 3: + return None + for _ in range(3): + word = word.replace('ca', 'ac') + require('ca' not in word, 'quotient reduction bound') + if any(word[i] == word[i + 1] for i in range(len(word) - 1)): + return None + require(word in BASIS, 'quotient basis') + return word + + +def q_product(left, right): + result = set() + for a in left: + for b in right: + word = reduced(a + b) + if word is not None: + result.symmetric_difference_update((word,)) + return frozenset(result) + + +def group_product(g, h): + a, b, c, d, e, f = ((g >> i) & 1 for i in range(6)) + aa, bb, cc, dd, ee, ff = ((h >> i) & 1 for i in range(6)) + values = (a ^ aa, b ^ bb, c ^ cc, d ^ dd ^ (a & bb), + e ^ ee ^ (b & cc), f ^ ff ^ (a & ee) ^ (d & cc)) + return sum(value << i for i, value in enumerate(values)) + + +def fixed_algebra(): + """Construct the group-to-quotient map and check every multiplication.""" + images = {0: frozenset(('',))} + queue = [0] + for index in range(64): + require(index < len(queue), 'group generation') + g = queue[index] + for letter, generator in zip('abc', (1, 2, 4)): + h = group_product(g, generator) + value = q_product(images[g], frozenset(('', letter))) + if h not in images: + images[h] = value + queue.append(h) + require(images[h] == value, 'consistent group image') + require(len(images) == 64, 'all group elements') + for g, h in product(range(64), repeat=2): + require(q_product(images[g], images[h]) == images[group_product(g, h)], + 'quotient homomorphism') + for a, b, c in product(BASIS, repeat=3): + aa, bb, cc = (frozenset((s,)) for s in (a, b, c)) + require(q_product(q_product(aa, bb), cc) == q_product(aa, q_product(bb, cc)), + 'quotient associativity') + require(images[32] == frozenset(('', 'abc', 'acb', 'bac', 'cba')), 'z image') + require(images[40] == frozenset(TARGET), 'uz image') + return {'group_products': 4096, 'quotient_associativity': 4913} + + +def quotient(word): + require(len(word) <= 14, 'word length bound') + result = {'': 9} + for letter, n in word: + require(letter in 'abc' and n in SPLIT, 'paid alphabet') + updated = dict(result) + for monomial, matrix in result.items(): + name = reduced(monomial + letter) + if name is not None: + updated[name] = updated.get(name, 0) ^ MULT[matrix][n] + result = {name: matrix for name, matrix in updated.items() if matrix} + return result + + +def gap_catalogue(): + """All four-call outer words, in all six gaps, retaining realizations.""" + catalogue = defaultdict(list) + zero_sequences = 0 + for ns in product(COUPLINGS, repeat=4): + if total(ns): + continue + zero_sequences += 1 + for positions in combinations_with_replacement(range(6), 4): + sums = [0] * 6 + for n, gap in zip(ns, positions): + sums[gap] ^= n + profile, running = [], 0 + for gap in range(5): + running ^= sums[gap] + profile.append(running) + catalogue[tuple(profile)].append((ns, positions)) + return dict(catalogue), zero_sequences + + +def side_table(middle): + """Packed AB, BA, ABA, BAB coefficients of a zero-total outer profile.""" + result = [] + for j, n in enumerate(middle): + left, right = total(middle[:j]), total(middle[j + 1:]) + row = [] + for p in range(16): + pn, np = MULT[p][n], MULT[n][p] + bab = MULT[MULT[left][p]][n] ^ MULT[np][right] + row.append(pn | (np << 4) | (MULT[pn][p] << 8) | (bab << 12)) + result.append(row) + return result + + +def profile_key(middle, profile): + """Column/row bit strings for each transported middle coupling.""" + u0 = u1 = w0 = w1 = 0 + for j, (n, p) in enumerate(zip(middle, profile)): + x, y = SPLIT[n] + px = ((p & 1) * (x & 1)) ^ (((p >> 1) & 1) * ((x >> 1) & 1)) + px |= ((((p >> 2) & 1) * (x & 1)) ^ (((p >> 3) & 1) * ((x >> 1) & 1))) << 1 + yp = ((y & 1) * (p & 1)) ^ (((y >> 1) & 1) * ((p >> 2) & 1)) + yp |= (((y & 1) * ((p >> 1) & 1)) ^ (((y >> 1) & 1) * ((p >> 3) & 1))) << 1 + u0 |= (px & 1) << j + u1 |= (px >> 1) << j + w0 |= (yp & 1) << j + w1 |= (yp >> 1) << j + return u0, u1, w0, w1 + + +def cross_key(a, c): + abc = cba = 0 + for i, j in product(range(2), repeat=2): + abc |= ((a[i] & c[2 + j]).bit_count() & 1) << (2 * i + j) + cba |= ((c[i] & a[2 + j]).bit_count() & 1) << (2 * i + j) + return abc, cba + + +def screened_profiles(middle, profiles): + table = side_table(middle) + a, c = defaultdict(list), defaultdict(list) + for profile in profiles: + value = table[0][profile[0]] ^ table[1][profile[1]] ^ table[2][profile[2]] + value ^= table[3][profile[3]] ^ table[4][profile[4]] + if value == 0x8888: + a[profile_key(middle, profile)].append(profile) + if value == 0: + c[profile_key(middle, profile)].append(profile) + return dict(a), dict(c) + + +def compatible_keys(a_keys, c_keys): + by_rows = defaultdict(list) + for key in c_keys: + by_rows[key[2:]].append(key) + for a in a_keys: + first = [m for m in range(32) if (a[0] & m).bit_count() % 2 == 1 + and (a[1] & m).bit_count() % 2 == 0] + second = [m for m in range(32) if (a[0] & m).bit_count() % 2 == 0 + and (a[1] & m).bit_count() % 2 == 1] + for m0, m1 in product(first, second): + for c in by_rows.get((m0, m1), ()): + if cross_key(a, c) == (9, 9): + yield a, c + + +def gap_words(realization, letter): + ns, positions = realization + return tuple(tuple((letter, n) for n, position in zip(ns, positions) if position == gap) + for gap in range(6)) + + +def interleavings(a, c): + result = [] + for positions in combinations(range(len(a) + len(c)), len(a)): + chosen = set(positions) + ia = ic = 0 + word = [] + for index in range(len(a) + len(c)): + if index in chosen: + word.append(a[ia]) + ia += 1 + else: + word.append(c[ic]) + ic += 1 + result.append(tuple(word)) + return tuple(result) + + +def expanded_words(middle, a_realization, c_realization): + a, c = gap_words(a_realization, 'a'), gap_words(c_realization, 'c') + alternatives = tuple(interleavings(aa, cc) for aa, cc in zip(a, c)) + for parts in product(*alternatives): + word = [] + for j in range(6): + word.extend(parts[j]) + if j < 5: + word.append(('b', middle[j])) + yield tuple(word) + + +def census(): + catalogue, zero_sequences = gap_catalogue() + profiles = tuple(sorted(catalogue)) + counts = dict(middles=0, outer_zero_sequences=zero_sequences, profiles=len(profiles), + a_pass=0, c_pass=0, key_pairs=0, profile_pairs=0, words=0, q_pass=0) + digest = sha256() + failures = defaultdict(int) + for middle in product(COUPLINGS, repeat=5): + if total(middle): + continue + counts['middles'] += 1 + a, c = screened_profiles(middle, profiles) + counts['a_pass'] += sum(len(ps) for ps in a.values()) + counts['c_pass'] += sum(len(ps) for ps in c.values()) + for ka, kc in compatible_keys(a, c): + counts['key_pairs'] += 1 + for pa, pc in product(a[ka], c[kc]): + counts['profile_pairs'] += 1 + for ra, rc in product(catalogue[pa], catalogue[pc]): + for word in expanded_words(middle, ra, rc): + image = quotient(word) + counts['words'] += 1 + counts['q_pass'] += image == TARGET + differing = [s for s in BASIS if image.get(s, 0) != TARGET.get(s, 0)] + require(differing, 'unexpected 13-call quotient solution') + failures[differing[0]] += 1 + digest.update(canonical([word, sorted(image.items())]) + b'\n') + counts['expanded_transcript_sha256'] = digest.hexdigest() + counts['first_differing_coefficient'] = dict(sorted(failures.items())) + return counts + + +def formal(word, roles=3): + """Full group-ring operator, including one arbitrary dirty role by default.""" + require(2 <= roles <= 5 and len(word) <= 14, 'formal fixture bound') + result = [[{0} if i == j else set() for j in range(roles)] for i in range(roles)] + generators = {'a': 1, 'b': 2, 'c': 4} + for letter, n in word: + require(letter in generators and n in SPLIT, 'paid formal alphabet') + x, y = SPLIT[n] + for i in range(roles): + increment = set() + for k in range(2): + if (x >> k) & 1: + for g in result[i][k]: + increment.symmetric_difference_update((g, group_product(g, generators[letter]))) + for j in range(2): + if (y >> j) & 1: + result[i][j].symmetric_difference_update(increment) + return [[sorted(entry) for entry in row] for row in result] + + +def positive_and_controls(): + word = tuple((letter, n) for letters, n in (('abcbabcb', 1), ('acbabc', 8)) + for letter in letters) + expected = [[([32, 40, 0][i:i + 1] if i == j else []) for j in range(3)] for i in range(3)] + require(formal(word) == expected and quotient(word) == TARGET, '14-call full formal witness') + for index in range(14): + omitted = word[:index] + word[index + 1:] + require(formal(omitted) != expected, 'omitted-call control') + changed = list(word) + changed[0] = ('c', changed[0][1]) + require(formal(changed) != expected, 'wrong-letter control') + return {'full_word': [list(step) for step in word], 'formal_roles': 3, 'formal_basis_columns': 192, + 'omitted_call_controls': 14, 'wrong_letter_controls': 1} + + +def check_sources(): + sources = json.loads((HERE / 'SOURCES.json').read_text()) + for item in sources['files']: + if item['usage'] == 'input': + data = (ROOT / item['path']).read_bytes() + require(sha256(data).hexdigest() == item['sha256'], 'source digest: ' + item['path']) + + +def check_receipt(actual, path): + expected = json.loads(path.read_text()) + require(canonical(actual) == canonical(expected), 'receipt mismatch') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', type=Path, help='write a receipt to a new path') + args = parser.parse_args() + if args.emit: + require(not args.emit.exists(), 'refuse existing receipt') + check_sources() + result = {'algebra': fixed_algebra(), 'positive': positive_and_controls(), 'census': census()} + if args.emit: + payload = json.dumps(result, sort_keys=True, indent=2) + '\n' + with args.emit.open('x') as output: + require(output.write(payload) == len(payload), 'receipt write length') + else: + check_receipt(result, HERE / 'EXPECTED.json') + counts = result['census'] + print('PASS_UT4_MIXED_CENTRAL_MIDDLE minimum=14 ' + f"middles={counts['middles']} words={counts['words']} q_pass={counts['q_pass']} no_new_kappa") + + +if __name__ == '__main__': + main() diff --git a/research/ut4-fifteen-call-five-b/verify.py b/research/ut4-fifteen-call-five-b/verify.py new file mode 100644 index 0000000000..e1efeb8d8a --- /dev/null +++ b/research/ut4-fifteen-call-five-b/verify.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Full finite 2-role and 3-role quotient censuses for the 15-call five-b UT4 boundary.""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location('ut4_fifteen_call_census', HERE / 'census.py') +C = importlib.util.module_from_spec(spec) +spec.loader.exec_module(C) + + +def verify(): + P, source = C.load() + algebra = P.fixed_algebra() + positive = P.positive_and_controls() + result = C.run(P, progress=True) + + old_2175 = source['predecessor_receipt']['data'] + C.require(algebra == old_2175['algebra'] and positive == old_2175['positive'], + 'predecessor PR2175 algebra/positive control mismatch') + + old_2314 = json.loads((ROOT / 'research/ut4-mixed-weighted-boundary/RESULT.json').read_text(encoding='utf-8')) + for key in ('4,5,4', '5,5,4', '4,5,5'): + for field in ('middles', 'a_pass', 'c_pass', 'key_pairs', 'profile_pairs', + 'words', 'q_pass', 'first_differing_coefficient'): + C.require(result['domains'][key][field] == old_2314['domains'][key][field], + f'predecessor PR2314 domain {key} field {field} mismatch') + + old_2343 = json.loads((ROOT / 'research/register-pairing-compression/RESULT.json').read_text(encoding='utf-8')) + C.require(old_2343['ut4_consequence']['only_cheaper_count_splits'] == [[4, 5, 6], [5, 5, 5], [6, 5, 4]] + and old_2343['ut4_consequence']['fifteen_call_existence_decided'] is False, + 'predecessor PR2343 open-splits handoff mismatch') + + C.require(result['outer_catalogues'] == { + '4': dict(zero_sequences=441, profiles=9721, realizations=55566), + '5': dict(zero_sequences=3600, profiles=47521, realizations=907200), + '6': dict(zero_sequences=33489, profiles=174670, realizations=15471918), + }, 'complete outer inventory mismatch') + + C.require(sum(result['domains'][k]['words'] for k in ('6,5,4', '5,5,5', '4,5,6')) == 20579840, + 'new 15-call two-role word count mismatch') + C.require(all(result['domains'][k]['q_pass'] == 0 for k in ('6,5,4', '5,5,5', '4,5,6')), + 'unexpected two-role quotient survivor') + + for mode in ('case_I_col_a_row_c', 'case_II_row_a_col_c'): + st3 = result['three_role_555'][mode] + C.require(st3['active_profile_pairs'] == 5664 and st3['dirty_profile_pairs'] == 17864 + and st3['words'] == 42447616 and st3['hh_q_pass'] == 0, + f'three-role (5,5,5) {mode} census mismatch') + + result.update( + status='PASS_UT4_FIFTEEN_CALL_FIVE_B', + algebra=algebra, + positive=positive, + scope=( + 'Formal F2[UT4(F2)] register-model theorem and complete necessary-quotient ' + 'rejection for all 15-call five-b splits across arbitrary finite restored ' + 'dirty workspaces; no native supplier or new kappa.' + ), + theorem=dict( + target='diag([z],[uz],I_rest)', + arbitrary_finite_restored_dirty_workspace=True, + excluded_fifteen_call_five_b_splits=[[6, 5, 4], [5, 5, 5], [4, 5, 6]], + all_fifteen_call_words_have_b_at_least_six=True, + five_b_calls_require_at_least_eleven_outer_calls=True, + five_b_calls_require_at_least_sixteen_total_calls=True, + weighted_lower_bound='min(4 alpha+6 beta+4 gamma, 4 alpha+5 beta+4 gamma+3 min(alpha,gamma))', + sharp_price_region='alpha,beta,gamma>=0 and beta<=3 min(alpha,gamma)', + exact_price_in_region='4 alpha+6 beta+4 gamma', + price_1_3_1_exact_minimum=26, + price_1_3_1_cost_25_impossible=True, + uniform_quantifiers_supplied_by='PROOF.md, not finite role extrapolation', + ), + ) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-result', action='store_true') + args = parser.parse_args() + result = json.loads(json.dumps(verify())) + path = HERE / 'RESULT.json' + if args.write_result: + path.write_text(json.dumps(result, sort_keys=True, indent=2) + '\n', encoding='utf-8') + else: + C.require(result == json.loads(path.read_text(encoding='utf-8')), + 'recorded result differs from full replay') + digest = hashlib.sha256(json.dumps(result, sort_keys=True, separators=(',', ':')).encode('utf-8')).hexdigest() + print(result['status'], 'new_two_role_words=20579840', 'three_role_555_words=84895232', 'receipt=' + digest) + + +if __name__ == '__main__': + main()