diff --git a/research/two-helper-zero-frame-feedback/README.md b/research/two-helper-zero-frame-feedback/README.md new file mode 100644 index 0000000000..a3e85de146 --- /dev/null +++ b/research/two-helper-zero-frame-feedback/README.md @@ -0,0 +1,146 @@ +# Two-helper zero-frame shears: no feedback gain at any target count + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped proof (every target count T) with finite corroboration. +No new supplier, κ or selected-frontier change.** + +## Result + +Use the model of [bit-zero-frame-feedback](../bit-zero-frame-feedback/README.md) +(PR #1306) and [bit-zero-frame-feedback-to-8-registers](../bit-zero-frame-feedback-to-8-registers/README.md) +(PR #2567). Registers are two helpers `h0, h1` and `T` targets `y_1..y_T`. All +inputs are arbitrary (dirty). A gate `(d, s)` is `x_d ^= x_s` at unit cost; there +are no extra registers. A restricted word has no gate with a helper destination +and a target source. The required map is the shear `(h, y) -> (h, y + K h)` +over F2, where `K` is `T × 2`. + +Write `a`, `b` and `c` for the number of rows of `K` equal to `(1,0)`, `(0,1)` +and `(1,1)`, and `r = a + b + c` for the number of nonzero rows. + +**Theorem.** For every `T ≥ 1` and every `K`, the restricted and unrestricted +minimum word lengths are equal: + +```text +d_P(K) = d_full(K) = a + b + c + min(c, 2) = r + min(c, 2). +``` + +So target-to-helper feedback never lowers the cost of a two-helper shear. This +settles the 2×7 shape of Open next question 1 in PR #2567, and every other +2×T shape. By that package's duality `cost_{H×T}(K) = cost_{T×H}(K^T)`, it also +settles every T×2 shape, including 7×2. The 3×6 and 4×5 shapes stay open. + +## Proof + +**Upper bound (restricted).** Apply `y_i ^= h0` or `y_i ^= h1` for each pure +row. If `c ≤ 1`, apply `y_i ^= h0; y_i ^= h1` for the `(1,1)` row. If `c ≥ 2`, +apply `h0 ^= h1`, then `y_i ^= h0` for each `(1,1)` row, then `h0 ^= h1`. The +pure reads come first, so they see the original `h0`. The length is +`a + b + 2c` or `a + b + c + 2`, which is `r + min(c, 2)` in both cases. No gate +reads a target into a helper. + +**Lower bound (feedback allowed).** Let `w` be any word, in the unrestricted +alphabet, whose product is the shear. Track each register's content as a +linear form in the initial values. The contents of all registers form an +invertible matrix after every prefix, so no register ever holds zero. + +1. *Each nonzero row needs its target as a destination.* A register that is + never a destination ends with its initial content. A target with a nonzero + row of `K` must change, so at least `r` gates have a target destination. +2. *A once-modified target gets a pure row if no helper is a destination.* + Suppose no gate has a helper destination. Then `h0` and `h1` hold their + initial values throughout. Every prefix product then has block form + `[[I, 0], [X, Y]]` with `Y` invertible, so each target register's content has + a nonzero target part. If target `y_i` is the destination of exactly one gate, + its final content is `y_i + v`, where `v` is the source content at that gate. + The final target part must be `y_i` alone, so `v` has zero target part. Hence + `v` is `h0` or `h1`, and the row of `y_i` is `(1,0)` or `(0,1)`. So every + `(1,1)` target is a destination at least twice. +3. *A once-modified helper cannot end unchanged.* If helper `h_x` is the + destination of exactly one gate, it ends with `h_x + v` with `v ≠ 0`. The + shear requires it to end as `h_x`. + +Now suppose `c ≥ 1` and `|w| ≤ r + min(c, 2) - 1`. Step 1 gives `|w| ≥ r`. If `|w| = r`, all gates have target destinations. If +`c ≥ 2` and `|w| = r + 1`, at most one gate is not target-destined, and step 3 +forbids a lone helper destination. In both cases no gate has a helper +destination. Step 2 then needs at least `r + c` target-destined gates. That +exceeds `|w|`, because `c ≥ 1` when `|w| = r` and `c ≥ 2` when `|w| = r + 1`. +When `c = 0`, step 1 alone gives `|w| ≥ r`. Therefore +`d_full(K) ≥ r + min(c, 2)`. Since `d_full ≤ d_P`, both minima equal the formula. ∎ + +With `T = 1` we have `c ≤ 1`, and the formula reduces to `wt(K)`, as in the +`T = 1` lemma of PR #2567. + +## Evidence + +`verify.py` uses only the standard library and imports no predecessor code. It +checks four things: + +- **Witnesses:** for every `K` with `T = 1..8` (87,380 matrices), the explicit + restricted word above has length `r + min(c, 2)` and computes the shear + exactly. The gates are linear, so this covers all dirty inputs. +- **Exact BFS:** for `T = 1, 2, 3` (84 matrices), it runs independent + breadth-first searches in the unrestricted and restricted alphabets. Both + minima equal the formula. +- **Consistency with PR #2567:** the formula matches the pinned certified + minima for every `K` in 2×4, 2×5 and 2×6 (5,376 matrices). The certificate is + authenticated by SHA256. This is a calibration of the formula, not a replay + of PR #2567's search. +- **Controls:** the verifier rejects a truncated witness and a wrong shared + gate, detects an inserted feedback gate, and rejects the weight formula + `wt(K)` on a 2×3 matrix with three `(1,1)` rows (BFS minimum 5, weight 6). + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-helper-zero-frame-feedback/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/two-helper-zero-frame-feedback/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-helper-zero-frame-feedback +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-helper-zero-frame-feedback --check-source-history +``` + +Any CPython 3.12 path works. Each direct run takes under one second and prints + +```text +PASS_TWO_HELPER_ZERO_FRAME_FEEDBACK witnesses=87380 bfs=84 pr2567=5376 controls=4 feedback_gains=0 no_new_kappa +``` + +The checks use explicit exceptions, so they stay active under `-O`. + +## Scope and limits + +The theorem covers `H = 2` (and `T = 2` by duality), F2, PR #1306's two +unit-cost single-source alphabets, zero frames and no extra registers. Larger +helper counts, nonzero frames, multi-source gates, other costs and other fields +are outside scope. Physical precision, hosting and supplier pricing are not +built or checked. The finite checks corroborate the written proof. They do not +replace it for `T > 8`. Independent human and formal proof-kernel review are +unclaimed. + +Power of Ten rule 3 deviation: CPython allocates dynamically. Data sizes are +bounded by the fixed limits `T ≤ 8` for witnesses and `T ≤ 3` for BFS. The +largest BFS ball has fewer than 10^5 states. + +## Open next questions + +1. **Does feedback help for three helpers at nine registers (3×6)?** Step 2 + of the proof needs a replacement: with three helpers, a shared helper sum + can serve several row types, and two-step gains can combine. A first step is + a closed form for `d_P` on 3×T using the row-type counts, checked against + PR #2567's 3×5 certificate. +2. **Is there a row-type formula for every H?** For `H = 2` the cost depends + only on the row-type counts. For larger `H` the restricted cost becomes a + shared-sum covering problem. A closed form for `d_P` would give the target for + an unrestricted lower bound. +3. **Does the destination-counting argument extend to twisted exits?** The + contamination lemma of PR #4071 handles twisted exits at fixed small shapes. + Step 2 assumes the helper block stays fixed, so it would need the twisted + helper block's own cost. + +## Credits + +The model, the restricted/unrestricted question and the 2×4–2×6 certificates +are from rtyu193-rgb's PR #2567, which builds on commdata2338's PR #1306, +bbMisk's PR #1557 and rtyu193-rgb's PR #1706. The twisted-exit question cites +thakrarsagar's PR #4071. The new contribution here is the all-T two-helper +theorem and its proof. diff --git a/research/two-helper-zero-frame-feedback/SOURCES.json b/research/two-helper-zero-frame-feedback/SOURCES.json new file mode 100644 index 0000000000..c2ca68f7b7 --- /dev/null +++ b/research/two-helper-zero-frame-feedback/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-zero-frame-feedback-to-8-registers/CERTIFICATE.json", + "usage": "input", + "git_blob": "9bda10dad1646ec2003b56dcd5fb9376d3c35e94", + "sha256": "c47b7a294fd5ac6a9379e8967ecda48f4ef1428b7efeddca93fb8c3b03b8adfc" + } + ] +} diff --git a/research/two-helper-zero-frame-feedback/TASK.json b/research/two-helper-zero-frame-feedback/TASK.json new file mode 100644 index 0000000000..e86ca02ae9 --- /dev/null +++ b/research/two-helper-zero-frame-feedback/TASK.json @@ -0,0 +1,120 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact restricted and unrestricted minimum unit-XOR word length for every two-helper zero-frame dirty shear (h,y)->(h,y+Kh) over F2, every target count T, in the PR1306/PR2567 model.", + "scope_change_reason": "Answers the two-helper part (including 2x7) of Open next question 1 in PR2567, which asks whether target feedback ever helps beyond eight registers. This is a register-model side theorem, not a new supplier.", + "bottleneck_link": "Side result: closes the D-local target-feedback relaxation for every two-helper prefix, so a feedback saving cannot come from H=2 or T=2 shears. No κ effect.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified all-T two-helper theorem; leave 3x6 and 4x5 open.", + "outcome": "completed", + "evidence": "README.md gives the written proof. verify.py checks 87,380 restricted witnesses (T=1..8), exact BFS for T=1..3 in both alphabets, agreement with PR2567's 2x4-2x6 minima (5,376 K) and four controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does target feedback help for 3x6 at nine registers?", + "why_it_matters": "Completes the nine-register case of PR2567's question with 4x5.", + "first_step": "Find a row-type closed form for d_P on 3xT and test it on PR2567's 3x5 certificate.", + "blocked_by": "Step 2 of the proof assumes two helpers." + }, + { + "question": "Is there a row-type formula for every H?", + "why_it_matters": "A closed restricted cost gives the target for a general lower bound.", + "first_step": "Formulate d_P as a shared helper-sum covering problem.", + "blocked_by": "No closed form for H>=3." + }, + { + "question": "Does destination counting extend to twisted two-helper exits?", + "why_it_matters": "PR4071 covers twisted exits only at fixed small shapes.", + "first_step": "Price the twisted helper block and redo step 2 with a changing helper block.", + "blocked_by": "Step 2 needs fixed helpers." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230512", + "playbook": "Investigation", + "citations": [ + { + "pr": 2567, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2567", + "author": "rtyu193-rgb", + "contribution": "Model, open question and 2x4-2x6 certified minima.", + "usage": "Pinned certificate used as a formula calibration input." + }, + { + "pr": 1306, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1306", + "author": "commdata2338", + "contribution": "Original model and alphabets.", + "usage": "Cited context only." + }, + { + "pr": 1557, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1557", + "author": "bbMisk", + "contribution": "3x4 certificate.", + "usage": "Cited context only." + }, + { + "pr": 1706, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1706", + "author": "rtyu193-rgb", + "contribution": "4x4 certificate.", + "usage": "Cited context only." + }, + { + "pr": 4071, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4071", + "author": "thakrarsagar", + "contribution": "Twisted-exit contamination lemma.", + "usage": "Cited for an open question only." + } + ], + "preserved_checkout": { + "branch": null, + "detached_head": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "prior_commits": [] + } +} diff --git a/research/two-helper-zero-frame-feedback/VERIFY.json b/research/two-helper-zero-frame-feedback/VERIFY.json new file mode 100644 index 0000000000..f511c1d6df --- /dev/null +++ b/research/two-helper-zero-frame-feedback/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-zero-frame-feedback-to-8-registers/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Restricted witnesses for every K at T=1..8 (87,380), exact restricted and unrestricted BFS for T=1..3 (84), formula against pinned PR2567 2x4-2x6 minima (5,376), four rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Restricted witnesses for every K at T=1..8 (87,380), exact restricted and unrestricted BFS for T=1..3 (84), formula against pinned PR2567 2x4-2x6 minima (5,376), four rejection controls." + } + ] +} diff --git a/research/two-helper-zero-frame-feedback/verify.py b/research/two-helper-zero-frame-feedback/verify.py new file mode 100644 index 0000000000..fdf21b6f82 --- /dev/null +++ b/research/two-helper-zero-frame-feedback/verify.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Two-helper zero-frame shears: feedback never helps, for every target count. + +Model of PR1306/PR2567: registers h0, h1, y0..y(T-1); a gate (d, s) is +register[d] ^= register[s] at unit cost; restricted words have no gate with a +helper destination and a target source. The map is (h, y) -> (h, y + K h). +For row counts a, b, c of (1,0), (0,1), (1,1) in K, PROOF.md shows that both +minima equal f(K) = a + b + c + min(c, 2). + +Checks (standard library only): + witnesses every K for T = 1..8: an explicit restricted word of length f(K) + computes exactly the shear (all dirty inputs, by linearity) + bfs exact unrestricted and restricted BFS for T = 1, 2, 3 against f + pr2567 f against the pinned 2x4, 2x5 and 2x6 certified minima + controls mutated words and a wrong formula are rejected + +Produced by Nick Petalas. Apache-2.0. +""" +import hashlib +import json +from pathlib import Path +import sys + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +PR2567 = ROOT / "research/bit-zero-frame-feedback-to-8-registers/CERTIFICATE.json" +PR2567_SHA256 = "c47b7a294fd5ac6a9379e8967ecda48f4ef1428b7efeddca93fb8c3b03b8adfc" +H = 2 +MAX_WITNESS_T = 8 +MAX_BFS_T = 3 + + +def require(cond, msg): + if not cond: + raise AssertionError(msg) + + +def rows_of(K, T): + """Row i of K as a 2-bit mask (bit j = helper j), K[i][j] = bit i*H + j.""" + return [(K >> (H * i)) & 3 for i in range(T)] + + +def formula(K, T): + r = rows_of(K, T) + c = r.count(3) + return r.count(1) + r.count(2) + c + min(c, 2) + + +def shear(K, T): + """Target matrix as a tuple of register rows (bit e = coefficient of register e).""" + out = [1 << j for j in range(H)] + for i, row in enumerate(rows_of(K, T)): + out.append((1 << (H + i)) | row) + return tuple(out) + + +def apply_word(word, n): + rows = [1 << e for e in range(n)] + for d, s in word: + require(d != s and 0 <= d < n and 0 <= s < n, "bad gate") + rows[d] ^= rows[s] + return tuple(rows) + + +def restricted(word): + return all(not (d < H and s >= H) for d, s in word) + + +def witness(K, T): + """Restricted word of length f(K): direct reads, then one shared h0 ^= h1 block when c >= 2.""" + rows = rows_of(K, T) + c = rows.count(3) + word = [(H + i, row - 1) for i, row in enumerate(rows) if row in (1, 2)] + both = [H + i for i, row in enumerate(rows) if row == 3] + if c >= 2: + word += [(0, 1)] + [(y, 0) for y in both] + [(0, 1)] + else: + word += [g for y in both for g in ((y, 0), (y, 1))] + return word + + +def check_witnesses(): + total = 0 + for T in range(1, MAX_WITNESS_T + 1): + n = H + T + for K in range(1 << (H * T)): + w = witness(K, T) + require(restricted(w), "witness uses feedback") + require(len(w) == formula(K, T), "witness length differs from f") + require(apply_word(w, n) == shear(K, T), "witness computes a different map") + total += 1 + return total + + +def bfs_distances(T, restricted_only, horizon): + n = H + T + gens = [(d, s) for d in range(n) for s in range(n) + if d != s and not (restricted_only and d < H and s >= H)] + start = tuple(1 << e for e in range(n)) + dist = {start: 0} + frontier = [start] + for depth in range(1, horizon + 1): + nxt = [] + for m in frontier: + for d, s in gens: + rows = list(m) + rows[d] ^= rows[s] + t = tuple(rows) + if t not in dist: + dist[t] = depth + nxt.append(t) + frontier = nxt + return dist + + +def check_bfs(): + compared = 0 + for T in range(1, MAX_BFS_T + 1): + horizon = max(formula(K, T) for K in range(1 << (H * T))) + full = bfs_distances(T, False, horizon) + rest = bfs_distances(T, True, horizon) + for K in range(1 << (H * T)): + m = shear(K, T) + require(full.get(m) == formula(K, T), f"unrestricted minimum differs T={T} K={K}") + require(rest.get(m) == formula(K, T), f"restricted minimum differs T={T} K={K}") + compared += 1 + return compared + + +def check_pr2567(): + data = PR2567.read_bytes() + require(hashlib.sha256(data).hexdigest() == PR2567_SHA256, "PR2567 certificate hash") + cert = json.loads(data) + compared = 0 + seen = [] + for shape in cert["shapes"]: + if shape["helpers"] != H: + continue + T = shape["targets"] + costs = [int(ch, 16) for ch in shape["costs_hex"]] + require(len(costs) == 1 << (H * T), "PR2567 cost table size") + for K, cost in enumerate(costs): + require(cost == formula(K, T), f"PR2567 cost differs T={T} K={K}") + compared += 1 + seen.append(T) + require(seen == [4, 5, 6], "expected PR2567 shapes 2x4, 2x5, 2x6") + return compared + + +def check_controls(): + T, K = 3, 0b111111 # three (1,1) rows: f = 5 + w = witness(K, T) + require(apply_word(w[:-1], H + T) != shear(K, T), "truncated word accepted") + require(apply_word([(1, 0)] + w[1:], H + T) != shear(K, T), "wrong shared gate accepted") + require(not restricted(w + [(0, H)]), "feedback gate not detected") + full = bfs_distances(T, False, 5) + require(full.get(shear(K, T)) != bin(K).count("1"), "weight formula wt(K) was not rejected") + return 4 + + +def main(): + w = check_witnesses() + b = check_bfs() + p = check_pr2567() + c = check_controls() + print(f"PASS_TWO_HELPER_ZERO_FRAME_FEEDBACK witnesses={w} bfs={b} pr2567={p} " + f"controls={c} feedback_gains=0 no_new_kappa") + + +if __name__ == "__main__": + sys.exit(main())