diff --git a/research/recursive-multiterm-anchor-seedb9a23/CLAIM.md b/research/recursive-multiterm-anchor-seedb9a23/CLAIM.md new file mode 100644 index 0000000000..b95713d349 --- /dev/null +++ b/research/recursive-multiterm-anchor-seedb9a23/CLAIM.md @@ -0,0 +1,5 @@ +# Research claim and scope + +Claimed 2026-10-14 on [Discussion #1167](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18927047): `recursive-interfaces`, seed `b9a23cfa075749f3d518c00eef14918f`, task `persistent-boundary`, exact base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. The scope is a required arbitrary-dirty output anchor that accumulates (s\ge2) common bilinear products before one two-wave fanout to (q-1) other arbitrary-dirty outputs. + +The local construction, inverse, finite-state replay, complete child/addition ledger, and rank-only selected-profile screen are complete. It supplies no selected-word placement, supplier admission, or new \(\kappa\). This claim is released with the bounded local result; finding a realizable source incidence pattern remains open. diff --git a/research/recursive-multiterm-anchor-seedb9a23/README.md b/research/recursive-multiterm-anchor-seedb9a23/README.md new file mode 100644 index 0000000000..cbf5d4ef81 --- /dev/null +++ b/research/recursive-multiterm-anchor-seedb9a23/README.md @@ -0,0 +1,51 @@ +# Coalesce dirty-anchor fanout for a sum of shared products + +**Finite local construction with an exact cost ledger. No selected-provider admission or new \(\kappa\).** + +For (q\ge2) arbitrary-dirty output accumulators (A_i), suppose every output needs the same sum of (s\ge2) bilinear products plus one private product: + +\[ +A_i^{out}=A_i^{in}+P+u_iv_i, +\qquad P=\sum_{j=1}^{s}x_jy_j. +\] + +Use (A_0), a required output with arbitrary initial value (a_0), as the persistent anchor. First send the old anchor value across the other outputs, (A_i\leftarrow A_i-A_0). Accumulate all (s) common products in (A_0), so it now holds (a_0+P). Send that updated anchor once across the other outputs, (A_i\leftarrow A_i+A_0), and add each private product. The result is (A_i^{in}+P+u_iv_i) for every (i). Reversing these steps restores every arbitrary dirty accumulator and leaves every source unchanged. + +The complete local bill is: + +| Schedule | Rank-one child calls | Width-\(w\) row additions | +|---|---:|---:| +| Compute every common and private product independently | (q(s+1)) | 0 | +| Accumulate common sum, then broadcast once | (s+q) | (2(q-1)) | +| Repeat a two-wave dirty-anchor fanout for each common term | (s+q) | (2s(q-1)) | + +Thus the construction saves (s(q-1)) multiplication children over independent evaluation, and coalescing the shared sum saves (2(s-1)(q-1)) row additions versus repeating the one-term dirty-anchor schedule. If μ is the cost of one rank-one child and (A_w) is the complete cost of one width-\(w\) row addition, the net saving over independent evaluation is + +\[ +(q-1)(s\mu-2A_w), +\] + +so the local break-even is (\mu>2A_w/s). For (q=3,s=3,w=1), the direct schedule uses 12 children; the aggregate anchor uses 6 children and 4 row additions, while repeating single-term fanout uses the same 6 children and 12 row additions. These counts include every multiplication child and all inter-output additions. The construction requires no clean helper, source copy, frame change, or cleanup child. The multiplication-add interface must preserve its source factors and add its product into the requested arbitrary target; this is the inherited child contract. + +For scale only, eight hypothetical (q=3,s=3) blocks would remove 48 rank-one children from the selected fixed-word profile and introduce 32 scalar additions at width one. Waiving those additions, the exact fixed-word ceiling rises only 0.905971%, well below 5%. This is a rank-only screen, not evidence that the selected word contains eight instances. The source trace does not identify common-product output families or an admission schedule, so no supplier or \(\kappa\) gain is claimed. + +The verifier checks the polynomial identity and its inverse for (2\le q\le5), (1\le s\le4), exhausts all 60,073 dirty/input states for (q=s=2) over \(\mathbb F_2\) and \(\mathbb F_3\), and rejects schedules that omit either compensation wave or use the wrong sign. The odd field control checks the subtraction explicitly. + +## Reproduce + +Python 3.12 and the standard library are sufficient: + +```sh +python3 scripts/research_package.py --package research/recursive-multiterm-anchor-seedb9a23 --check-only +python3.12 scripts/research_package.py --package research/recursive-multiterm-anchor-seedb9a23 +``` + +Expected verifier line starts `PASS_RECURSIVE_MULTITERM_DIRTY_ANCHOR`. The selector assignment and original card are pinned in [TASK.json](TASK.json); selected-record and moment-model pins are listed in [SOURCES.json](SOURCES.json). The claim is [Discussion #1167](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18927047). + +This scope extends, but does not repackage, the one-common-product dirty-anchor construction in PR #1944 and active claim #18925817. It changes the object to a sum of (s\ge2) common products, accumulates that sum before fanout, and removes one compensation pair per extra common term. PR #1907 uses a clean required-output anchor; PR #1872 uses a clean helper and cleanup; PR #1155 treats general linear restoration coalescing rather than this bilinear output contract. + +## Open next questions + +Can the selected local word or another admitted supplier expose several common bilinear summands shared across at least two dirty output roles with a legal source, frame, and output schedule? The next step is a source-level incidence search for (s\ge2) common product terms, followed by a fully charged placement; the current selected trace does not encode enough operand ownership to infer such a pattern. + +**Attribution.** The selected construction remains credited to its authors (see the pinned selected record and manifest). This multi-term local identity, exact finite replay, and package were prepared by Cinna Davis with substantial OpenAI Codex assistance; no subagents were used. No independent human review or supplier-level result is claimed. diff --git a/research/recursive-multiterm-anchor-seedb9a23/RESULT.json b/research/recursive-multiterm-anchor-seedb9a23/RESULT.json new file mode 100644 index 0000000000..8757258398 --- /dev/null +++ b/research/recursive-multiterm-anchor-seedb9a23/RESULT.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "finite-local-construction", + "track": "recursive-interfaces", + "research_seed": "b9a23cfa075749f3d518c00eef14918f", + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "formula": { + "outputs": "A_i_out = A_i_in + sum_{j=1}^s x_j*y_j + u_i*v_i", + "direct_child_calls": "q*(s+1)", + "anchor_child_calls": "s+q", + "anchor_row_adds": "2*(q-1)*w", + "repeated_single_term_row_adds": "2*s*(q-1)*w", + "child_calls_saved": "s*(q-1)", + "row_adds_saved_vs_repeated_fanout": "2*(s-1)*(q-1)*w", + "net_saving": "(q-1)*(s*mu - 2*A_w)", + "break_even": "mu > 2*A_w/s" + }, + "exhaustive_dirty_states": 60073, + "exhaustive_domain": "q=2,s=2 over F_2 and F_3; all dirty outputs and all common/private scalar inputs", + "symbolic_domain": "2<=q<=5, 1<=s<=4 over the integer polynomial ring, forward and inverse", + "cost_example": { + "q": 3, + "s": 3, + "width": 1, + "direct_children": 12, + "anchor_children": 6, + "anchor_adds": 4, + "separate_fanout_adds": 12, + "children_saved": 6, + "fanout_adds_saved": 8, + "net_saving": "6*mu-4*A_1", + "break_even": "mu > 2*A_1/3" + }, + "illustrative_profile": { + "1": 2364, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "hypothetical_groups": 8, + "rank_one_children_saved": 48, + "row_adds_at_width_one": 32, + "baseline_ceiling_hi": "1690054109089/1000000000000000", + "illustrative_ceiling": [ + "68214620471/40000000000000", + "53292672243/31250000000000" + ], + "rank_only_gain_percent_hi": "0.9059711523232471", + "five_percent_gate": "missed even before charging row additions", + "supplier_admitted": false, + "new_kappa": false +} diff --git a/research/recursive-multiterm-anchor-seedb9a23/SOURCES.json b/research/recursive-multiterm-anchor-seedb9a23/SOURCES.json new file mode 100644 index 0000000000..c92590c8ea --- /dev/null +++ b/research/recursive-multiterm-anchor-seedb9a23/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ] +} diff --git a/research/recursive-multiterm-anchor-seedb9a23/TASK.json b/research/recursive-multiterm-anchor-seedb9a23/TASK.json new file mode 100644 index 0000000000..cc3ed1642d --- /dev/null +++ b/research/recursive-multiterm-anchor-seedb9a23/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "persistent-boundary", + "track": "recursive-interfaces", + "research_seed": "b9a23cfa075749f3d518c00eef14918f", + "priority_revision": 3, + "catalogue_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "predecessors": [ + { + "reference": "CrocSwap/integer-mult-bounds#1944", + "head": "11110e70e462f95a3e5adcb1d290cd67cd0807e7", + "relationship": "One common bilinear product through a two-wave arbitrary-dirty output anchor; this scope accumulates a sum with s>=2 before one fanout." + }, + { + "reference": "CrocSwap/integer-mult-bounds/discussioncomment-18925817", + "head": "da1ec3f0e25e84544b9ea1499a0155f2", + "relationship": "Active one-common-term dirty-anchor claim; the new parameter is a multi-term common sum and coalescing all compensation rounds." + }, + { + "reference": "CrocSwap/integer-mult-bounds#1907", + "head": "49b870f7a64f5f414208c3a82d4483b9cc95f5b8", + "relationship": "Clean required-output anchor, unlike the arbitrary-dirty anchor here." + }, + { + "reference": "CrocSwap/integer-mult-bounds#1872", + "head": "626ce207ec92a76f70a84843fe4ce3c39f67899d", + "relationship": "Clean shared helper with inverse cleanup; this scope has no helper and counts dirty-anchor compensation." + }, + { + "reference": "CrocSwap/integer-mult-bounds#1155", + "head": "d7d50406fbdc7ac4141ba454b2e2440dc74942db", + "relationship": "General linear restoration coalescing; this package gives a specific nonlinear bilinear output contract." + }, + { + "reference": "CrocSwap/integer-mult-bounds#1348", + "head": "74768ab408b1ae2ce2c7094b49457a86fcb06e94", + "relationship": "Coverage-law threshold screen; considered and declined because the active unpaid-coordinate route overlaps it." + }, + { + "reference": "CrocSwap/integer-mult-bounds#1791", + "head": "00d05a64898571cf57a14310fbcd3507ca99c5ec", + "relationship": "Centre-path sharing budget screen; considered and declined as a crowded alternate." + }, + { + "reference": "CrocSwap/integer-mult-bounds#1888", + "head": "9c0fd1d20d33353018a508fbc84e4189525c593c", + "relationship": "Mixed-rank centre-sharing overhead limit; considered and declined as a crowded alternate." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18927047", + "original_card": { + "id": "persistent-boundary", + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Write typed entry/exit contracts and a contracting multitype recurrence.", + "Derive a lower bound for the compulsory transitions of one proposed typed interface." + ], + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Find a concrete consecutive-call boundary in the selected review and list its entry/exit obligations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "allowed_variations": [ + "A two-type pilot or one explicit deferred restoration." + ], + "scope_change_triggers": [ + "Rewriting the old scalar recurrence as a matrix without eliminating work." + ], + "overlap_terms": [ + "persistent boundary", + "deferred restoration", + "multitype" + ] + }, + "scope_status": "refined", + "scope_change_reason": "The broad pair-of-calls card is narrowed to an explicit s>=2 shared-bilinear-sum interface: accumulate the common products in one required dirty output, then perform one two-wave compensation. The construction is checked as a local reversible map and is not presented as a selected supplier placement.", + "candidate_scope_triage": [ + { + "scope": "coverage-law-change", + "decision": "declined", + "reason": "Discussion #1587s unpaid-coordinate investigation and open coverage threshold PR #1348 cover the changed-coverage premise." + }, + { + "scope": "centre-path-sharing", + "decision": "declined", + "reason": "Discussion #1516 and open budget screens PR #1791/#1888 cover this route." + }, + { + "scope": "persistent-boundary multi-term dirty-anchor accumulation", + "decision": "selected", + "reason": "Active adjacent work covers one common product (s=1); the experiment changes the object to s>=2 common terms and coalesces their boundary compensation." + } + ], + "actual_scope": "For q>=2 arbitrary-dirty output accumulators with a required dirty anchor A0, realize A_i_out=A_i_in+sum_{j=1}^s x_j*y_j+u_i*v_i for s>=2 using s+q product-add children and 2(q-1) width-w row additions; compare with independent evaluation and repeated one-term dirty-anchor fanout.", + "bottleneck_link": "The persistent anchor avoids recomputing each shared bilinear term in every output and carries the entire shared sum across s consecutive child calls. It reduces q(s+1) product children to s+q, and coalesces 2s(q-1) one-term compensation additions into 2(q-1).", + "stop_rule": "Stop after deriving the exact forward and inverse schedules, checking the symbolic identity for 2<=q<=5 and 1<=s<=4, exhausting all dirty/input states for q=s=2 over F2 and F3, validating the full child/addition formulas, and computing the eight-block rank-only ceiling screen. Do not infer a selected-word instance or supplier admission without a source-incidence mapping.", + "evidence": "The reversible schedule is exact for arbitrary dirty outputs and read-only sources. Exhaustive q=s=2 replay covers 60,073 states across F2 and F3; symbolic checks cover the stated q,s rectangle. For q=3,s=3,w=1, independent evaluation uses 12 children, the aggregate anchor uses 6 children plus 4 row additions, and repeating the one-term fanout uses 12 row additions. Eight hypothetical blocks save 48 rank-one children and 32 width-one additions; even waiving additions, the selected fixed-word ceiling gain is only 0.905971%.", + "author": "Cinna Davis, with substantial OpenAI Codex assistance; no subagents.", + "ai_assistance": "Substantial assistance in overlap exploration, construction derivation, exact symbolic and finite-state verification, cost accounting, and package writing. No subagents were used.", + "outcome": "completed", + "open_questions": [ + { + "question": "Does any admitted local word contain at least two common bilinear summands shared across multiple arbitrary-dirty output roles?", + "why_it_matters": "The local schedule lowers child and compensation counts, but a source-level incidence match is needed before it can change a paid recursive profile.", + "first_step": "Decode one selected supplier's exact child input/output incidence and enumerate output families with at least two identical common product terms.", + "blocked_by": "The selected local trace records child order and rank but not enough operand ownership and destination map data to certify such a multi-term common sum." + } + ] +} diff --git a/research/recursive-multiterm-anchor-seedb9a23/VERIFY.json b/research/recursive-multiterm-anchor-seedb9a23/VERIFY.json new file mode 100644 index 0000000000..9de4d6de2a --- /dev/null +++ b/research/recursive-multiterm-anchor-seedb9a23/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "docs/research/agent-task-catalog.json", + "research/complex-local-word-ceiling/RESULT.json", + "research/complex-local-word-ceiling/ceiling.py" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Exact source pins; symbolic forward and inverse identities for multiple q,s; exhaustive arbitrary-dirty state replay over F2 and F3; both missing-wave and wrong-sign controls; complete multiplication-child and row-add formulas; certified hypothetical profile ceiling and five-percent screen." + } + ] +} diff --git a/research/recursive-multiterm-anchor-seedb9a23/verify.py b/research/recursive-multiterm-anchor-seedb9a23/verify.py new file mode 100644 index 0000000000..bda1f79705 --- /dev/null +++ b/research/recursive-multiterm-anchor-seedb9a23/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Verify dirty-anchor accumulation of a sum of shared bilinear products.""" +from __future__ import annotations + +import hashlib +import itertools +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(ROOT / "research/complex-local-word-ceiling")) +import ceiling as C # noqa: E402 + +PINNED_FILES = { + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b", + "docs/research/agent-task-catalog.json": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "research/complex-local-word-ceiling/RESULT.json": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d", + "research/complex-local-word-ceiling/ceiling.py": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc", +} +BASE_PROFILE = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} +BASE_CEILING = (Q(52814190909, 31250000000000), Q(1690054109089, 10**15)) +ILLUSTRATIVE_PROFILE = {1: 2364, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} +ILLUSTRATIVE_CEILING = ( + Q(68214620471, 40000000000000), + Q(53292672243, 31250000000000), +) + + +def require(ok: bool, why: str) -> None: + if not ok: + raise RuntimeError(why) + + +def add_scaled(dst: dict[tuple[str, ...], int], src: dict[tuple[str, ...], int], scale: int): + out = dict(dst) + for monomial, coefficient in src.items(): + out[monomial] = out.get(monomial, 0) + scale * coefficient + return {m: c for m, c in out.items() if c} + + +def product_poly(x: str, y: str) -> dict[tuple[str, ...], int]: + return {tuple(sorted((x, y))): 1} + + +def forward_symbolic(q: int, common: list[tuple[str, str]], private: list[tuple[str, str]], *, + before: bool = True, after: bool = True, first_scale: int = -1): + out = [{(f"A{i}",): 1} for i in range(q)] + if before: + for i in range(1, q): + out[i] = add_scaled(out[i], out[0], first_scale) + for x, y in common: + out[0] = add_scaled(out[0], product_poly(x, y), 1) + if after: + for i in range(1, q): + out[i] = add_scaled(out[i], out[0], 1) + for i, (x, y) in enumerate(private): + out[i] = add_scaled(out[i], product_poly(x, y), 1) + return out + + +def inverse_symbolic(out, common, private): + q = len(out) + state = [dict(poly) for poly in out] + for i in range(q - 1, -1, -1): + state[i] = add_scaled(state[i], product_poly(*private[i]), -1) + for i in range(q - 1, 0, -1): + state[i] = add_scaled(state[i], state[0], -1) + for x, y in reversed(common): + state[0] = add_scaled(state[0], product_poly(x, y), -1) + for i in range(1, q): + state[i] = add_scaled(state[i], state[0], 1) + return state + + +def check_symbolic_family() -> None: + for q in range(2, 6): + for s in range(1, 5): + common = [(f"x{j}", f"y{j}") for j in range(s)] + private = [(f"u{i}", f"v{i}") for i in range(q)] + result = forward_symbolic(q, common, private) + for i in range(q): + expected = {(f"A{i}",): 1} + for x, y in common: + expected = add_scaled(expected, product_poly(x, y), 1) + expected = add_scaled(expected, product_poly(*private[i]), 1) + require(result[i] == expected, f"symbolic output identity q={q} s={s} i={i}") + require(inverse_symbolic(result, common, private) == [{(f"A{i}",): 1} for i in range(q)], + f"symbolic inverse q={q} s={s}") + + +def forward_values(a, x, y, u, v, p, *, before=True, after=True, first_sign=-1): + q, s = len(a), len(x) + out = list(a) + if before: + for i in range(1, q): + out[i] = (out[i] + first_sign * out[0]) % p + for j in range(s): + out[0] = (out[0] + x[j] * y[j]) % p + if after: + for i in range(1, q): + out[i] = (out[i] + out[0]) % p + for i in range(q): + out[i] = (out[i] + u[i] * v[i]) % p + return out + + +def inverse_values(out, x, y, u, v, p): + q, s = len(out), len(x) + state = list(out) + for i in range(q - 1, -1, -1): + state[i] = (state[i] - u[i] * v[i]) % p + for i in range(q - 1, 0, -1): + state[i] = (state[i] - state[0]) % p + for j in range(s - 1, -1, -1): + state[0] = (state[0] - x[j] * y[j]) % p + for i in range(1, q): + state[i] = (state[i] + state[0]) % p + return state + + +def check_exhaustive_dirty_states() -> int: + q, s = 2, 2 + total = 0 + for p in (2, 3): + for values in itertools.product(range(p), repeat=3 * q + 2 * s): + pos = 0 + a = values[pos:pos + q]; pos += q + x = values[pos:pos + s]; pos += s + y = values[pos:pos + s]; pos += s + u = values[pos:pos + q]; pos += q + v = values[pos:pos + q] + original_sources = (x, y, u, v) + got = forward_values(a, x, y, u, v, p) + common_sum = sum(x[j] * y[j] for j in range(s)) % p + expected = tuple((a[i] + common_sum + u[i] * v[i]) % p for i in range(q)) + require(tuple(got) == expected, f"dirty forward replay p={p} state={values}") + require(tuple(inverse_values(got, x, y, u, v, p)) == tuple(a), + f"dirty inverse replay p={p} state={values}") + require((x, y, u, v) == original_sources, "source values are read-only") + total += 1 + return total + + +def check_failure_controls() -> None: + # The first wave removes the old dirty anchor; the second installs its update. + a, x, y, u, v = (1, 0), (0, 0), (0, 0), (0, 0), (0, 0) + expected = (1, 0) + require(tuple(forward_values(a, x, y, u, v, 3, before=False)) != expected, + "missing-old-anchor-wave negative control") + a, x, y, u, v = (0, 0), (1, 0), (1, 0), (0, 0), (0, 0) + require(tuple(forward_values(a, x, y, u, v, 3, after=False)) != (1, 1), + "missing-updated-anchor-wave negative control") + a, x, y, u, v = (1, 0), (0, 0), (0, 0), (0, 0), (0, 0) + require(tuple(forward_values(a, x, y, u, v, 3, first_sign=1)) != (1, 0), + "wrong compensation sign negative control") + + +def check_cost_formula() -> None: + for q in range(2, 9): + for s in range(1, 6): + direct_children = q * (s + 1) + shared_children = s + q + require(direct_children - shared_children == s * (q - 1), "child-call saving formula") + combined_adds = 2 * (q - 1) + separate_adds = 2 * s * (q - 1) + require(separate_adds - combined_adds == 2 * (s - 1) * (q - 1), + "coalesced fanout addition saving") + + +def check_selected_profile_screen() -> None: + base = C.ceiling(BASE_PROFILE, 73, 896, 9, 64, grid=Q(1, 10**15)) + candidate = C.ceiling(ILLUSTRATIVE_PROFILE, 73, 896, 9, 64, grid=Q(1, 10**15)) + require(base == BASE_CEILING, "selected profile ceiling pin") + require(candidate == ILLUSTRATIVE_CEILING, "eight-block rank-only candidate ceiling") + require(candidate[1] < BASE_CEILING[1] * Q(105, 100), "hypothetical profile still misses five-percent gate") + + +def check_pins() -> None: + for relative, expected in PINNED_FILES.items(): + actual = hashlib.sha256((ROOT / relative).read_bytes()).hexdigest() + require(actual == expected, f"source SHA-256 pin: {relative}") + + +def check_result_record(exhaustive_count: int) -> None: + result = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + require(result["exhaustive_dirty_states"] == exhaustive_count == 60073, "RESULT exhaustive count") + require(result["illustrative_profile"] == {str(k): v for k, v in ILLUSTRATIVE_PROFILE.items()}, + "RESULT profile") + require(result["illustrative_ceiling"] == [str(x) for x in ILLUSTRATIVE_CEILING], "RESULT ceiling") + require(result["cost_example"] == { + "q": 3, + "s": 3, + "width": 1, + "direct_children": 12, + "anchor_children": 6, + "anchor_adds": 4, + "separate_fanout_adds": 12, + "children_saved": 6, + "fanout_adds_saved": 8, + "net_saving": "6*mu-4*A_1", + "break_even": "mu > 2*A_1/3", + }, "RESULT cost example") + + +def main() -> None: + check_pins() + check_symbolic_family() + exhaustive = check_exhaustive_dirty_states() + check_failure_controls() + check_cost_formula() + check_selected_profile_screen() + check_result_record(exhaustive) + gain = 100 * (ILLUSTRATIVE_CEILING[1] / BASE_CEILING[1] - 1) + print( + "PASS_RECURSIVE_MULTITERM_DIRTY_ANCHOR " + f"symbolic_q=2..5 symbolic_s=1..4 exhaustive_states={exhaustive} " + f"q3_s3_direct=12_shared=6_adds=4 separate_fanout_adds=12 " + f"eight_block_rank_only_gain_percent={float(gain):.6f} " + "supplier_admission=none negative_controls=3" + ) + + +if __name__ == "__main__": + main()