diff --git a/research/bit-twisted-feedback-contamination-lemma/PROOF.md b/research/bit-twisted-feedback-contamination-lemma/PROOF.md new file mode 100644 index 0000000000..4b1b5f67c1 --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/PROOF.md @@ -0,0 +1,157 @@ +# Contamination-charge lemma for every word + +## Setting + +There are `n = H + Y` registers over F2: helpers `0..H-1`, then targets `H..n-1`. +All inputs are dirty. A state is a matrix `M` in `GL_n(F2)`. Row `r` is the +linear form held by register `r`. A gate `(d,s)` means `r[d] ^= r[s]`, with +`d != s` and cost one. It replaces row `d` by row `d` plus row `s`. + +`P = P_{H,Y}` is the set of invertible `M` whose helper rows do not depend on +target inputs. These are the block lower-triangular matrices `[[A,0],[C,D]]`. +The restricted alphabet omits feedback gates (a helper destination with a target +source). The restricted gates generate `P`. Every twisted exit +`[[T,0],[K,I_Y]]` lies in `P`. `d_P` is the restricted minimum and `d_full` the +unrestricted minimum, so `d_full <= d_P` on `P`. + +## Construction + +The construction maintains three objects: + +* a permutation `phi` from physical registers to virtual registers; +* an `H x Y` matrix `Z` (the contamination); +* the state `N` of an emitted restricted word. + +It starts with `phi = id`, `Z = 0`, `N = I`. Write `c_b` for helper row `b` of +`N` and `t_j` for target row `j`. The invariant is: + +> **(INV)** physical register `r` holds virtual content `v_{phi(r)}`, where +> virtual helper `b` holds `c_b + Z_b t` and virtual target `j` holds `t_j`. +> Equivalently, `M = Pi_phi U(Z) N`, with `U(Z) = [[I,Z],[0,I]]` and +> `(Pi_phi X)_r = X_{phi(r)}`. + +The invariant fixes a decomposition of the state; `N` itself always lies in `P`. +A physical gate `(d,s)` acts on the virtual contents as the gate +`(phi(d), phi(s))`. Below, `z = Z_a` is a row and `col = Z[:,i]` is a column. +`|.|` counts ones. Each case lists the emitted restricted gates, the update, and +the reason INV still holds. + +1. **Virtual feedback** `h_a ^= y_j`. Emit nothing. Set `Z_a += e_j`. Virtual + helper `a` becomes `c_a + (Z_a + e_j) t`. +2. **Helper mixing** `h_a ^= h_b`. Emit `(a,b)`. Set `Z_a += Z_b`. Helper `a` + becomes `(c_a + c_b) + (Z_a + Z_b) t`. +3. **Target mixing** `y_i ^= y_j`. Emit `(H+i, H+j)`. Add column `i` of `Z` to + column `j`. With `t'_i = t_i + t_j`, we have `t_i = t'_i + t'_j`. So + `Z_b t = Z_b' t'`, where `Z_b'[j] = Z_b[j] + Z_b[i]`. +4. **Read** `y_i ^= h_a` with `z_i = 0`. + * Emit `(H+i, H+j)` for each `j` in `supp z`, then `(H+i, a)`, then + `(b, a)` for each `b` in `supp col`. This costs `1 + |z| + |col|`. + * Set `Z += col z`. + * The new target is `t'_i = t_i + c_a + z t`. It equals the actual read + result `t_i + (c_a + z t)`. Because `z_i = 0`, `z t = z t'`, so + `t_i = t'_i + c_a + z t'`. + * Substitute this into helper `b`, which holds `c_b + Z_b t`. It becomes + `(c_b + col_b c_a) + (Z_b + col_b z) t'`. That matches the emitted + `c_b ^= c_a`. + * When `z = 0` and `col = 0`, the read is **clean**: it emits only itself. + Otherwise (`z` or `col` nonzero) the read is **contaminated**. +5. **Singular read** `y_i ^= h_a` with `z_i = 1`. + * The actual target becomes `t_i + c_a + z t = c_a + z' t`, with + `z' = z + e_i`. The term `t_i` cancels, so the virtual target block + loses rank. When `phi` preserves the blocks (for example at the first + singular read), the physical target-input block of `M` loses rank too, + and a frame read off `M` alone (helper rows minus a multiple of the + target rows, which needs an invertible target block) does not exist + there. Exchanging helper `a` and target `i` keeps INV in every case. + * Emit `(H+i, H+j)` for each `j` in `supp z'`, then `(H+i, a)`, then + `(b, a)` for each `b` in `supp col` other than `a`. This costs + `|z| + |col| - 1`. The new `N` has `t'_i = t_i + c_a + z' t`, so it stays + in `P`. + * Exchange the roles of virtual helper `a` and virtual target `i`, so + `phi <- sigma o phi` with `sigma = (a, H+i)`. Set `Z_a <- z'`, and + `Z_b <- Z_b + col_b z'` for `b != a`. + * Check INV. The new virtual target `i` is the unchanged physical content + of old helper `a`. That content is `c_a + t_i + z' t = t'_i`. + * The new virtual helper `a` is the read result `c_a + z' t`. Since + `z'_i = 0`, this equals `c_a + z' t'`. + * Every other helper `b` held `c_b + col_b t_i + sum_{j != i} Z_b[j] t_j`. + Substitute `t_i = t'_i + c_a + z' t'`. It becomes + `(c_b + col_b c_a) + (Z_b + col_b z') t'`. + +**End of the word.** Suppose `M_L` is in `P`. Since `N_L` is also in `P`, the +frame `Pi_phi U(Z)` is in `P`. Its helper rows have no target columns. + +* A helper row is either `Z_b` (if `phi(r) = b < H`) or `e_j` (if `phi(r)` is + a target). So `phi` maps helpers to helpers, and `Z = 0`. +* Hence `M_L = Pi_phi N_L`. Fix this by permuting registers inside each block. + Each transposition is a three-XOR swap, which is a restricted word. +* The number of transpositions is `n - cyc(phi)`. + +## Lemma + +Let `w` be any word of length `L` whose product `M` lies in `P`. The +construction outputs a restricted word computing exactly `M` with length + +`L - f_v + c(w)`, where + +`c(w) = sum_{contaminated reads} (|z| + |col|) + sum_{singular reads} (|z| + |col| - 2) + 3 (n - cyc(phi_L))` + +Here `f_v` counts virtual feedback gates (case 1). Hence `d_P(M) <= L - f_v + c(w)`. + +No step assumes that a target block is invertible. Case 5 is the singular +case. Every term of `c` is nonnegative: in case 5, `|z| >= 1` and `|col| >= 1`. + +## Corollaries + +1. **Deletion.** Suppose every read is clean (`Z_a = 0` and `Z[:,i] = 0` at + the read). Then case 5 never occurs, `phi = id`, `f_v` equals the number + `f` of feedback gates, and `c = 0`. The restricted word is `w` with its + feedback gates deleted. So `d_P(M) <= L - f`. +2. **Where a gain must come from.** Suppose `d_full(M) < d_P(M)`, and let `w` + be a minimum unrestricted word for `M`. + * `w` contains feedback, since otherwise it would be restricted. + * Its first feedback gate occurs while `Z = 0`, so `phi = id` then. Hence + `f_v >= 1`. + * Then `c(w) >= d_P(M) - L + f_v >= 2`. So `w` has a contaminated or + singular read. +3. If `c(w) <= f_v(w)` for some word `w` of length `L` for `M`, then + `d_P(M) <= L`. + +A singular read can have surcharge `0` (for example `z = e_i`, `col = e_a`). +So `c(w) = 0` does not imply that every read is clean. The converse in +Corollary 1 is what holds. + +## Mechanical corroboration + +`lemma.py` asserts INV after every gate and the length identity at the end. +`verify.py` checks the following words: + +* For every element of every `P_{H,Y}` with `n <= 4`: one BFS-minimum + unrestricted word and one random-detour word, 6,628 words in total. For each, + the output reproduces `M` and `d_P(M) <= |output|`. +* 8,400 random words ending in `P` with `n = 2..8`, over every split; half + are forced to exits `[[T,0],[K,I]]` with random `T`, and 3,998 end at + twisted exits (`T != I`). +* 2,800 free random words, where only the per-gate invariant is checked. +* Together these words exercise 2,946 words with singular reads, 1,612 words + with relabel swaps and 4,705 words with contaminated reads. + +`numpy_crosscheck.py` runs the construction on one greedy (first-gate) minimum +unrestricted word for each of the 333,712 five-register exits `[[T,0],[K,I]]` +(333,552 twisted plus 160 settled `T = I` shears). In 35 of the 4+1 words the +construction meets a non-clean read, and each has `c = f_v + 1`: the +construction outputs a restricted word of length `L + 1`, so the lemma alone +does not certify those 35 exits. The census does (`d_P = d_full = L`). Which +words are non-clean depends on the greedy choice of minimum word. + +As a positive control, `numpy_crosscheck.py` also finds every element of the +five-register `P_{H,Y}` where feedback strictly helps: exactly 120 (60 in +`P_{2,3}`, 60 in `P_{3,2}`), each with gap 1 and none an exit (target block +`D != I`). On one greedy minimum word of each it asserts Corollary 2: +`f_v >= 1`, a non-clean read, and `c >= f_v + 1`. + +`verify.py` reports `lemma_words = 15,028`: the 6,628 + 8,400 words ending in +`P`. The 2,800 free words check only the per-gate invariant. + +This is a written proof plus finite corroboration. It was reviewed only by AI +passes in the same loop; there is no human review and no formal (Lean) proof. diff --git a/research/bit-twisted-feedback-contamination-lemma/README.md b/research/bit-twisted-feedback-contamination-lemma/README.md new file mode 100644 index 0000000000..63b12b735a --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/README.md @@ -0,0 +1,215 @@ +# Twisted helper exits: no target-to-helper feedback gain at any fixed 3+3 or five-register exit, plus an every-word contamination-charge lemma + +**Scoped proof plus finite certificates. No new supplier, no κ effect, no selected-frontier change.** + +1. **Lemma (every word; written proof in [PROOF.md](PROOF.md)).** + * *Setting:* `H` helpers and `Y` targets, dirty inputs, unit-cost directed + XORs. `P = P_{H,Y}` is the restricted (no target→helper) group, and it + contains every exit `[[T,0],[K,I]]` (identity target block). An exit is + *twisted* when `T != I`; `T = I` exits are the untwisted shears. + * *Construction:* for any word `w` of length `L` whose product `M` lies in + `P`, an explicit tracking construction outputs a restricted word computing + exactly `M`. Its length is `L - f_v + c(w)`. + * `f_v` counts the feedback gates the construction absorbs. + * `c(w)` is an explicit contamination charge (see below). + * The tracked state is a contamination matrix `Z` plus a virtual + register labelling. + * *The charge:* + * A nonsingular contaminated read `y_i ^= h_a` (`Z[a,i] = 0`, with + `Z_a`, `Z[:,i]` not both zero) costs `|Z_a| + |Z[:,i]|` extra. + * A singular read (`Z[a,i] = 1`) costs `|Z_a| + |Z[:,i]| - 2` extra. + * A read with `Z_a = 0` and `Z[:,i] = 0` is *clean* and costs nothing + extra. "Non-clean" means contaminated or singular. + * Restoring the final labelling costs 3 per swap. + * *No invertible-target-block hypothesis.* A frame read off the current matrix alone + would need an invertible target block, which fails after `h ^= y; y ^= h`. + The singular-read step handles this by exchanging the roles of one helper + and one target. + * *Corollaries:* + * If every read is clean, deleting all feedback gates gives a restricted + word: `d_P(M) <= L - f`. + * Any strict feedback advantage needs every minimum unrestricted word to + have `c(w) >= f_v + 1 >= 2`, so it must contain a non-clean + (contaminated or singular) read. This is only a necessary condition: + 35 minimum words below already satisfy it at exits with no advantage. + * *Positive control:* feedback does help at some non-exit elements of + `P`, so the exit condition (target block `D = I`) is load-bearing. In + the five-register model exactly 120 elements of `P` have + `d_full = d_P - 1`: 60 in `P_{2,3}` and 60 in `P_{3,2}`, none an exit + (all have `D != I`); `P_{1,4}` and `P_{4,1}` have none. Corollary 2 + holds on a minimum word of each (`f_v >= 1`, a non-clean read and + `c >= f_v + 1`); `numpy_crosscheck.py` asserts all of this. +2. **3+3 decision (finite certificate).** + * All **85,504** exits `[[T,0],[K,I_3]]` with `T in GL_3(F2) \ {I}` were + checked. There is **no strict feedback advantage**: `d_full = d_P` for + every exit. + * The common minimum has distribution + `1:6, 2:96, 3:744, 4:3,594, 5:11,463, 6:23,948, 7:29,259, 8:15,438, 9:956` + (maximum 9). + * The 512 `T = I` shears are PR1306's census. They are cited, not + re-claimed; the run agrees with it (0 advantage). +3. **Five-register shapes (finite certificate).** There is no strict advantage + for any of the **333,552** twisted exits in the new shapes: + + | Shape | Twisted exits | Maximum minimum (twisted) | Settled `T = I` shears also run | + |---|---:|---:|---:| + | 2+3 | 320 | 6 | 64 (PR1306) | + | 3+2 | 10,688 | 8 | 64 (PR1306) | + | 4+1 | 322,544 | 10 | 16 (PR2567 `Y = 1` lemma) | + + The run also covers the 16 already-settled 1+4 exits (all `T = I`, PR2567), + so 333,712 exits in total; it agrees with the settled cases (0 advantage). + +**Decision informed.** PR1868 question 3 asks whether target-to-helper +feedback helps a replacement helper contract at fixed twisted exits. + +* *Closed here:* the fixed-exit question in PR1306's model for the 3+3 shape + (the 3x3 twisted case PR2494 left open) and for the twisted five-register + shapes 2+3, 3+2 and 4+1. With PR2494's `H + Y <= 4` census, this covers + every twisted shape with at most five registers. +* *Not closed:* the twisted 2+4, 4+2 and 5+1 shapes and anything larger; the + actual seed02 D boundary (at least 3 helpers and 99 targets), where only + Corollary 2's necessary condition applies; the C-absorption pricing in + question 3; and the twisted-versus-restored exit comparison. +* There is no κ effect either way, because the bit side does not bind + (`research/r439-twisted-star-absorption-seed02`). +* *Context only:* open PR #2721 (geckods) argues the framed transfer does not + use the no-target-feedback clause. This package is distinct and does not + depend on it; if that clause is relaxed, this result says feedback buys + nothing at fixed exits in these shapes. + +## What is new + +* Predecessors cover only these cases: + * ywz65's `research/bit-twisted-feedback-four-registers` (PR2494): + `H + Y <= 4`. + * PR1306 / PR1557 / PR1706 and rtyu193-rgb's + `bit-zero-frame-feedback-to-8-registers`: untwisted `T = I` shears, plus an + `H = 1` / `Y = 1` lemma. +* Why now: PR1868 question 3 explicitly asked for the 3x3 case and PR2494 + left it open; this package closes it with two independent exact methods. + The lemma explains the result structurally and certifies all but 35 of the + 333,712 greedy five-register minimum words directly; the five-register + census is a 30-second byproduct of the same run. (PR2494's "new lead" + condition asks for a favourable candidate word; none is claimed here.) +* New here: + * the every-word charge lemma (including singular steps); + * the twisted 3+3 domain; + * the twisted five-register shapes 2+3, 3+2 and 4+1. +* PR1306's substitution lemma is a different statement and is not reused. + +## Method and independence + +* **3+3, primary (stdlib, `independent33.py`).** + * Encoding: column-major. + * Restricted minima: right-multiplication meet-in-the-middle with restricted + balls `B^P_6 x B^P_3`. This is exact up to 9, and every exit has a word of + length at most 9. + * Unrestricted minima: `B_5 x B_3` in `GL_6(F2)`. This is exact up to 8, so + `d_full >= 9 = d_P` for the 956 exits with `d_P = 9`. + * Orbit reduction: helper/target relabelling (S3 x S3), 3,478 classes. +* **3+3, second method (`numpy_crosscheck.py`, numpy==2.5.4).** + * Restricted minima: dense BFS over all 14,450,688 elements of `P_{3,3}`. + * Unrestricted minima: row-major left multiplication against `B_4 x B_4`. + * Its own orbit canonicalisation also finds 3,478 classes. + * Both methods report the same class count, the same histograms and zero + strict advantages. Per-class results are not cross-joined between the + two scripts. `independent33.py` asserts that its restricted balls stay in + `P_{3,3}`, so it stands alone even though `d_full = d_P`. +* **Five registers.** Dense BFS over all 2^25 matrices (`GL_5`: 9,999,360 + elements) and over each parabolic. +* **Corroborating the lemma.** The construction is run on one greedy + (first-gate) minimum unrestricted word per five-register exit (333,712 + words). In 35 of the 4+1 words it meets a non-clean read, and each of those + has `c = f_v + 1`. So the lemma is not tight on them: it outputs a restricted + word of length `L + 1`, and those 35 exits are decided by the census + (`d_P = d_full = L`), not by the lemma. Which words are non-clean depends on + the greedy choice. `verify.py`'s `lemma_words = 15,028` counts the words + ending in `P` (6,628 + 8,400); the 2,800 free words check only the per-gate + invariant. +* All arithmetic is exact over F2. The 3+3 and five-register minima are global + minima: BFS uses unit weights and runs to exhaustion, and MITM splits every + word of length at most `a + b` at position `a`. + +## Reproduce + +From the repository root (Python 3.12; the registered replay installs only the pinned numpy): + +```sh +python3.12 scripts/research_package.py --package research/bit-twisted-feedback-contamination-lemma --install-deps +``` + +Expected lines: + +* `PASS_TWISTED_FEEDBACK_CONTAMINATION_LEMMA exits33=86016 twisted=85504 classes=3478 strict_feedback_advantage=0 max_restricted_min=9 lemma_words=15028 controls=5` + from `verify.py` (stdlib, about 40 s). +* `PASS_TWISTED_FEEDBACK_NUMPY_CROSSCHECK twisted33=85504 classes=3478 five_register_exits=333712 twisted5=333552 strict_feedback_advantage=0 lemma_words=333712 nonexit_advantage_controls=120` + from `numpy_crosscheck.py` (about 35 s, under 0.5 GB RSS). + +Run locally with system Python 3.14 (stdlib), and numpy 2.5.4 in a scratch venv. + +**Negative controls** (in `verify.py`; each must fail in the stated way): + +1. `h^=y; y^=h` makes the target block zero, so no frame can be read off the + matrix there, yet the construction covers the double-swap word with two + singular reads. +2. Naively deleting feedback from `h^=y0; y1^=h; h^=y0` gives the wrong map. +3. The charge is necessary on that word: `L - f = 1 < d_P = 2`. +4. A forged extra gate fails replay. +5. A self XOR is rejected. + +## Scope, inherited assumptions and unresolved obligations + +* *Model:* PR1306's algebraic model of fixed register labels, dirty inputs and + unit-cost XORs. There are no free permutations, COPY/ERASE, frames or extra + registers. +* *What is compared:* fixed exits `(T,K)`. Twisted and restored exits are not + interchangeable. +* *What remains open:* physical continuation and absorption of `T`, R439 + substitution, chronology across nonzero frames, hosting, precision/tape, + all-size compilation and native supplier replay. There is no general + no-feedback theorem beyond the lemma's statement, and no frontier change. +* *Review:* the lemma has no formal (Lean) proof. Review was by AI passes in + the same loop only; there was no human review. + +## Open next questions + +1. **Removing a non-clean read at zero net cost.** `c <= f_v` already fails + for some minimum words: the 35 greedy 4+1 words have `c = f_v + 1`, yet + their exits have equal-length restricted words. Is there a local rewriting + rule that turns a minimum word with a non-clean read into a restricted + word of the same length, at least for one-target (`Y = 1`) twisted exits + at every `H`? That would extend the decision beyond five registers. + Such a rule must use `D = I`: no zero-cost rule exists on all of `P`, + because 120 non-exit five-register elements have a strict feedback gain. + * *First step:* for each of the 35 words, align it with a restricted + minimum word of the same length and extract the local rewrite. + * *Blocked by:* no candidate rule yet; the census only certifies lengths. +2. **Seven registers.** Does a strict advantage first appear at seven + registers (3+4, 4+3)? Only a concrete word would reopen the PR1868 feedback + question. A larger negative census alone is not justified by this result. + +The structured versions are in [TASK.json](TASK.json). + +## Sources and credit + +* *Pins:* base commit `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (priority + revision 6). Exact Git blobs and SHA-256 pins are in + [SOURCES.json](SOURCES.json): + * four-register README `9ce21f23…`; + * to-8 README `a67a6b18…`; + * r439-twisted-star-absorption-seed02 README `ddd5b484…`; + * the selected record `bb2eaa58…`, which is PR1094 and unchanged. +* *Predecessor PRs (authors and heads checked with `gh`):* + * **ywz65** (PR2494, head `80fea4ae`): four-register twisted census. + * **Sagar Thakrar** (PR1868, head `6b222d01`): twisted-helper contract and + question 3. + * **@commdata2338** (PR1306, head `0d4c0069`): model, substitution lemma, + MITM and the 3x3 `T = I` census. + * **Hanson Sun (@bbMisk)** (PR1557, head `15e0987e`): 3x4 census. + * **rtyu193-rgb** (PR1706, head `dc6a2599`): 4x4 census; and PR2567 (head + `d28ac97c`), the to-8 package with the `H = 1` / `Y = 1` lemma and + duality. +* *No reuse:* no predecessor code is imported or changed. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/bit-twisted-feedback-contamination-lemma/SOURCES.json b/research/bit-twisted-feedback-contamination-lemma/SOURCES.json new file mode 100644 index 0000000000..b2f1e77858 --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/bit-twisted-feedback-four-registers/README.md", + "usage": "input", + "git_blob": "1fada03bfb8a3605c5cd8326c227b0e9abf7c694", + "sha256": "9ce21f2362fd641530bcd3991b73355160a9cdd2472affd9ed7a2d72b2268747" + }, + { + "path": "research/bit-zero-frame-feedback-to-8-registers/README.md", + "usage": "input", + "git_blob": "be3a35e8f252cfea295d42bc43df6cc55c94ff05", + "sha256": "a67a6b18a5ce18e2f100ab475c68c46a41e2d135a3a2443040f76cb3fbccbfb4" + }, + { + "path": "research/r439-twisted-star-absorption-seed02/README.md", + "usage": "input", + "git_blob": "84bd7838324a5d3216f2c91441b77dcbb065818a", + "sha256": "ddd5b4848981bf2df3ed2ad9faa01805a0528d7b4464c6f6b6935f01ddc37915" + } + ] +} diff --git a/research/bit-twisted-feedback-contamination-lemma/TASK.json b/research/bit-twisted-feedback-contamination-lemma/TASK.json new file mode 100644 index 0000000000..5d951ed159 --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "refined", + "actual_scope": "Boundary (h,y)->(T h, y+K h) with dirty inputs, T in GL_H(F2), unit-cost directed XORs, fixed labels. (1) Written every-word lemma: any word of length L whose product lies in P_{H,Y} yields an explicit restricted word of length L - f_v + c(w) computing the same map, with an explicit contamination charge c and no hypothesis that the target block is invertible. (2) Exact 3+3 decision over the 85,504 exits with T != I: no strict feedback advantage, common minimum histogram 1:6 2:96 3:744 4:3594 5:11463 6:23948 7:29259 8:15438 9:956. (3) Five-register shapes 2+3, 3+2, 4+1: no strict advantage for the 333,552 twisted (T != I) exits (320 + 10,688 + 322,544); the run also covers 144 settled T=I shears in those shapes and the 16 settled 1+4 exits, 333,712 in total. Positive control: in the same five-register model exactly 120 non-exit elements of P (60 in P_{2,3}, 60 in P_{3,2}, all with target block D != I) have d_full = d_P - 1, and Corollary 2 holds on a minimum word of each; so the exit condition D = I is load-bearing.", + "scope_change_reason": "The card asks whether one specified helper-mixing word satisfies a replacement for the inherited H2/K interface. This package answers the replacement contract's feedback question (PR1868 question 3) for twisted exits: an every-word contamination-charge lemma plus exact 3+3 and five-register decisions. It admits no H2/K word and changes no paid profile.", + "bottleneck_link": "Side result for the bit-helper-contract line (PR1868 question 3, fixed exits only): in PR1306's model, target-to-helper feedback gives no gain at any twisted exit of the 3+3 shape (the case PR2494 left open) or of the five-register shapes 2+3, 3+2, 4+1 (with PR2494's H+Y <= 4 census, every twisted shape with at most five registers). Not closed: twisted 2+4, 4+2, 5+1 and larger shapes; the actual seed02 D boundary (at least 3 helpers and 99 targets), where only Corollary 2's necessary condition (a non-clean, i.e. contaminated or singular, read with c >= f_v + 1) applies; C-absorption pricing; twisted-versus-restored exits. No kappa effect either way: the bit side does not bind (r439-twisted-star-absorption-seed02).", + "budget_minutes": 90, + "stop_rule": "Submit only if some exit has a cross-checked strict feedback advantage, or the lemma is written for every word with no target-block invertibility hypothesis, mechanically corroborated, with the finite 3+3 decision as corroboration (met by the latter).", + "outcome": "negative-result", + "evidence": "PROOF.md (written lemma and corollaries); verify.py (stdlib: construction on 6,628 words, two per element of every P_{H,Y} with n<=4, 8,400 random P-words n<=8, 2,800 free words with the per-gate invariant only; stdlib column-major 3+3 MITM via independent33.py with restricted balls asserted inside P_{3,3}; five controls); numpy_crosscheck.py (numpy==2.5.4: dense P_{3,3} BFS + row-major B4xB4 MITM; dense five-register census; construction on one greedy minimum word per five-register exit, 333,712 words, 35 of which (all 4+1) have a non-clean read with c = f_v + 1, so those exits are decided by the census, not the lemma).", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) in research, code, checking and writing; reviewed only by AI passes in the same loop, no independent human review.", + "open_questions": [ + { + "question": "Is there a local rewriting rule that turns a minimum word with a non-clean read into a restricted word of the same length, at least for one-target (Y = 1) twisted exits at every H? Such a rule must use D = I, because 120 non-exit five-register elements of P have a strict feedback gain.", + "why_it_matters": "c <= f_v already fails for some minimum words (the 35 greedy 4+1 words have c = f_v + 1, yet their exits have equal-length restricted words), so the lemma alone cannot extend the decision; such a rule would extend it beyond five registers.", + "first_step": "For each of the 35 greedy 4+1 words, align it with a restricted minimum word of the same length and extract the local rewrite.", + "blocked_by": "No candidate rule yet; the census certifies lengths, not rewrites." + }, + { + "question": "Does a strict feedback advantage first appear at seven registers (3+4 or 4+3 twisted exits)?", + "why_it_matters": "Only a concrete word beating a certified restricted minimum would reopen the feedback question for a replacement helper contract.", + "first_step": "Use Corollary 2 to restrict the search to words with a non-clean (contaminated or singular) read and charge at least f_v + 1, rather than a blind census.", + "blocked_by": "No favourable candidate; a larger negative census alone is not justified by this result." + } + ] +} diff --git a/research/bit-twisted-feedback-contamination-lemma/VERIFY.json b/research/bit-twisted-feedback-contamination-lemma/VERIFY.json new file mode 100644 index 0000000000..8e011e9fcc --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.5.4" + ], + "inputs": [ + "research/bit-twisted-feedback-four-registers/README.md", + "research/bit-zero-frame-feedback-to-8-registers/README.md", + "research/r439-twisted-star-absorption-seed02/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Contamination-charge construction (6,628 words, two per element of every P_{H,Y} with n<=4; 8,400 random P-words n<=8; 2,800 free words, per-gate invariant only), stdlib column-major 3+3 MITM decision over 85,504 twisted exits, five negative controls" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/numpy_crosscheck.py" + ], + "timeout_seconds": 300, + "checks": "numpy second method: dense P_{3,3} BFS and row-major B4xB4 MITM; dense five-register census (333,712 exits: 333,552 twisted plus 160 settled T=I shears); construction on one greedy minimum word per five-register exit (35 non-clean 4+1 words with c = f_v + 1); positive control: all 120 non-exit elements of five-register P with a strict feedback gain, 60 in P_{2,3} and 60 in P_{3,2}, with Corollary 2 asserted on a minimum word of each" + } + ] +} diff --git a/research/bit-twisted-feedback-contamination-lemma/independent33.py b/research/bit-twisted-feedback-contamination-lemma/independent33.py new file mode 100644 index 0000000000..6fb72dde10 --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/independent33.py @@ -0,0 +1,126 @@ +"""Primary 3+3 method (run by verify.py; numpy_crosscheck.py is the second method): stdlib only, column-major encoding, +right-multiplication meet-in-the-middle with splits 6+3 (restricted) and 5+3 (unrestricted). +Imports nothing from lemma.py or numpy_crosscheck.py. Column c of a 6x6 F2 matrix is the 6-bit field at 6c.""" +import itertools + +COL0 = sum(1 << (6 * c) for c in range(6)) + + +def gate(x, d, s): # row d ^= row s, applied to every column field + return x ^ (((x >> s) & COL0) << d) + + +def ball(gens, radius): + ident = sum(1 << (7 * c) for c in range(6)) + dist = {ident: 0} + front = [ident] + for k in range(1, radius + 1): + nxt = [] + for x in front: + for d, s in gens: + y = gate(x, d, s) + if y not in dist: + dist[y] = k + nxt.append(y) + front = nxt + return dist + + +def right_table(M): + cols = [(M >> (6 * c)) & 63 for c in range(6)] + tab = [0] * 64 + for pat in range(1, 64): + low = pat & -pat + tab[pat] = tab[pat ^ low] ^ cols[low.bit_length() - 1] + return tab + + +def mitm(M, small, big, cap): + """min |u|+|v| over M*u = v with u in small, v in big (exact when <= cap), else cap+1.""" + tab = right_table(M) + best = cap + 1 + for u, du in small.items(): + x = 0 + for c in range(6): + x |= tab[(u >> (6 * c)) & 63] << (6 * c) + dv = big.get(x) + if dv is not None and du + dv < best: + best = du + dv + return best + + +def exits(): + """All (T, K): T in GL3(F2), K in M_3x3(F2); column-major 6x6 [[T,0],[K,I]].""" + def inv3(T): + rows = [[T[r][c] for c in range(3)] + [int(r == c) for c in range(3)] for r in range(3)] + for c in range(3): + p = next((r for r in range(c, 3) if rows[r][c]), None) + if p is None: + return False + rows[c], rows[p] = rows[p], rows[c] + for r in range(3): + if r != c and rows[r][c]: + rows[r] = [a ^ b for a, b in zip(rows[r], rows[c])] + return True + out = [] + for tb in range(512): + T = [[tb >> (3 * r + c) & 1 for c in range(3)] for r in range(3)] + if not inv3(T): + continue + for kb in range(512): + K = [[kb >> (3 * r + c) & 1 for c in range(3)] for r in range(3)] + x = 0 + for r in range(6): + for c in range(6): + if r < 3 and c < 3: + v = T[r][c] + elif r >= 3 and c < 3: + v = K[r - 3][c] + else: + v = int(r == c) + x |= v << (6 * c + r) + out.append((T, K, x)) + return out + + +def canonical(T, K): + best = None + for s in itertools.permutations(range(3)): + Tp = tuple(tuple(T[s.index(r)][s.index(c)] for c in range(3)) for r in range(3)) + Kp = tuple(sorted(tuple(K[r][s.index(c)] for c in range(3)) for r in range(3))) + key = (Tp, Kp) + if best is None or key < best: + best = key + return best + + +def main(): + full = [(d, s) for d in range(6) for s in range(6) if d != s] + restr = [(d, s) for d, s in full if not (d < 3 <= s)] + B3, B5 = ball(full, 3), ball(full, 5) + P3, P6 = ball(restr, 3), ball(restr, 6) + blk = sum(1 << (6 * c + r) for r in range(3) for c in range(3, 6)) # helper rows x target columns + assert not any(k & blk for k in P3) and not any(k & blk for k in P6) # restricted balls stay in P_{3,3} + E = exits() + classes = {} + for T, K, x in E: + classes.setdefault(canonical(T, K), []).append((T, K, x)) + hist_p, hist_f, adv, twisted = {}, {}, 0, 0 + for key, members in classes.items(): + T, K, x = members[0] + dp = mitm(x, P3, P6, 9) + df = mitm(x, B3, B5, 8) + assert dp <= 9 and df <= dp, (key, dp, df) # every exit has a restricted word of length <= 9 + for T, K, _ in members: + if T != [[1, 0, 0], [0, 1, 0], [0, 0, 1]]: + twisted += 1 + hist_p[dp] = hist_p.get(dp, 0) + 1 + hist_f[min(df, dp)] = hist_f.get(min(df, dp), 0) + 1 + adv += df < dp + print("independent33 exits", len(E), "classes", len(classes), "twisted", twisted, + "strict_advantage", adv, "dP_hist", sorted(hist_p.items()), "dfull_hist", sorted(hist_f.items())) + return len(E), len(classes), twisted, adv, sorted(hist_p.items()) + + +if __name__ == "__main__": + main() diff --git a/research/bit-twisted-feedback-contamination-lemma/lemma.py b/research/bit-twisted-feedback-contamination-lemma/lemma.py new file mode 100644 index 0000000000..d7d6d51b1a --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/lemma.py @@ -0,0 +1,134 @@ +"""Every-word contamination-charge construction (stdlib only). + +Registers 0..H-1 are helpers, H..H+Y-1 targets. A gate (d, s) is r[d] ^= r[s]. +A matrix is a list of row bitmasks over the n = H+Y dirty inputs. +`simulate(word, H, Y)` returns a restricted word (no helper<-target gate) and the +explicit charge ledger. The invariant M_t = P_phi U(Z_t) N_t is asserted after +every gate, so no invertibility hypothesis is used anywhere. +""" + + +def identity(n): + return [1 << r for r in range(n)] + + +def apply(word, rows): + rows = list(rows) + for d, s in word: + if d == s: + raise ValueError("self XOR") + rows[d] ^= rows[s] + return rows + + +def in_parabolic(rows, H, Y): + tmask = ((1 << Y) - 1) << H + return all(rows[r] & tmask == 0 for r in range(H)) + + +def frame_rows(N, Z, phi, H, Y): + """Physical rows of P_phi U(Z) N.""" + n = H + Y + virt = list(N) + for b in range(H): + z = Z[b] + while z: + j = (z & -z).bit_length() - 1 + virt[b] ^= N[H + j] + z &= z - 1 + return [virt[phi[r]] for r in range(n)] + + +def simulate(word, H, Y, check=True): + n = H + Y + phi = list(range(n)) # physical register -> virtual register + Z = [0] * H # Z[b]: Y-bit row of the contamination matrix + N = identity(n) # restricted simulation state + M = identity(n) # actual state + out = [] # restricted word (virtual labels = physical labels) + led = {"length": len(word), "virtual_feedback": 0, "clean_reads": 0, + "contaminated_reads": 0, "singular_reads": 0, "read_charge": 0, + "relabel_swaps": 0} + + def emit(d, s): + if d < H <= s: + raise AssertionError("emitted a feedback gate") + out.append((d, s)) + N[d] ^= N[s] + + for d, s in word: + if d == s or not (0 <= d < n and 0 <= s < n): + raise ValueError("bad gate") + M[d] ^= M[s] + vd, vs = phi[d], phi[s] + if vd < H and vs >= H: # virtual feedback: absorbed, cost 0 + Z[vd] ^= 1 << (vs - H) + led["virtual_feedback"] += 1 + elif vd < H: # helper mixing + emit(vd, vs) + Z[vd] ^= Z[vs] + elif vs >= H: # target mixing y_i ^= y_j + i, j = vd - H, vs - H + emit(vd, vs) + for b in range(H): + if Z[b] >> i & 1: + Z[b] ^= 1 << j + else: # read y_i ^= h_a + i, a = vd - H, vs + Za = Z[a] + col = [b for b in range(H) if Z[b] >> i & 1] + if not Za and not col: + led["clean_reads"] += 1 + emit(vd, a) + elif not Za >> i & 1: # contaminated, nonsingular + led["contaminated_reads"] += 1 + led["read_charge"] += bin(Za).count("1") + len(col) + for j in range(Y): + if Za >> j & 1: + emit(vd, H + j) + emit(vd, a) + for b in col: + emit(b, a) + for b in col: + Z[b] ^= Za + else: # singular: target block loses rank + led["singular_reads"] += 1 + led["read_charge"] += bin(Za).count("1") + len(col) - 2 + for j in range(Y): + if j != i and Za >> j & 1: + emit(vd, H + j) + emit(vd, a) + rest = Za ^ (1 << i) + for b in col: + if b != a: + emit(b, a) + Z[b] ^= rest + Z[a] = rest + for r in range(n): # swap roles of virtual a and virtual H+i + if phi[r] == a: + phi[r] = vd + elif phi[r] == vd: + phi[r] = a + if check and frame_rows(N, Z, phi, H, Y) != M: + raise AssertionError("frame invariant failed") + + led["final_in_P"] = in_parabolic(M, H, Y) + if led["final_in_P"]: + # M in P and N in P force U(Z) = I and a block-preserving phi. + assert all(z == 0 for z in Z), "Z must vanish at a parabolic endpoint" + assert all((phi[r] < H) == (r < H) for r in range(n)), "phi must preserve blocks" + # physical r must hold virtual phi[r]: sort with 3-XOR swaps inside each block + cur = list(range(n)) # cur[r] = virtual content now in register r + for r in range(n): + if cur[r] != phi[r]: + q = cur.index(phi[r]) + for (x, y) in ((r, q), (q, r), (r, q)): + emit(x, y) + cur[r], cur[q] = cur[q], cur[r] + led["relabel_swaps"] += 1 + assert N == M, "restricted word must reproduce the endpoint" + led["charge"] = led["read_charge"] + 3 * led["relabel_swaps"] + led["restricted_length"] = len(out) + if led["final_in_P"]: + assert len(out) == led["length"] - led["virtual_feedback"] + led["charge"] + return out, led diff --git a/research/bit-twisted-feedback-contamination-lemma/numpy_crosscheck.py b/research/bit-twisted-feedback-contamination-lemma/numpy_crosscheck.py new file mode 100644 index 0000000000..f96eb29fee --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/numpy_crosscheck.py @@ -0,0 +1,160 @@ +"""numpy cross-check (pinned numpy==2.5.4): dense BFS + row-major left-multiplication MITM for 3+3, +dense five-register census for 2+3, 3+2, 4+1 (and the settled 1+4), and the contamination-charge +construction run on one greedy (first-gate) optimal unrestricted word for every five-register exit +[[T,0],[K,I]] (T=I shears included and counted separately; twisted means T != I).""" +import itertools, os, sys, time +import numpy as np +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +from lemma import simulate, apply, identity + + +def bfs_dense(nbits, start, step, gates): + dist = np.full(1 << nbits, 255, np.uint8); dist[start] = 0 + front = np.array([start], np.int64); d = 0 + while front.size: + d += 1 + for g in gates: + y = step(front, g); y = y[dist[y] == 255]; dist[y] = d + front = np.nonzero(dist == d)[0].astype(np.int64) + return dist + + +def three_plus_three(): + def step(x, g): + k, p, q = g + if k == 'h': return x ^ (((x >> (3 * q)) & 7) << (3 * p)) + if k == 't': return x ^ (((x >> (9 + 6 * q)) & 63) << (9 + 6 * p)) + return x ^ (((x >> (3 * q)) & 7) << (9 + 6 * p)) + gates = [('h', a, b) for a in range(3) for b in range(3) if a != b] + \ + [('t', i, j) for i in range(3) for j in range(3) if i != j] + [('r', i, a) for i in range(3) for a in range(3)] + ident = (1 | 2 << 3 | 4 << 6) | (8 << 9) | (16 << 15) | (32 << 21) + dist = bfs_dense(27, ident, step, gates) + assert int((dist < 255).sum()) == 168 * 168 * 512 + idx = np.nonzero(dist < 255)[0]; ok = np.ones(idx.size, bool) + for i in range(3): ok &= ((idx >> (9 + 6 * i + 3)) & 7) == (1 << i) + ex = idx[ok]; dP = dist[ex].astype(np.int64) + E = np.zeros_like(ex) + for a in range(3): E |= ((ex >> (3 * a)) & 7) << (6 * a) + for i in range(3): E |= ((ex >> (9 + 6 * i)) & 63) << (6 * (3 + i)) + def conj(x, p): + y = np.zeros_like(x) + for r in range(6): + for k in range(6): y |= ((x >> (6 * r + k)) & 1) << (6 * p[r] + p[k]) + return y + canon = E.copy() + for a in itertools.permutations(range(3)): + for b in itertools.permutations(range(3)): canon = np.minimum(canon, conj(E, a + tuple(3 + q for q in b))) + reps, inv = np.unique(canon, return_inverse=True) + full = [(d, s) for d in range(6) for s in range(6) if d != s] + sph = [np.array([sum(1 << (7 * r) for r in range(6))], np.int64)]; seen = sph[0] + for k in range(1, 5): + y = np.unique(np.concatenate([sph[-1] ^ (((sph[-1] >> (6 * s)) & 63) << (6 * d)) for d, s in full])) + y = y[~np.isin(y, seen, assume_unique=True)]; sph.append(y); seen = np.union1d(seen, y) + B = np.concatenate(sph); Bd = np.concatenate([np.full(s.size, k) for k, s in enumerate(sph)]) + o = np.argsort(B); B, Bd = B[o], Bd[o] + rd = np.full(reps.size, 9) + for n_, M in enumerate(reps.tolist()): + rows = [(M >> (6 * k)) & 63 for k in range(6)] + T = np.array([np.bitwise_xor.reduce([rows[k] for k in range(6) if p >> k & 1] or [0]) for p in range(64)], np.int64) + uM = np.zeros_like(B) + for r in range(6): uM |= T[(B >> (6 * r)) & 63] << (6 * r) + pos = np.searchsorted(B, uM); pos[pos >= B.size] = 0; hit = B[pos] == uM + if hit.any(): rd[n_] = min(9, int((Bd[hit] + Bd[pos[hit]]).min())) + dF = np.minimum(rd[inv], dP) + tw = (ex & 511) != (1 | 2 << 3 | 4 << 6) + assert (rd[inv] >= dF).all() and int(dP.max()) == 9 + return dict(exits=int(ex.size), classes=int(reps.size), twisted=int(tw.sum()), + strict_advantage=int((dF[tw] < dP[tw]).sum()), t_eq_i_advantage=int((dF[~tw] < dP[~tw]).sum()), + dP_hist=np.bincount(dP[tw]).tolist(), dfull_hist=np.bincount(dF[tw]).tolist(), + sphere_sizes=[int(s.size) for s in sph]) + + +def five_registers(): + n = 5 + step = lambda x, g: x ^ (((x >> (n * g[1])) & 31) << (n * g[0])) + full = [(d, s) for d in range(n) for s in range(n) if d != s] + ident = sum(1 << (n * i + i) for i in range(n)) + Df = bfs_dense(25, ident, step, full) + assert int((Df < 255).sum()) == 9999360 + def greedy(xs): # one optimal unrestricted word per element, by vectorized greedy (first-gate) descent on Df + cur = xs.copy(); words = [[] for _ in range(xs.size)] + while True: + live = np.nonzero(Df[cur] > 0)[0] + if not live.size: break + choice = np.full(live.size, -1) + for gi, g in enumerate(full): + nb = step(cur[live], g) + take = (choice < 0) & (Df[nb] == Df[cur[live]] - 1) + choice[take] = gi + assert (choice >= 0).all() + for li, gi in zip(live.tolist(), choice.tolist()): words[li].append(full[gi]) + cur[live] = np.array([step(np.array([c]), full[g])[0] for c, g in zip(cur[live].tolist(), choice.tolist())]) + return [wd[::-1] for wd in words] # descent g1..gk from M to I: M = g1...gk, apply gk first + + def lemma_run(x, w, H, Y, Dr): + rows = [(x >> (n * r)) & 31 for r in range(n)] + assert apply(w, identity(n)) == rows + out, led = simulate(w, H, Y) + assert apply(out, identity(n)) == rows and int(Dr[x]) <= len(out) + return out, led + + res = {} + for H in range(1, n): + Y = n - H + Dr = bfs_dense(25, ident, step, [(d, s) for d, s in full if not (d < H <= s)]) + idx = np.nonzero(Dr < 255)[0]; ok = np.ones(idx.size, bool) + for j in range(Y): ok &= (((idx >> (n * (H + j))) & 31) >> H) == (1 << j) + tg = idx[ok] + ti = np.ones(tg.size, bool) + for r in range(H): ti &= ((tg >> (n * r)) & 31) == (1 << r) # helper block T = I (an untwisted shear) + words = greedy(tg) + lem = dict(words=0, non_clean=0, singular=0, swaps=0, certified_by_lemma=0, max_charge_minus_fv=0) + for x, w in zip(tg.tolist(), words): + out, led = lemma_run(x, w, H, Y, Dr) + lem['words'] += 1; lem['non_clean'] += led['contaminated_reads'] + led['singular_reads'] > 0 # contaminated or singular + lem['singular'] += led['singular_reads'] > 0; lem['swaps'] += led['relabel_swaps'] > 0 + lem['certified_by_lemma'] += led['charge'] <= led['virtual_feedback'] + lem['max_charge_minus_fv'] = max(lem['max_charge_minus_fv'], led['charge'] - led['virtual_feedback']) + # positive control: feedback DOES help at some non-exit elements of P (target block D != I); + # Corollary 2 must then hold: f_v >= 1 and charge >= f_v + 1 on a minimum unrestricted word + gap = Dr[idx].astype(int) - Df[idx].astype(int) + pa = idx[gap > 0] + assert not np.isin(pa, tg).any() and (gap[gap > 0] == 1).all() + for x, w in zip(pa.tolist(), greedy(pa)): + out, led = lemma_run(x, w, H, Y, Dr) + assert len(w) == int(Dr[x]) - 1 and led['virtual_feedback'] >= 1 + assert led['contaminated_reads'] + led['singular_reads'] > 0 and led['charge'] >= led['virtual_feedback'] + 1 + adv = Dr[tg].astype(int) - Df[tg].astype(int) + tw = tg[~ti] + res[f"{H}+{Y}"] = dict(exits=int(tg.size), strict_advantage=int((adv > 0).sum()), + max_min=int(Dr[tg].max()), dP_hist=np.bincount(Dr[tg]).tolist(), lemma=lem, + t_eq_i=int(ti.sum()), twisted=int(tw.size), + twisted_max_min=int(Dr[tw].max()) if tw.size else 0, + nonexit_feedback_advantage=int(pa.size)) + return res + + +if __name__ == "__main__": + t = time.time() + r33 = three_plus_three() + print("3+3", r33, round(time.time() - t, 1), flush=True) + assert (r33["exits"], r33["classes"], r33["twisted"], r33["strict_advantage"], r33["t_eq_i_advantage"]) == (86016, 3478, 85504, 0, 0) + assert r33["dP_hist"] == r33["dfull_hist"] == [0, 6, 96, 744, 3594, 11463, 23948, 29259, 15438, 956] + r5 = five_registers() + print("five", r5, round(time.time() - t, 1), flush=True) + assert {k: (v["exits"], v["strict_advantage"], v["max_min"]) for k, v in r5.items()} == { + "1+4": (16, 0, 4), "2+3": (384, 0, 6), "3+2": (10752, 0, 8), "4+1": (322560, 0, 10)} + assert {k: (v["t_eq_i"], v["twisted"], v["twisted_max_min"]) for k, v in r5.items()} == { + "1+4": (16, 0, 0), "2+3": (64, 320, 6), "3+2": (64, 10688, 8), "4+1": (16, 322544, 10)} + # greedy words with a non-clean read: only 35 in 4+1, each with charge = f_v + 1 (lemma not tight there) + assert {k: (v["lemma"]["non_clean"], v["lemma"]["words"] - v["lemma"]["certified_by_lemma"], + v["lemma"]["max_charge_minus_fv"]) for k, v in r5.items()} == { + "1+4": (0, 0, 0), "2+3": (0, 0, 0), "3+2": (0, 0, 0), "4+1": (35, 35, 1)} + # feedback gains exactly 1 at 60 + 60 non-exit elements of P_{2,3}, P_{3,2} (D != I): the exit condition D = I is load-bearing + assert {k: v["nonexit_feedback_advantage"] for k, v in r5.items()} == {"1+4": 0, "2+3": 60, "3+2": 60, "4+1": 0} + words = sum(v["lemma"]["words"] for v in r5.values()) + twisted5 = sum(v["twisted"] for v in r5.values()) + assert (words, twisted5) == (333712, 333552) + print(f"PASS_TWISTED_FEEDBACK_NUMPY_CROSSCHECK twisted33={r33['twisted']} classes={r33['classes']} " + f"five_register_exits={words} twisted5={twisted5} strict_feedback_advantage=0 lemma_words={words} " + f"nonexit_advantage_controls=120") diff --git a/research/bit-twisted-feedback-contamination-lemma/verify.py b/research/bit-twisted-feedback-contamination-lemma/verify.py new file mode 100644 index 0000000000..fec5b13355 --- /dev/null +++ b/research/bit-twisted-feedback-contamination-lemma/verify.py @@ -0,0 +1,182 @@ +#!/usr/bin/env python3 +"""Stdlib verifier: contamination-charge construction + exact 3+3 twisted-exit decision + controls. + +PASS line: PASS_TWISTED_FEEDBACK_CONTAMINATION_LEMMA +""" +import os +import random +import sys +from collections import deque + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +from lemma import apply, identity, simulate # noqa: E402 +import independent33 # noqa: E402 + + +def bfs(n, gens): + start = tuple(identity(n)) + dist, par, queue = {start: 0}, {start: None}, deque([start]) + while queue: + x = queue.popleft() + for d, s in gens: + y = list(x) + y[d] ^= y[s] + y = tuple(y) + if y not in dist: + dist[y], par[y] = dist[x] + 1, (x, (d, s)) + queue.append(y) + return dist, par + + +def word_to(par, x): + w = [] + while par[x] is not None: + x, g = par[x] + w.append(g) + return w[::-1] + + +def mul(A, B): + out = [] + for a in A: + v, k = 0, 0 + while a: + if a & 1: + v ^= B[k] + a >>= 1 + k += 1 + out.append(v) + return out + + +def elim_word(G, n): + """A word w with apply(w, I) == G (Gaussian elimination; every op is an involution).""" + A, ops = list(G), [] + for c in range(n): + p = next(r for r in range(c, n) if A[r] >> c & 1) + if p != c: + A[c] ^= A[p] + ops.append((c, p)) + for r in range(n): + if r != c and A[r] >> c & 1: + A[r] ^= A[c] + ops.append((r, c)) + assert A == identity(n) + return ops[::-1] + + +def invertible(rows, n): + A = list(rows) + for c in range(n): + p = next((r for r in range(c, n) if A[r] >> c & 1), None) + if p is None: + return False + A[c], A[p] = A[p], A[c] + for r in range(n): + if r != c and A[r] >> c & 1: + A[r] ^= A[c] + return True + + +def tally(totals, led): + totals["singular"] += led["singular_reads"] > 0 + totals["swaps"] += led["relabel_swaps"] > 0 + totals["contaminated"] += led["contaminated_reads"] > 0 + + +def check_lemma(): + totals = dict(exhaustive_words=0, random_words=0, free_words=0, singular=0, swaps=0, contaminated=0) + rng = random.Random(20261019) + for n in (2, 3, 4): # every element of every parabolic, n <= 4 + full = [(d, s) for d in range(n) for s in range(n) if d != s] + Df, Pf = bfs(n, full) + assert len(Df) == {2: 6, 3: 168, 4: 20160}[n] + for H in range(1, n): + Y = n - H + Dr, _ = bfs(n, [(d, s) for d, s in full if not (d < H <= s)]) + for X in Dr: + detour = [rng.choice(full) for _ in range(rng.randrange(1, 12))] + inv = apply(list(reversed(detour)), identity(n)) + for w in (word_to(Pf, X), detour + word_to(Pf, tuple(mul(list(X), inv)))): + assert apply(w, identity(n)) == list(X) + out, led = simulate(w, H, Y) + assert apply(out, identity(n)) == list(X) and Dr[X] <= len(out) + totals["exhaustive_words"] += 1 + tally(totals, led) + for n in range(2, 9): # random words ending in P, n <= 8, every split + full = [(d, s) for d in range(n) for s in range(n) if d != s] + for H in range(1, n): + Y = n - H + for trial in range(300): + while True: + X = [rng.getrandbits(H) for _ in range(H)] + [rng.getrandbits(n) for _ in range(Y)] + if trial % 2: # exact twisted exit [[T,0],[K,I]] + X = X[:H] + [(X[H + j] & ((1 << H) - 1)) | 1 << (H + j) for j in range(Y)] + if invertible(X, n): + break + u = [rng.choice(full) for _ in range(rng.randrange(0, 3 * n))] + w = u + elim_word(mul(X, apply(list(reversed(u)), identity(n))), n) + assert apply(w, identity(n)) == X + out, led = simulate(w, H, Y) + assert led["final_in_P"] and apply(out, identity(n)) == X + totals["random_words"] += 1 + tally(totals, led) + for _ in range(100): # arbitrary endpoints: per-gate frame invariant only + simulate([rng.choice(full) for _ in range(rng.randrange(1, 40))], H, Y) + totals["free_words"] += 1 + assert totals["singular"] > 0 and totals["swaps"] > 0 and totals["contaminated"] > 0 + return totals + + +def controls(): + """Each control exercises a way the claim could be wrong and must fail in the stated way.""" + passed = 0 + # 1. The invertibility gap is real: after h^=y; y^=h the target block is 0, so no + # frame read off M's target block exists there; the construction still covers the word (two swaps = I). + w = [(0, 1), (1, 0), (0, 1), (0, 1), (1, 0), (0, 1)] + assert (apply(w[:2], identity(2))[1] >> 1) & 1 == 0, "control 1: target block must be singular" + out, led = simulate(w, 1, 1) + assert led["singular_reads"] == 2 and apply(out, identity(2)) == identity(2) + passed += 1 + # 2. Deleting feedback is wrong at a contaminated read: h^=y0; y1^=h; h^=y0 (H=1, Y=2). + w = [(0, 1), (2, 0), (0, 1)] + target = apply(w, identity(3)) + naive = apply([g for g in w if not (g[0] < 1 <= g[1])], identity(3)) + assert naive != target, "control 2: naive deletion must fail" + out, led = simulate(w, 1, 2) + assert apply(out, identity(3)) == target and led["charge"] == 1 and len(out) == 2 + passed += 1 + # 3. The charge is necessary: L - f = 1 < d_P(target) = 2 for that word. + full = [(d, s) for d in range(3) for s in range(3) if d != s] + Dr, _ = bfs(3, [(d, s) for d, s in full if not (d < 1 <= s)]) + assert Dr[tuple(target)] == 2 > len(w) - led["virtual_feedback"], "control 3" + passed += 1 + # 4. A forged extra gate is detected by replay. + try: + assert apply(out + [(1, 2)], identity(3)) == target, "forged word" + except AssertionError as exc: + assert "forged word" in str(exc) + passed += 1 + # 5. A self XOR is rejected. + try: + simulate([(1, 1)], 1, 1) + except ValueError: + passed += 1 + return passed + + +def main(): + totals = check_lemma() + print("lemma", totals, flush=True) + exits, classes, twisted, adv, hist = independent33.main() + assert (exits, classes, twisted, adv) == (86016, 3478, 85504, 0) + assert hist == [(1, 6), (2, 96), (3, 744), (4, 3594), (5, 11463), (6, 23948), (7, 29259), (8, 15438), (9, 956)] + n_controls = controls() + assert n_controls == 5 + print(f"PASS_TWISTED_FEEDBACK_CONTAMINATION_LEMMA exits33={exits} twisted={twisted} classes={classes} " + f"strict_feedback_advantage={adv} max_restricted_min={max(d for d, _ in hist)} " + f"lemma_words={totals['exhaustive_words'] + totals['random_words']} controls={n_controls}") + + +if __name__ == "__main__": + main()