From f6712095d07d555969b6e67b792a0e98e8eea8d3 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 08:43:59 +0000 Subject: [PATCH] Census dynamic helper captures on the final G20 BIT word (PR5586 B1): none pays for one helper or any pair; joint bound for larger sets Exact census on the PR5708 local word: every retained helper with an arbitrary injected payload at every dead/live epoch boundary (one live interval each, none pays), the five joint-dead pairs and all 6030 pairs with a shared query (none pays), and a parity-token bound for owned sets of any size. Positive control rediscovers the nine PR5671 late-binding captures on the PR5667 word. No new kappa. The complete search for three or more helpers is recorded as an open question. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011VhYmBnPWtZUVcoWbpL8nT --- research/g20-dynamic-capture-census/PROOF.md | 96 +++ research/g20-dynamic-capture-census/README.md | 84 +++ .../g20-dynamic-capture-census/RESULT.json | 247 +++++++ .../g20-dynamic-capture-census/SOURCES.json | 66 ++ research/g20-dynamic-capture-census/TASK.json | 83 +++ .../g20-dynamic-capture-census/VERIFY.json | 28 + .../g20-dynamic-capture-census/capture.py | 667 ++++++++++++++++++ research/g20-dynamic-capture-census/verify.py | 157 +++++ 8 files changed, 1428 insertions(+) create mode 100644 research/g20-dynamic-capture-census/PROOF.md create mode 100644 research/g20-dynamic-capture-census/README.md create mode 100644 research/g20-dynamic-capture-census/RESULT.json create mode 100644 research/g20-dynamic-capture-census/SOURCES.json create mode 100644 research/g20-dynamic-capture-census/TASK.json create mode 100644 research/g20-dynamic-capture-census/VERIFY.json create mode 100644 research/g20-dynamic-capture-census/capture.py create mode 100644 research/g20-dynamic-capture-census/verify.py diff --git a/research/g20-dynamic-capture-census/PROOF.md b/research/g20-dynamic-capture-census/PROOF.md new file mode 100644 index 0000000000..f79fe1a5d2 --- /dev/null +++ b/research/g20-dynamic-capture-census/PROOF.md @@ -0,0 +1,96 @@ +# Dynamic captures on the PR5708 G20 word: model and argument + +## Word model + +The local word is `research/g20-conjugation-admission/WORD.json.gz` with the +frames of its vendored G20 source. Wire i starts with the symbol x_i. A +payload is a finite F2 sum of terms M x_i, M an exact 8x8 rational matrix +(a product of frame reflections R_f = I - 2 P_f). `ADD d s f` adds the +payload of s to d; `Q d s t k` is a paid query of rank k and multiplies by +R_s R_t; `ZERO_Q` moves a zero payload for free; `ERASE`/`INIT` touch owned +wires only. The replay checks every frame, rank and zero move and reproduces +the published local paid profile {1:1281, 2:1338, 3:58, 4:57, 5:102, 6:10}. +Helpers are the 415 retained non-main wires; their target ranks are the +frame-dimension differences (413 rank 8, helpers 465 and 684 rank 4). + +## Captures + +Owning a set H of helpers debits sum over H of r_h^t. For h in H, h is +*dead-forward* before event i when its content then reaches no retained +output other than outputs of H (backward replay of the exact operators). +In each maximal dead interval [a, b] that contains no read of h, writes into +h are dropped and h is held zero, so its own queries in [a, b) become free +`ZERO_Q` moves. Just before event b, h receives an arbitrary payload w +(ERASE plus same-frame ADDs). Scalar costs of these changes are not charged, +which can only favour a capture. + +## Exact kill condition + +A forward replay injects a fresh symbol u into h before each b. Since the +operators act linearly, the true payload of every query is + + p_q = rest_q + sum M_(q,s) (w_s + snap_s), + +where rest_q is the replayed payload with injected symbols removed and owned +input symbols set to zero, snap_s is the replayed content of h just before +the injection (owned inputs zeroed), and M_(q,s) is the coefficient of u_s. +The replay checks that every such coefficient is a single matrix and that no +injected symbol reaches a retained output outside H. A query is removed iff +p_q = 0. + +*Single dependence.* If q depends on one injected symbol, it is removed iff +w_s = M^-1 (rest_q + M snap_s): one exact value. Queries are grouped by that +value; the best group of each epoch is the most a single injection removes. +For one helper every query depends on one symbol, so the single-helper census +is exact. On PR5708 every helper has two dead intervals (before its first +read and after its last) and so one injection; the leading interval never +contains a read of the helper. + +*Parity classes.* Let parity(p) be the F2 sum of the symbol masks over all +matrices. It is F2-linear and parity(M p) = parity(p) for one invertible +matrix M. If q depends on a set D of injected symbols and p_q = 0, then + + parity(rest_q) + sum_(s in D) parity(snap_s) = sum_(s in D) parity(w_s). + +The left side is a label computed from the word; all removed queries with the +same D share one label. Hence the removed mass of queries with dependence D +is at most the heaviest label class. + +## Pairs + +Individual schedule (each helper keeps its own dead intervals): for pair +(a, b) the gain is at most free(a) + free(b) + best(a) + best(b) + heaviest +class of the shared queries - 8^t(a) - 8^t(b). The 5638 pairs where this is +not positive are closed. When no single-dependence query is removed, the gain +is at most free + heaviest class - debits, which is negative for every pair +(checked). Otherwise w_a lies in the group values of a (or zero) and w_b is +in the group values of b, zero, or forced by one shared query; symmetrically. +All such candidates are evaluated exactly for the 392 remaining pairs; the +best gain is -1.957. + +Joint schedule: a backward replay finds five pairs (h, p) where the content +of h at some time reaches only the outputs of h and p. Owning both lengthens +dead intervals. Each pair is reanalysed with joint deadness; four close by +the class bound and the pair (297, 684) by exact enumeration (-1.968). + +## Joint token bound + +Under the individual schedule, a removed query satisfies +parity(p_base) = sum over owned h it depends on of (e_h + b_h), where b_h +collects the parities of w_h and of the dropped writes. So every removed +base-word parity row lies in a d-dimensional space for d owned helpers. Give +each eligible query ceil(4 r^t) copies of its row (2213 queries, 15544 +tokens) and greedily split them into N = 26 F2-independent sets. A +d-dimensional space meets each set in at most d vectors, so the removed +t-mass is at most 26 d / 4 = 6.5 d, plus at most one free own query per +helper (rank at most 2, checked). A helper with a free own query of rank 1 or +none therefore contributes at most -0.439; one with a free rank-2 query at +most +0.556. The greedy N is an upper bound; the true minimum may be smaller. + +## Limits + +The joint token bound uses individual dead intervals; joint deadness is +checked for pairs only. Sets of three or more helpers containing several +helpers with a free rank-2 query are not decided. All decisions use +double-precision moments with margins above 1e-3, except the exact neutral +case of helper 684 (one H4 removed for one H4 target). diff --git a/research/g20-dynamic-capture-census/README.md b/research/g20-dynamic-capture-census/README.md new file mode 100644 index 0000000000..058ae29f7f --- /dev/null +++ b/research/g20-dynamic-capture-census/README.md @@ -0,0 +1,84 @@ +# Dynamic helper captures on the final G20 BIT word + +On the exact PR5708 G20 local word (conditional ordinary BIT saving +0.003507719059749), no owned-helper capture of the PR5586 **B1** kind pays +its target for one helper or for any pair of helpers, with an arbitrary +injected payload at every epoch. Every retained helper has exactly **one +live interval**, so the multi-epoch premise of B1 has no instance on this +word. A joint parity-token bound limits larger owned sets. The complete +search over sets of three or more helpers is left open below, with a +concrete encoding. No new kappa or supplier admission is claimed. + +Claim type: finite exact census with a scoped linear-algebra argument. +Base: canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`. + +## Results at the B1 target C = 0.0037 (t = 1 - C) + +| Check | Result | +|---|---| +| Needed over the PR5708 invoice | +40.952 signed moment, +2.2751 per local word (18 calls) | +| Debit of one owned full helper | 8^t = 7.9387 | +| Single helper, arbitrary injection, all epochs (415 helpers) | none pays; best 0 (helper 684, H4 for H4); max removed rank mass 7 | +| Live intervals per helper | exactly 1 for all 415 | +| Pairs whose joint ownership lengthens a dead interval | 5, all lose (exact best -1.968) | +| Pairs with a shared query, individual schedule | 6030: 5638 closed by the parity-class bound, 392 enumerated exactly; best -1.957 | +| Joint token bound, any owned set | removed t-mass at most 26/4 = 6.5 per owned helper, plus its free own query | +| Consequence | a set gains only through the 180 helpers with a free rank-2 own query (at most +0.556 each); reaching 0.0037 needs at least 5 of them, all compatible | + +Positive control: on the PR5667 word (the source of Ali Romman's PR5671, +from Dugongue's PR5665 theorem) at C = 0.0035 the same single-helper census +finds exactly the nine selected late-binding helpers of PR5671 +(223, 319, 331, 344, 371, 375, 484, 501, 551), each as a free own H1 plus one +removed H7. No other helper is positive there. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/g20-dynamic-capture-census +python3.12 -I -W error -B research/g20-dynamic-capture-census/verify.py +``` + +Python 3.12 and the standard library suffice; one run takes under a +minute. Expected final token: `PASS_G20_DYNAMIC_CAPTURE_CENSUS`. The +verifier authenticates the pinned inputs in SOURCES.json, checks the PR5708 +local paid profile, recomputes every number above and compares RESULT.json +in full. `--write` regenerates RESULT.json. [PROOF.md](PROOF.md) gives the +model, the exactness argument and the precise scope. + +## Scope + +The word, its frames and its native contract are used as published. Captures +own retained helpers, drop writes into a helper while it is dead-forward, +and inject arbitrary payloads by ordinary same-frame scalar operations; the +scalar fees of those injections are not charged, which only helps a capture. +Paid frame conversions, added contacts, changed scalar order and changed +words are outside this census. Native/ROW, compiler, ordinary backend, +precision and tape premises of the source framework are unchanged and not +replayed. This is an author check, not independent acceptance. + +## Open next questions + +- **Complete joint search for three or more helpers.** Only sets built + mostly from the 180 helpers with a free rank-2 own query can still gain, + at most +0.556 per helper by the token bound. Encode candidate injections + with their exact matrix-level kill conditions and solve the weighted + maximum consistent subset (ILP or MaxSAT) with the moment gain as + objective; check any witness with `capture.py`. Expected outcome is + negative, but it is not proved here. Volunteers are welcome. +- **Changed words.** B1 needs helpers with several live intervals or larger + shared queries. Run `capture.py` on any new G20 successor word: a second + live interval or a positive single-helper bound is the signal. + +TASK.json records both questions. + +## Credit + +Dugongue proposed B1 in PR5586 and the deferred-input theorem in PR5665. +Ali Romman supplied the nine-owned-relation method (PR5421), the static +entry-capture capacity bound whose token argument is adapted here (PR5604), +the PR5671 late-binding admission used as the control and the PR5679/PR5708 +words. Credit ai-nanachi's PR5512 G20 source and all native, controller, +helper, ordinary and stock predecessors named in those packages. Nick +Petalas's PR5983 covers a different (split) mechanism on the same word. +Prepared for Matarener with substantial Anthropic Claude assistance +(Claude Code). Apache-2.0. diff --git a/research/g20-dynamic-capture-census/RESULT.json b/research/g20-dynamic-capture-census/RESULT.json new file mode 100644 index 0000000000..80920cfa69 --- /dev/null +++ b/research/g20-dynamic-capture-census/RESULT.json @@ -0,0 +1,247 @@ +{ + "C": "37/10000", + "control_PR5667": { + "C": "7/2000", + "positive": [ + 223, + 319, + 331, + 344, + 371, + 375, + 484, + 501, + 551 + ], + "shape": "free own H1 + removed H7" + }, + "joint_bound": { + "N": 26, + "capacity_per_owned_helper": 6.5, + "distinct_rows": 1945, + "eligible": 2213, + "helpers_with_free_rank2": 180, + "per_helper_gain_max": { + "free_own_rank1": -0.438685, + "free_own_rank2": 0.556193, + "no_free_own": -1.438685 + }, + "set_sizes": [ + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 637, + 636, + 634, + 634, + 621, + 545, + 534, + 409, + 65 + ], + "tokens": 15544 + }, + "joint_dead_pairs": [ + { + "bound": -0.947985, + "epochs": 3, + "pair": [ + 233, + 340 + ] + }, + { + "bound": -0.957206, + "epochs": 2, + "pair": [ + 274, + 467 + ] + }, + { + "bound": -1.958152, + "epochs": 2, + "pair": [ + 297, + 465 + ] + }, + { + "bound": 2.011165, + "epochs": 2, + "exact_best_gain": -1.968371, + "exact_removed_ranks": [ + 4, + 5 + ], + "pair": [ + 297, + 684 + ] + }, + { + "bound": -0.957206, + "epochs": 2, + "pair": [ + 323, + 464 + ] + } + ], + "pairs": { + "best_gain": -1.95666, + "best_pair": [ + 352, + 369 + ], + "best_removed_ranks": [ + 6, + 6 + ], + "closed_by_row_class_bound": 5638, + "enumerated": 392, + "with_shared_query": 6030 + }, + "single": { + "best_gain": 0.0, + "epochs_per_helper": 1, + "helpers": 415, + "max_removed_rank_mass": 7, + "neutral": [ + 684 + ], + "positive": 0, + "profile": [ + [ + [], + [ + 1, + 1 + ], + 1 + ], + [ + [], + [ + 1, + 2, + 2 + ], + 2 + ], + [ + [], + [ + 4 + ], + 1 + ], + [ + [], + [ + 5 + ], + 92 + ], + [ + [], + [ + 6 + ], + 17 + ], + [ + [ + 1 + ], + [ + 1, + 2, + 2 + ], + 6 + ], + [ + [ + 1 + ], + [ + 1, + 4 + ], + 76 + ], + [ + [ + 1 + ], + [ + 5 + ], + 30 + ], + [ + [ + 1 + ], + [ + 6 + ], + 10 + ], + [ + [ + 2 + ], + [ + 2 + ], + 70 + ], + [ + [ + 2 + ], + [ + 3 + ], + 110 + ] + ] + }, + "source": { + "events": 14794, + "helpers": 415, + "owned": 48, + "paid": { + "1": 1281, + "2": 1338, + "3": 58, + "4": 57, + "5": 102, + "6": 10 + }, + "wires": 685 + }, + "target": { + "calls": 18, + "invoice_moment_at_C": -40.952037, + "min_free_rank2_helpers_in_any_set_reaching_C": 5, + "needed_per_local_word": 2.275113 + } +} diff --git a/research/g20-dynamic-capture-census/SOURCES.json b/research/g20-dynamic-capture-census/SOURCES.json new file mode 100644 index 0000000000..084d05f56e --- /dev/null +++ b/research/g20-dynamic-capture-census/SOURCES.json @@ -0,0 +1,66 @@ +{ + "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/kappa-0035-target-atlas/bit-targets.md", + "usage": "provenance", + "git_blob": "bc7dcff05dcbd5054332fe6367e858283ef04914", + "sha256": "42898aa5879021b71659225e6c012dc8b3f33b74d6a29744139afa1d0094ca0d" + }, + { + "path": "research/bit-g20-entry-capture-capacity/PROOF.md", + "usage": "provenance", + "git_blob": "c92a5842aaa8544b974e5beda3bd9bfc6120aeee", + "sha256": "58b53af43e125aa1ac0f04d5d5c915ca3157f0d4facc055f92f35ab7236b8e66" + }, + { + "path": "research/g20-conjugation-admission/WORD.json.gz", + "usage": "input", + "git_blob": "3877a72d8a15adb03f6492f7d2fd8fa902ecb639", + "sha256": "8dd441fdb9c8923df06eb5ebfda37d03e4539f2305763e688d8c7025d196c4b1" + }, + { + "path": "research/g20-conjugation-admission/INVOICE.json", + "usage": "input", + "git_blob": "08ed5c4b9b0b03e16cd74b35880839c08a7125f4", + "sha256": "a2a9559bdc3b3293eae111c927e02e7cccecbaa0d35299c352421a58b3609296" + }, + { + "path": "research/g20-conjugation-admission/LOCAL-RESULT.json", + "usage": "input", + "git_blob": "29cd42b8baa531f2598b9b8894fd514c754ed17c", + "sha256": "ec37bf5ddf743caf6a415bd4ce6fcd9c0f40922f0066ea79f6d2321ee0f18e96" + }, + { + "path": "research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json", + "usage": "input", + "git_blob": "9edf8d95b45a9c9c766a956bfcd3c19cf07bc13c", + "sha256": "0d99fc6b8f45c03dfba5252a03dd9e7fe23be3a7593dfe15368e34da6629a654" + }, + { + "path": "research/g20-late-binding-admission/prior/WORD.json.gz", + "usage": "input", + "git_blob": "976059558e4e4881decab75d8af41bee7be1ad93", + "sha256": "647d944a94a744b20a68a07180415caf3a8a130111f5907d40d7f617f1b60eef" + }, + { + "path": "research/g20-late-binding-admission/CUTS.json", + "usage": "input", + "git_blob": "dd8a3fe26b12918768da145fc76c2485a0844f70", + "sha256": "9a95f5399c7af312c8b41b3fe8b93f0b238220f20f7ed4b19c9dab54ae673a66" + } + ] +} diff --git a/research/g20-dynamic-capture-census/TASK.json b/research/g20-dynamic-capture-census/TASK.json new file mode 100644 index 0000000000..7d8a2bc751 --- /dev/null +++ b/research/g20-dynamic-capture-census/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Exact census of dynamic owned-helper captures (atlas PR5586 B1) on the final PR5708 G20 local word: every retained helper with an arbitrary injected payload at every dead/live epoch boundary; the five helper pairs whose joint ownership lengthens a dead interval; every helper pair under the individual schedule; and a joint parity-token bound for owned sets of any size. Positive control on the PR5667 word.", + "scope_change_reason": "The card asks for one uncovered changed helper path. PR5586 B1 and the open questions of PR5604/PR5671 point to multi-epoch and joint dynamic captures as the uncovered class; before choosing an instance this package checks the whole class on the exact word.", + "bottleneck_link": "The ordinary BIT target B* = 0.0037 needs +40.95 of signed moment over the PR5708 invoice, i.e. +2.28 per local word across 18 calls; each owned full helper debits 8^t = 7.94. The census shows how much of that a capture can repay on this word.", + "budget_minutes": 300, + "stop_rule": "Stop when single helpers, all epochs, joint-dead pairs and all helper pairs are decided exactly, the control rediscovers the nine PR5671 cuts, and the receipt is reproduced; leave larger joint sets as an explicit open question with the bound that remains.", + "outcome": "completed", + "evidence": "README.md, PROOF.md, RESULT.json, capture.py, verify.py.", + "author": "Matarener", + "ai_assistance": "Substantial Anthropic Claude assistance (Claude Code) for the implementation and calculations. No package code imported; no independent human acceptance claimed.", + "open_questions": [ + { + "question": "Does any owned set of three or more helpers pay its targets on the PR5708 word (complete joint search)?", + "why_it_matters": "It is the only part of the single-word B1 capture class left open here. The joint parity-token bound closes every set except those built mainly from the helpers with a free rank-2 own query; reaching 0.0037 would need at least the number of such helpers stated in RESULT.json joint_bound, all compatible.", + "first_step": "Restrict to helpers with a free rank-2 own query and their shared queries (RESULT.json joint_bound). Encode each candidate injection as an F2 vector of parity bits plus exact matrix-level equalities, and solve the weighted maximum consistent subset as an ILP or SAT/MaxSAT instance with the gain inequality as objective; verify any positive witness with capture.py exact replay.", + "blocked_by": "A new exact solver encoding (hours of compute); no new mathematics needed." + }, + { + "question": "Do changed words (new producers, paid frame conversions, address-dependent recoding) create helpers with more than one live interval or larger shared queries?", + "why_it_matters": "On this word every helper has exactly one live interval, so the multi-epoch premise of B1 has no instance; B1 needs a changed producer.", + "first_step": "Run capture.py analyze_sets on any new G20 successor word; a second live interval or a single-helper bound above zero is the signal.", + "blocked_by": "A changed word." + } + ] +} diff --git a/research/g20-dynamic-capture-census/VERIFY.json b/research/g20-dynamic-capture-census/VERIFY.json new file mode 100644 index 0000000000..c48e236409 --- /dev/null +++ b/research/g20-dynamic-capture-census/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/g20-conjugation-admission/WORD.json.gz", + "research/g20-conjugation-admission/INVOICE.json", + "research/g20-conjugation-admission/LOCAL-RESULT.json", + "research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json", + "research/g20-late-binding-admission/prior/WORD.json.gz", + "research/g20-late-binding-admission/CUTS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 570, + "checks": "Authenticate inputs and the PR5708 local paid profile; exact single-helper capture census with arbitrary injections at every dead/live epoch boundary (0 paying, one live interval per helper); five joint-dead pairs (exact, none pays); all helper pairs with a shared query (row-class bound plus exact enumeration, none pays); joint parity-token bound; positive control rediscovers the nine PR5671 late-binding captures on the PR5667 word; RESULT.json compared in full." + } + ] +} diff --git a/research/g20-dynamic-capture-census/capture.py b/research/g20-dynamic-capture-census/capture.py new file mode 100644 index 0000000000..95324aa073 --- /dev/null +++ b/research/g20-dynamic-capture-census/capture.py @@ -0,0 +1,667 @@ +#!/usr/bin/env python3 +"""Dynamic capture census for a G20 BIT local word (atlas PR5586 target B1). Apache-2.0. + +Prepared for Matarener with Claude (Anthropic), via Claude Code. Python 3.12, standard library only. + +Word contract (as in the G20 packages): every wire carries a payload, an F2-linear combination of the +input symbols x_0..x_{n-1}, each with an exact 8x8 rational operator; ADD d s f adds wire s into wire d +(both in frame f); Q d s t k is a paid native query of rank k with action R_s R_t (R_f = I - 2 P_f); +ZERO_Q is a free move of a zero payload; ERASE/INIT only touch owned wires. + +A capture owns a retained helper h (its rank-r target is debited, r^t with t = 1 - C). While h is +dead-forward (its content cannot reach any retained output) every write into h is dropped and h is kept zero, +so its own queries there are free. At the end of each dead interval h receives an arbitrary injected payload +w (ERASE plus same-frame ADDs). A paid query is removed iff its whole symbolic payload becomes zero. + +Exactness: one forward replay injects a fresh symbol u_(h,j) into h at the last dead moment of each of its +dead intervals. With h owned, the true payload of query q is + p_q = rest_q + sum_(h,j) M_(q,h,j) (w_(h,j) + snap_(h,j)), +where rest_q is the replayed payload with u-terms removed and the owned input symbols set to zero, snap is +the replayed content of h just before the injection (owned inputs zeroed), and every coefficient M is a +single matrix (checked). A query depending on one injected symbol is removed iff w equals the unique value +M^-1 (rest_q + M snap); such queries are grouped by that value. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Fr +from hashlib import sha256 +import gzip, itertools, json, math + + +# ---------------------------------------------------------------- exact 8x8 rational matrices +def _inv(m): + n = len(m) + a = [[Fr(x) for x in row] + [Fr(int(i == j)) for j in range(n)] for i, row in enumerate(m)] + for c in range(n): + p = next(i for i in range(c, n) if a[i][c] != 0) + a[c], a[p] = a[p], a[c] + v = a[c][c] + a[c] = [x / v for x in a[c]] + for i in range(n): + if i != c and a[i][c] != 0: + f = a[i][c] + a[i] = [x - f * y for x, y in zip(a[i], a[c])] + return tuple(tuple(row[n:]) for row in a) + + +def _to_int(a): + den = 1 + for row in a: + for x in row: + den = den * x.denominator // math.gcd(den, x.denominator) + return den, [[int(x * den) for x in row] for row in a] + + +def _mul(a, b): + """Exact rational product, computed over the integers with a common denominator.""" + da, ia = _to_int(a) + db, ib = _to_int(b) + cols = list(zip(*ib)) + d = da * db + return tuple(tuple(Fr(sum(x * y for x, y in zip(r, c)), d) for c in cols) for r in ia) + + +I8 = tuple(tuple(Fr(int(i == j)) for j in range(8)) for i in range(8)) + + +def _projector(B): + if not B: + return tuple(tuple(Fr(0) for _ in range(8)) for _ in range(8)) + Bt = tuple(map(tuple, zip(*B))) + return _mul(_mul(Bt, _inv(_mul(B, Bt))), B) + + +class Mats: + """Interned matrices; payload = dict matrix-id -> bitmask of symbols (F2 multiplicity).""" + def __init__(self): + self.ids, self.mats, self.prod, self.invs = {}, [], {}, {} + self.I = self.get(I8) + + def get(self, m): + i = self.ids.get(m) + if i is None: + i = self.ids[m] = len(self.mats) + self.mats.append(m) + return i + + def mul(self, a, b): + r = self.prod.get((a, b)) + if r is None: + r = self.prod[(a, b)] = self.get(_mul(self.mats[a], self.mats[b])) + return r + + def inv(self, a): + r = self.invs.get(a) + if r is None: + r = self.invs[a] = self.get(_inv(self.mats[a])) + return r + + +def padd(a, b): + out = dict(a) + for m, bits in b.items(): + z = out.get(m, 0) ^ bits + if z: + out[m] = z + else: + del out[m] + return out + + +def pleft(mats, M, p): + out = {} + for m, bits in p.items(): + mm = mats.mul(M, m) + z = out.get(mm, 0) ^ bits + if z: + out[mm] = z + else: + del out[mm] + return out + + +def pmask(p, mask): + """Keep only the symbols in mask (substitute all others by zero).""" + out = {} + for m, b in p.items(): + b &= mask + if b: + out[m] = b + return out + + +def pkey(mats, p): + if not p: + return 'ZERO' + rows = sorted((mats.mats[m], b) for m, b in p.items()) + return sha256(repr(rows).encode()).hexdigest()[:32] + + +def support(p): + s = 0 + for b in p.values(): + s |= b + return s + + +def parity(p): + """F2-linear bitmap: symbol multiplicities summed over all matrices. For an invertible single matrix M, + parity(M p) = parity(p), so a vanishing payload has zero parity.""" + s = 0 + for b in p.values(): + s ^= b + return s + + +# ---------------------------------------------------------------- the word +class Word: + def __init__(self, word_path, frames_path, main_wires=222): + with open(word_path, 'rb') as fh: + w = json.loads(gzip.decompress(fh.read())) + with open(frames_path) as fh: + frames = json.load(fh)['frames'] + self.rec, self.owned, self.start, self.final = w['records'], set(w['owned']), w['start'], w['final'] + self.width = len(self.start) + self.mats = Mats() + used = {x for x in self.start + self.final if x is not None} + for e in self.rec: + if e[0] == 'ADD': + used.add(e[3]) + elif e[0] in ('Q', 'ZERO_Q'): + used |= {e[2], e[3]} + elif e[0] in ('ERASE', 'INIT') and e[2] is not None: + used.add(e[2]) + self.dim = {f: frames[str(f)]['dim'] for f in used} + self.R = {} + for f in used: + P = _projector(tuple(tuple(Fr(x) for x in r) for r in frames[str(f)]['B'])) + self.R[f] = self.mats.get(tuple(tuple(I8[i][j] - 2 * P[i][j] for j in range(8)) for i in range(8))) + self.qm = {} + self.helpers = [i for i in range(self.width) if i not in self.owned and i >= main_wires] + self.target_rank = {h: abs(self.dim[self.final[h]] - self.dim[self.start[h]]) for h in self.helpers} + self.inmask = (1 << self.width) - 1 + + def qmat(self, s, t): + r = self.qm.get((s, t)) + if r is None: + r = self.qm[(s, t)] = self.mats.mul(self.R[s], self.R[t]) + return r + + # forward replay with optional injections {event index: [(wire, symbol bit)]} applied before the event + def replay(self, inject=None): + inject = inject or {} + mats, st = self.mats, list(self.start) + fld = [{mats.I: 1 << i} for i in range(self.width)] + queries, snaps, first_read, paid = [], {}, {}, Counter() + for ix, e in enumerate(self.rec): + for (h, bit) in inject.get(ix, ()): + snaps[bit] = fld[h] + fld[h] = padd(fld[h], {mats.I: 1 << bit}) + op, d = e[0], e[1] + if op == 'ERASE': + fld[d] = {} + st[d] = e[2] + elif op == 'INIT': + st[d] = e[2] + elif op == 'ADD': + s, f = e[2], e[3] + if not (st[d] == f == st[s]): + raise ValueError('ADD frame mismatch at %d' % ix) + first_read.setdefault(s, ix) + fld[d] = padd(fld[d], fld[s]) + elif op == 'Q': + if st[d] != e[2] or abs(self.dim[e[2]] - self.dim[e[3]]) != e[4]: + raise ValueError('query frame/rank at %d' % ix) + paid[e[4]] += 1 + queries.append((ix, d, e[4], fld[d])) + fld[d] = pleft(mats, self.qmat(e[2], e[3]), fld[d]) + st[d] = e[3] + elif op == 'ZERO_Q': + if pmask(fld[d], self.inmask): + raise ValueError('free move of a nonzero payload at %d' % ix) + st[d] = e[3] + else: + raise ValueError('unknown op ' + op) + return queries, snaps, first_read, paid, fld + + # backward replay: for each helper, a bytearray dead[ix] = content of h just before event ix cannot reach + # any retained output other than those in ignore(h) (always including h itself). + def dead_profiles(self, helpers, ignore=None): + mats = self.mats + adj = [({mats.I: 1 << i} if i not in self.owned else {}) for i in range(self.width)] + ign = {h: (1 << h) | sum(1 << x for x in (ignore or {}).get(h, ())) for h in helpers} + n = len(self.rec) + dead = {h: bytearray(n + 1) for h in helpers} + + cur = {h: (support(adj[h]) & ~ign[h]) == 0 for h in helpers} + for h in helpers: + dead[h][n] = cur[h] + for ix in range(n - 1, -1, -1): + e = self.rec[ix] + op, d = e[0], e[1] + touched = d + if op == 'ADD': + adj[e[2]] = padd(adj[e[2]], adj[d]) + touched = e[2] + elif op == 'Q': + Q = self.qmat(e[2], e[3]) + adj[d] = {mats.mul(m, Q): b for m, b in adj[d].items()} + elif op == 'ERASE': + adj[d] = {} + if touched in cur: + cur[touched] = (support(adj[touched]) & ~ign[touched]) == 0 + for h in helpers: + dead[h][ix] = cur[h] + return dead + + +def intervals(db): + """Maximal runs of True in db (indices 0..n); returns [(a, b)] with dead before events a..b.""" + out, ix, n = [], 0, len(db) + while ix < n: + a = db.find(1, ix) + if a < 0: + break + b = db.find(0, a) + if b < 0: + b = n + out.append((a, b - 1)) + ix = b + return out + + +def moment(k, t): + return k ** t + + +# ---------------------------------------------------------------- set analysis +def analyze_sets(W, sets, C, ignore_partners=False): + """For each owned set H (tuple of helpers): epochs, dead own-wire queries, exact single-symbol groups, + multi-symbol queries. Returns per-set records. With ignore_partners, deadness of h in H ignores all + outputs of H; otherwise only h's own output.""" + t = 1 - float(C) + helpers = sorted({h for H in sets for h in H}) + out = [] + if ignore_partners: + todo = [(H, W.dead_profiles(list(H), {h: set(H) for h in H})) for H in sets] + else: + dp = W.dead_profiles(helpers) + todo = [(H, dp) for H in sets] + n = len(W.rec) + cache = {} + ivs = {} + for H, dead in todo: + if ignore_partners: + ivs = {} + for h in (H if ignore_partners else helpers): + if h not in ivs: + ivs[h] = intervals(dead[h]) + key = (H if ignore_partners else None) + inject, syms = defaultdict(list), [] + bit = W.width + for h in (H if ignore_partners else helpers): + for j, (a, b) in enumerate(ivs[h]): + if b < n: + inject[b].append((h, bit)) + syms.append((h, j, a, b, bit)) + bit += 1 + if key not in cache: + queries, snaps, _, _, fld = W.replay(inject) + sups = [support(q[3]) for q in queries] + bybit, bywire = defaultdict(list), defaultdict(list) + for qi, (ix, d, k, p) in enumerate(queries): + bywire[d].append(qi) + s_ = sups[qi] >> W.width + while s_: + low = s_ & -s_ + bybit[low.bit_length() - 1 + W.width].append(qi) + s_ ^= low + outsup = [support(f) for f in fld] + cache[key] = (queries, snaps, sups, bybit, bywire, outsup) + out.append(_set_record(W, H, dead, syms, cache[key], t, ivs)) + return out + + +def _set_record(W, H, dead, syms, ctx, t, ivs): + queries, snaps, sups, bybit, bywire, outsup = ctx + mats = W.mats + Hs = set(H) + mysyms = [s for s in syms if s[0] in Hs] + keep = W.inmask & ~sum(1 << h for h in H) # owned inputs substituted by zero + symmask = sum(1 << s[4] for s in mysyms) + allsym = sum(1 << s[4] for s in syms) + # no injected symbol of h may reach a retained output other than ignored ones + for (h, j, a, b, bt) in mysyms: + for i in range(W.width): + if i in W.owned or i in Hs: + continue + if outsup[i] >> bt & 1: + raise ValueError('injected symbol of %d reaches retained output %d' % (h, i)) + reads = defaultdict(list) + for ix, e in enumerate(W.rec): + if e[0] == 'ADD' and e[2] in Hs: + reads[e[2]].append(ix) + free = {} + for h in H: + for (a, b) in ivs[h]: + if not any(a <= r < b for r in reads[h]): + free[h] = free.get(h, []) + [(a, b)] + dead_own, groups, multi = [], defaultdict(lambda: defaultdict(list)), [] + cand = sorted({qi for s_ in mysyms for qi in bybit.get(s_[4], ())} | {qi for h in H for qi in bywire.get(h, ())}) + for qi in cand: + ix, d, k, p = queries[qi] + if d in Hs and any(a <= ix < b for (a, b) in free.get(d, ())): + dead_own.append((ix, d, k)) + continue + dep = [s for s in mysyms if sups[qi] >> s[4] & 1] + if not dep: + continue + if len(dep) > 1: + # a removed query satisfies parity(rest) + sum parity(snap_s) = sum_{s in dep} parity(w_s): + # removed queries with the same dependence set share this parity label + label = parity(pmask(p, keep)) + for s_ in dep: + label ^= parity(pmask(snaps[s_[4]], keep)) + multi.append((ix, d, k, [(s_[0], s_[1]) for s_ in dep], label)) + continue + h, j, a, b, bt = dep[0] + coef = [m for m, bb in p.items() if bb >> bt & 1] + if len(coef) != 1: + raise ValueError('composite coefficient at query %d' % ix) + M = coef[0] + rest = pmask(p, keep) + rest = padd(rest, pleft(mats, M, pmask(snaps[bt], keep))) + v = pleft(mats, mats.inv(M), rest) + groups[(h, j)][pkey(mats, v)].append((ix, d, k)) + epochs = [] + for (h, j, a, b, bt) in mysyms: + g = groups.get((h, j), {}) + best = max(g.items(), key=lambda kv: (sum(moment(x[2], t) for x in kv[1]), kv[0])) if g else None + epochs.append({'helper': h, 'epoch': j, 'dead_from': a, 'inject_before': b, 'groups': len(g), + 'best_value': best[0] if best else None, + 'best': [list(x) for x in best[1]] if best else []}) + debit = sum(moment(W.target_rank[h], t) for h in H) + killed_single = sum(moment(x[2], t) for e in epochs for x in e['best']) + dmass = sum(moment(k, t) for _, _, k in dead_own) + classes = defaultdict(lambda: defaultdict(float)) + for ix, d, k, dep, label in multi: + classes[tuple(map(tuple, dep))][label] += moment(k, t) + mmass = sum(max(c.values()) for c in classes.values()) + return {'set': list(H), 'epochs': epochs, 'dead_own': [list(x) for x in dead_own], + 'multi': [[ix, d, k, dep] for ix, d, k, dep, _ in multi], 'multi_class_mass': mmass, 'debit': debit, + 'bound': dmass + killed_single + mmass - debit, 'exact_if_no_multi': not multi, + 'groups_by_epoch': {'%d/%d' % hk: {kk: [list(x) for x in vv] for kk, vv in g.items()} + for hk, g in groups.items()}} + + +# ---------------------------------------------------------------- pairs under the individual schedule +def pair_census(W, singles, C): + """Exact two-helper census. Each owned helper keeps its individual dead intervals (one live interval + each on the PR5708 word). Queries depending on both injections are removed only if their F2 bitmap row + equals e_a+e_b+bitmap(w_a)+bitmap(w_b); hence all removed double queries share one row (row-class bound). + Pairs whose bound is positive are enumerated exactly over w_a in groups(a)+{0}, w_b forced by a double or + in groups(b)+{0}, and symmetrically; the doubles-only case is bounded by the row class.""" + t = 1 - float(C) + mats = W.mats + rec1 = {r['set'][0]: r for r in singles} + helpers = sorted(rec1) + hmask = sum(1 << h for h in helpers) + dead_ix = {h: {x[0] for x in rec1[h]['dead_own']} for h in helpers} + inj = {} + bit = W.width + inject = defaultdict(list) + for h in helpers: + eps = rec1[h]['epochs'] + if len(eps) != 1: + raise ValueError('pair census assumes one live interval per helper') + inject[eps[0]['inject_before']].append((h, bit)) + inj[h] = bit + bit += 1 + queries, snaps, _, _, _ = W.replay(inject) + # bitmap rows of the base word (for row classes) + shared = defaultdict(list) + for qi, (ix, d, k, p) in enumerate(queries): + sup = support(p) + hs = [h for h in helpers if sup >> inj[h] & 1 and not (d == h and ix in dead_ix[h])] + for a, b in itertools.combinations(hs, 2): + if (d == a and ix in dead_ix[a]) or (d == b and ix in dead_ix[b]): + continue + shared[(a, b)].append(qi) + G = {h: sum(moment(x[2], t) for e in rec1[h]['epochs'] for x in e['best']) for h in helpers} + Dm = {h: sum(moment(x[2], t) for x in rec1[h]['dead_own']) for h in helpers} + deb = {h: moment(W.target_rank[h], t) for h in helpers} + + stats = Counter() + exact = [] + best_overall = None + for (a, b), qis in sorted(shared.items()): + stats['pairs'] += 1 + rows = Counter() + for qi in qis: + ix, d, k, p = queries[qi] + rows[_true_row(W, p, (a, b), inj, snaps)] += moment(k, t) + rmax = max(rows.values()) + bound = Dm[a] + Dm[b] + G[a] + G[b] + rmax - deb[a] - deb[b] + donly = Dm[a] + Dm[b] + rmax - deb[a] - deb[b] + if donly > 0: + raise ValueError('doubles-only bound positive for pair %s' % ((a, b),)) + if bound <= 0: + stats['closed_by_row_class_bound'] += 1 + continue + stats['enumerated'] += 1 + g = _pair_exact(W, queries, snaps, inj, a, b, qis, rec1, t) + exact.append({'pair': [a, b], 'bound': bound, 'shared': len(qis), 'best_gain': g[0], + 'best_ranks': g[1]}) + if best_overall is None or g[0] > best_overall[0]: + best_overall = (g[0], a, b, g[1]) + stats['pairs_without_shared_query_max_gain'] = max(G[h] + Dm[h] - deb[h] for h in helpers) * 2 + return dict(stats), exact, best_overall + + +def _true_row(W, p, H, inj, snaps): + """Class label of a double query: its payload with owned inputs zeroed, snapshots folded in, and the + injected symbols replaced by marker bits; two doubles can both vanish only if these rows coincide.""" + keep = W.inmask & ~sum(1 << h for h in H) + row = parity(pmask(p, keep)) + for h in H: + bt = inj[h] + coef = [m for m, bb in p.items() if bb >> bt & 1] + if len(coef) != 1: + raise ValueError('composite coefficient') + row ^= parity(pmask(snaps[bt], keep)) + return row + + +def _pair_exact(W, queries, snaps, inj, a, b, qis, rec1, t): + mats = W.mats + keep = W.inmask & ~((1 << a) | (1 << b)) + + def parts(p): + Ma = [m for m, bb in p.items() if bb >> inj[a] & 1] + Mb = [m for m, bb in p.items() if bb >> inj[b] & 1] + rest = pmask(p, keep) + if Ma: + rest = padd(rest, pleft(mats, Ma[0], pmask(snaps[inj[a]], keep))) + if Mb: + rest = padd(rest, pleft(mats, Mb[0], pmask(snaps[inj[b]], keep))) + return (Ma[0] if Ma else None), (Mb[0] if Mb else None), rest + + dead_a = [x for x in rec1[a]['dead_own']] + dead_b = [x for x in rec1[b]['dead_own']] + dset = {x[0] for x in dead_a + dead_b} + qa, qb, qd = [], [], [] + for qi, (ix, d, k, p) in enumerate(queries): + if ix in dset and d in (a, b): + continue + sup = support(p) + ha, hb = sup >> inj[a] & 1, sup >> inj[b] & 1 + if ha or hb: + Ma, Mb, rest = parts(p) + (qd if (ha and hb) else qa if ha else qb).append((k, Ma, Mb, rest)) + va = {'ZERO': {}} + for k, Ma, Mb, rest in qa: + v = pleft(mats, mats.inv(Ma), rest) + va[pkey(mats, v)] = v + vb = {'ZERO': {}} + for k, Ma, Mb, rest in qb: + v = pleft(mats, mats.inv(Mb), rest) + vb[pkey(mats, v)] = v + cands = [] + for wa in va.values(): + for wb in vb.values(): + cands.append((wa, wb)) + for k, Ma, Mb, rest in qd: + cands.append((wa, pleft(mats, mats.inv(Mb), padd(rest, pleft(mats, Ma, wa))))) + for wb in vb.values(): + for k, Ma, Mb, rest in qd: + cands.append((pleft(mats, mats.inv(Ma), padd(rest, pleft(mats, Mb, wb))), wb)) + base = sum(moment(x[2], t) for x in dead_a + dead_b) - moment(W.target_rank[a], t) - moment(W.target_rank[b], t) + best = None + seen = set() + for wa, wb in cands: + sig = (pkey(mats, wa), pkey(mats, wb)) + if sig in seen: + continue + seen.add(sig) + killed = [] + for k, Ma, Mb, rest in qa: + if not padd(rest, pleft(mats, Ma, wa)): + killed.append(k) + for k, Ma, Mb, rest in qb: + if not padd(rest, pleft(mats, Mb, wb)): + killed.append(k) + for k, Ma, Mb, rest in qd: + if not padd(padd(rest, pleft(mats, Ma, wa)), pleft(mats, Mb, wb)): + killed.append(k) + g = base + sum(moment(k, t) for k in killed) + if best is None or g > best[0]: + best = (g, sorted(killed)) + return best + + +# ---------------------------------------------------------------- joint token bound (any number of helpers) +def token_bound(W, singles, C): + """Joint bound for any owned set under the individual schedule. Removing query q forces + parity(p_q) = sum over owned helpers h it depends on of (e_h + parity(w_h) + parity(writes into h)), + so every removed base-word parity row lies in a d-dimensional span for d owned helpers. ceil(4 r^t) + copies of each eligible row are greedily partitioned into N F2-independent sets; a d-dimensional span + meets each in at most d vectors, so removed t-mass <= N d / 4 (plus the free dead own-wire queries).""" + t = 1 - float(C) + helpers = sorted(r['set'][0] for r in singles) + hmask = sum(1 << h for h in helpers) + deadq = {x[0] for r in singles for x in r['dead_own']} + rows = [1 << i for i in range(W.width)] + eligible = [] + for ix, e in enumerate(W.rec): + op, d = e[0], e[1] + if op == 'ERASE': + rows[d] = 0 + elif op == 'ADD': + rows[d] ^= rows[e[2]] + elif op == 'Q' and rows[d] & hmask and ix not in deadq: + eligible.append((ix, d, e[4], rows[d])) + remaining = Counter() + for ix, d, k, row in eligible: + remaining[row] += math.ceil(4 * k ** t - 1e-12) + tokens = sum(remaining.values()) + sets = [] + while remaining: + bs, chosen = _Basis(), [] + for r, cnt in sorted(remaining.items(), key=lambda kv: (-kv[1], kv[0])): + if bs.add(r): + chosen.append(r) + for r in chosen: + remaining[r] -= 1 + if not remaining[r]: + del remaining[r] + sets.append(len(chosen)) + return {'eligible': len(eligible), 'distinct_rows': len({q[3] for q in eligible}), 'tokens': tokens, + 'N': len(sets), 'set_sizes': sets, 'capacity_per_owned_helper': len(sets) / 4} + + +class _Basis: + def __init__(self): + self.b = {} + + def reduce(self, v): + while v: + p = v.bit_length() - 1 + if p not in self.b: + return v + v ^= self.b[p] + return 0 + + def add(self, v): + v = self.reduce(v) + if v: + self.b[v.bit_length() - 1] = v + return True + return False + + def contains(self, v): + return self.reduce(v) == 0 + + +# ---------------------------------------------------------------- joint deadness +def partner_pairs(W): + """Ordered pairs (h, p): at some time the content of helper h reaches no retained output except those + of h and of one other helper p. Owning both can lengthen h's dead intervals.""" + mats = W.mats + adj = [({mats.I: 1 << i} if i not in W.owned else {}) for i in range(W.width)] + hmask = sum(1 << h for h in W.helpers) + found = set() + hs = set(W.helpers) + + def check(h): + u = support(adj[h]) & ~(1 << h) + if u and not (u & ~hmask) and not (u & (u - 1)): + found.add((h, u.bit_length() - 1)) + for h in W.helpers: + check(h) + for ix in range(len(W.rec) - 1, -1, -1): + e = W.rec[ix] + op, d = e[0], e[1] + touched = d + if op == 'ADD': + adj[e[2]] = padd(adj[e[2]], adj[d]) + touched = e[2] + elif op == 'Q': + Q = W.qmat(e[2], e[3]) + adj[d] = {mats.mul(m, Q): b for m, b in adj[d].items()} + elif op == 'ERASE': + adj[d] = {} + if touched in hs: + check(touched) + return sorted(found) + + +def reads_before_injection(W, singles): + """Number of ADD reads of each owned helper before its injection point (must be zero for the + parity argument: the owned input symbol then never leaves its own wire).""" + bad = {} + for r in singles: + h = r['set'][0] + b = r['epochs'][0]['inject_before'] + n = sum(1 for ix in range(b) if W.rec[ix][0] == 'ADD' and W.rec[ix][2] == h) + if n: + bad[h] = n + return bad + + +def exact_joint_pair(W, rec, C): + """Exact two-helper search under the joint schedule of rec (from analyze_sets with ignore_partners): + requires one injection per helper; same candidate enumeration as pair_census.""" + t = 1 - float(C) + a, b = rec['set'] + eps = rec['epochs'] + need = [e for e in eps if e['best'] or any(h == e['helper'] and j == e['epoch'] + for m in rec['multi'] for (h, j) in m[3])] + if sorted(e['helper'] for e in need) != [a, b]: + raise ValueError('exact_joint_pair needs one active epoch per helper') + inject, inj, bit = defaultdict(list), {}, W.width + for e in need: + inject[e['inject_before']].append((e['helper'], bit)) + inj[e['helper']] = bit + bit += 1 + queries, snaps, _, _, _ = W.replay(inject) + rec1 = {h: {'dead_own': [x for x in rec['dead_own'] if x[1] == h]} for h in (a, b)} + return _pair_exact(W, queries, snaps, inj, a, b, None, rec1, t) diff --git a/research/g20-dynamic-capture-census/verify.py b/research/g20-dynamic-capture-census/verify.py new file mode 100644 index 0000000000..9b568c449d --- /dev/null +++ b/research/g20-dynamic-capture-census/verify.py @@ -0,0 +1,157 @@ +#!/usr/bin/env python3 +"""Verify the dynamic capture census on the final G20 BIT word (PR5708). Apache-2.0. + +Prepared for Matarener with Claude (Anthropic), via Claude Code. Python 3.12, standard library only. +Checks: (0) pinned inputs and the PR5708 local paid profile; (1) single-helper captures with any injected +payload and all dead/live epochs; (2) helper pairs whose joint ownership lengthens a dead interval; +(3) exact two-helper census under the individual schedule; (4) joint token bound for any owned set; +(5) positive control: on the PR5667 word the single census rediscovers exactly the nine PR5665/PR5671 +late-binding captures; (6) RESULT.json equals the recomputed receipt. `--write` regenerates RESULT.json. +""" +from collections import Counter +from fractions import Fraction as Fr +from hashlib import sha256 +from pathlib import Path +import importlib.util, json, sys, time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FRAMES = ROOT/'research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json' +WORD = ROOT/'research/g20-conjugation-admission/WORD.json.gz' +LOCAL = ROOT/'research/g20-conjugation-admission/LOCAL-RESULT.json' +INVOICE = ROOT/'research/g20-conjugation-admission/INVOICE.json' +WORD5667 = ROOT/'research/g20-late-binding-admission/prior/WORD.json.gz' +CUTS = ROOT/'research/g20-late-binding-admission/CUTS.json' +C_TARGET = Fr(37, 10000) +C_CONTROL = Fr(35, 10000) +EPS = 1e-9 + + +def need(ok, why): + if not ok: + raise SystemExit('FAIL: ' + why) + + +def log(*a): + print(time.strftime('%H:%M:%S'), *a, flush=True) + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + sys.modules[name] = mod + spec.loader.exec_module(mod) + return mod + + +def r6(x): + return round(x, 6) + + +def main(): + K = load('g20_capture', HERE/'capture.py') + for row in json.loads((HERE/'SOURCES.json').read_text())['files']: + if row['usage'] == 'input': + need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], 'input ' + row['path']) + log('PASS_INPUTS_AUTHENTICATED') + res = {'C': str(C_TARGET)} + t = 1 - float(C_TARGET) + + # (0) source profile + W = K.Word(WORD, FRAMES) + _, _, _, paid, _ = W.replay() + want = json.loads(LOCAL.read_text())['stats']['paid'] + need({str(k): v for k, v in paid.items()} == want, 'PR5708 local paid profile') + need(Counter(W.target_rank.values()) == Counter({8: 413, 4: 2}), 'helper targets') + res['source'] = {'events': len(W.rec), 'wires': W.width, 'owned': len(W.owned), 'helpers': len(W.helpers), + 'paid': {str(k): paid[k] for k in sorted(paid)}} + log('PASS_SOURCE_PROFILE', res['source']) + + # (1) single helpers + singles = K.analyze_sets(W, [(h,) for h in W.helpers], C_TARGET) + need(all(len(r['epochs']) == 1 for r in singles), 'one live interval per helper') + need(all(not r['multi'] for r in singles), 'single-symbol dependence') + need(not K.reads_before_injection(W, singles), 'no reads before injection') + need(all(len(r['dead_own']) <= 1 and all(x[2] <= 2 for x in r['dead_own']) for r in singles), + 'at most one free own query, rank <= 2') + best = max(r['bound'] for r in singles) + pos = [r['set'][0] for r in singles if r['bound'] > EPS] + need(not pos, 'a single-helper capture pays its target: %s' % pos) + hist = Counter((tuple(x[2] for x in r['dead_own']), tuple(sorted(x[2] for x in r['epochs'][0]['best']))) + for r in singles) + neutral = [r['set'][0] for r in singles if abs(r['bound']) <= EPS] + res['single'] = {'helpers': len(singles), 'epochs_per_helper': 1, 'positive': 0, 'best_gain': r6(best), + 'neutral': neutral, + 'max_removed_rank_mass': max(sum(x[2] for x in r['dead_own']) + + sum(x[2] for x in r['epochs'][0]['best']) for r in singles), + 'profile': sorted([[list(a), list(b), n] for (a, b), n in hist.items()])} + log('PASS_SINGLE', {k: v for k, v in res['single'].items() if k != 'profile'}) + + # (2) joint deadness + pp = K.partner_pairs(W) + sets = sorted({tuple(sorted(p)) for p in pp}) + joint = K.analyze_sets(W, sets, C_TARGET, ignore_partners=True) + res['joint_dead_pairs'] = [] + for r in joint: + row = {'pair': r['set'], 'epochs': len(r['epochs']), 'bound': r6(r['bound'])} + if r['bound'] > EPS: + g = K.exact_joint_pair(W, r, C_TARGET) + need(g[0] <= EPS, 'joint-dead pair pays: %s' % (r['set'],)) + row['exact_best_gain'] = r6(g[0]) + row['exact_removed_ranks'] = g[1] + res['joint_dead_pairs'].append(row) + log('PASS_JOINT_DEAD', res['joint_dead_pairs']) + + # (3) pairs + stats, exact, best2 = K.pair_census(W, singles, C_TARGET) + need(best2 is None or best2[0] <= EPS, 'pair pays: %s' % (best2,)) + need(stats['pairs_without_shared_query_max_gain'] <= EPS, 'pairs without shared query') + res['pairs'] = {'with_shared_query': stats['pairs'], 'closed_by_row_class_bound': + stats.get('closed_by_row_class_bound', 0), 'enumerated': stats.get('enumerated', 0), + 'best_gain': r6(best2[0]) if best2 else None, + 'best_pair': [best2[1], best2[2]] if best2 else None, + 'best_removed_ranks': best2[3] if best2 else None} + log('PASS_PAIRS', res['pairs']) + + # (4) joint token bound + tb = K.token_bound(W, singles, C_TARGET) + cap = tb['N'] / 4 + d2, d1 = 2 ** t, 1.0 + res['joint_bound'] = dict(tb, per_helper_gain_max={ + 'free_own_rank2': r6(cap + d2 - 8 ** t), 'free_own_rank1': r6(cap + d1 - 8 ** t), + 'no_free_own': r6(cap - 8 ** t)}, + helpers_with_free_rank2=sum(1 for r in singles if any(x[2] == 2 for x in r['dead_own'])), + ) + need(cap + d1 - 8 ** t < 0, 'token bound closes helpers without a rank-2 free query') + inv = json.loads(INVOICE.read_text()) + calls = 18 + F = sum(n * int(k) ** t for k, n in inv['targets'].items()) - sum(n * int(k) ** t for k, n in inv['paid'].items()) + need(F < 0, 'PR5708 invoice is below the target') + per_word = -F / calls + gmax = cap + d2 - 8 ** t + import math + res['target'] = {'invoice_moment_at_C': r6(F), 'calls': calls, 'needed_per_local_word': r6(per_word), + 'min_free_rank2_helpers_in_any_set_reaching_C': math.ceil(per_word / gmax)} + log('PASS_TOKEN_BOUND', {k: v for k, v in res['joint_bound'].items() if k != 'set_sizes'}) + + # (5) positive control + W2 = K.Word(WORD5667, FRAMES) + s2 = K.analyze_sets(W2, [(h,) for h in W2.helpers], C_CONTROL) + pos2 = sorted(r['set'][0] for r in s2 if r['bound'] > EPS) + sel = sorted(x['helper'] for x in json.loads(CUTS.read_text())['selected']) + need(pos2 == sel, 'control rediscovers PR5671 cuts: %s vs %s' % (pos2, sel)) + shapes = Counter((tuple(x[2] for x in r['dead_own']), tuple(sorted(x[2] for x in r['epochs'][0]['best']))) + for r in s2 if r['set'][0] in sel) + need(shapes == Counter({((1,), (7,)): 9}), 'control shapes H1+H7') + res['control_PR5667'] = {'C': str(C_CONTROL), 'positive': pos2, 'shape': 'free own H1 + removed H7'} + log('PASS_CONTROL', res['control_PR5667']) + + path = HERE/'RESULT.json' + if '--write' in sys.argv: + path.write_text(json.dumps(res, indent=1, sort_keys=True) + '\n') + need(json.loads(path.read_text()) == json.loads(json.dumps(res, sort_keys=True)), 'RESULT.json') + print('PASS_G20_DYNAMIC_CAPTURE_CENSUS', flush=True) + + +if __name__ == '__main__': + main()