diff --git a/research/complex-rank2-retiming-seed73506/README.md b/research/complex-rank2-retiming-seed73506/README.md new file mode 100644 index 0000000000..563364cec2 --- /dev/null +++ b/research/complex-rank2-retiming-seed73506/README.md @@ -0,0 +1,60 @@ +# One-touch rank-2 retiming cannot meet the 5% ceiling gate + +**Scoped negative result; no construction and no new κ.** On the selected PR1094 gauge44 local program, the complete class of same-column rank-1 climb pairs with exactly one intervening scalar event has 690 candidates in each direction. The maximum set that can be fused without reusing a climb has **674 pairs**. Even if every one becomes a rank-2 child at zero additional operation, copy, frame, hosting, precision, interface, or restoration cost, the exact selected-word ceiling rises only **4.6659458%**, below the predeclared 5% target. + +## Exact object and result + +The source is `research/community-frontier1094-audit/selected-replay.tar.gz`, SHA-256 `f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6`. The program member is `candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz`, SHA-256 `241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a`. The verifier extracts and checks these bytes; it does not modify the frozen source. + +For each direction, climbs are grouped by column in program order. A candidate is a consecutive `(rank 1, rank 1)` pair with exactly one intervening event that references the column; all 690 such intervening events are scalar operations. Forward and backward candidate sets agree. On each column, the climb events form a path and candidate fusions are edges between adjacent rank-1 vertices. A greedy path matching and a separate dynamic-programming recurrence both give the maximum compatible set: **674**. + +The selected local profile is `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` at width `m=73`, 896 families, 9 stages, and centre charge 64. For `n` disjoint fusions, the optimistic profile is + +```text +{1: 2412 - 2n, 2: 418 + n, 3: 432, 4: 142, 5: 82, 8: 8} +``` + +It preserves all 5,586 local rank units and the incumbent 1,646 idle units, which the relaxation fills at rank 51 under the halving guard. The exact interval engine in `research/complex-local-word-ceiling/ceiling.py` gives: + +| Case | Certified ceiling bracket for `a` | +|---|---:| +| Selected profile | `[0.001690054109088, 0.001690054109089]` | +| All 674 one-touch fusions, with zero added cost | `[0.001768911117731, 0.001768911117732]` | +| Required target, 5% above the selected upper endpoint | `0.00177455681454345` | + +At that target, the exact relaxation for 674 fusions is already greater than 1. The least number of zero-overhead rank-2 fusions that passes is **720**: 719 fails and 720 passes. Thus this one-touch candidate family misses the gate by at least 46 fusions even before any physical implementation bill is added. + +## Cost boundary + +Every incumbent source, helper, recursive-child, centre, and coverage charge remains in the selected profile. The screen grants the proposed scalar/frame retiming, copies, hosting, precision, interface transitions, and dirty-state restoration for free. This is deliberately favorable. Any additional paid child rank would consume rank-51 idle mass and lower the ceiling; all other implementation costs are waived here, so a real construction would still have to account for their effect. The screen rules out reaching the 5% target **through this complete one-touch fusion family under the unchanged coverage law**. + +It does not prove that any pair can actually be retimed. It does not rule out pairs with two or more intervening operations, a different block rank, a changed word or coverage law, or another helper inventory. It is not a universal lower bound on complex decoders and supplies no physical supplier or κ. + +## Relation to prior work + +Arham Tahir's [PR1605](https://github.com/CrocSwap/integer-mult-bounds/pull/1605) gives the rank-2 cost threshold but no physical realization. Josie Elliston's [finding in Discussion 1596](https://github.com/CrocSwap/integer-mult-bounds/discussions/1596#discussioncomment-18915212) gives the 5% κ threshold for unrestricted rank-1 pair fusion and leaves its frame/dirty-state contract open. Navinor's [source event count in Discussion 1659](https://github.com/CrocSwap/integer-mult-bounds/discussions/1659#discussioncomment-18916048) identifies the one-touch candidates syntactically without frame or dirty-state semantics. This package intersects that exact chronological class with the exact disjoint-pair budget and stops before an unpromising physical synthesis. + +The active [frame-reassignment claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1659) fixes the paid profile. The active [nested-endpoint claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1674) fixes scalar order. This screen changes both local schedule and paid rank profile, but makes no claim about their results. The current selected record is `836330098538459/500000000000000000`; its review is `docs/research/community-batch1099-review.md`, source manifest is `research/community-frontier1094-audit/SELECTED-SOURCE.json`, certificate is `research/community-frontier1094-audit/ASSEMBLY.json` (SHA-256 `1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045`), and selected replay instruction is `make frontier1094-verify`. This package does not rerun or alter that replay. + +## Reproduce + +From the repository root: + +```sh +python3.12 scripts/research_package.py --package research/complex-rank2-retiming-seed73506 --check-only +python3.12 scripts/research_package.py --package research/complex-rank2-retiming-seed73506 +``` + +The package verifier rechecks archive/member pins, both event directions, the 674-edge maximum matching by two algorithms, the selected baseline ceiling, the optimistic profile, and the exact 719/720 target boundary. Expected marker: + +```text +PASS_ONE_TOUCH_RANK2_RETIMING_SCREEN candidates=690 matched=674 a_gain_pct<4.666 target_min=720 +``` + +## Open next questions + +- **Can a larger chronological class reach 720 disjoint fusions?** This matters because the one-touch class is too small even under the free-retiming relaxation. A feasible first step is to enumerate pairs with two intervening scalar operations and test whether a common rank-2 frame can preserve their exact map. The blocker is a transformation that carries both dirty-state dependencies through those operations without adding a paid rank-1 child. + +## Credit + +Retain the selected PR1094 lineage credited in the selected review; Douglas Colkitt/PR1240 and Sagar Thakrar/PR1012 for the ceiling model; Arham Tahir/PR1605 for integer block budgets; Josie Elliston/Discussion 1596 for rank-2 fusion thresholds; and Navinor/Discussion 1659 for the source-bound event classification. The exact ceiling engine is reused and pinned; the event parsing and matching certificate are new. Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/complex-rank2-retiming-seed73506/SOURCES.json b/research/complex-rank2-retiming-seed73506/SOURCES.json new file mode 100644 index 0000000000..d15b84460c --- /dev/null +++ b/research/complex-rank2-retiming-seed73506/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-local-word-ceiling/README.md", + "usage": "input", + "git_blob": "f5f742f8196da29d2c3f4dffb3c27685ca9401f6", + "sha256": "b60be039cb0e03e064a27407d0bce9e58908d793da5ee405c876de5aebfa5f81" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ] +} diff --git a/research/complex-rank2-retiming-seed73506/TASK.json b/research/complex-rank2-retiming-seed73506/TASK.json new file mode 100644 index 0000000000..401ff8f6a9 --- /dev/null +++ b/research/complex-rank2-retiming-seed73506/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "On the selected PR1094 local program, screen the complete bounded family of disjoint fusions of consecutive same-column rank-1 climb pairs with exactly one intervening scalar event, allowing that scalar/frame schedule to change.", + "scope_change_reason": "The generic decoder card is refined to a concrete retiming family in the pinned selected word. Unlike the active fixed-schedule frame and endpoint claims, this changes the local scalar schedule and paid rank profile. The complete zero-overhead profile is screened before any physical synthesis.", + "bottleneck_link": "Rank-1 children account for 2,412 of the selected 5,586 local rank units. Combining two rank-1 children into one rank-2 child reduces the recursive moment per paid rank unit; the exact selected-word ceiling tests whether this bounded retiming family can clear the revision-3 5% mechanism gate.", + "budget_minutes": 60, + "stop_rule": "Enumerate the source-pinned one-touch pairs in both directions, compute the exact maximum disjoint matching, and screen that complete profile at zero additional cost. Stop if the exact ceiling is below 1.05 times the selected ceiling upper endpoint.", + "outcome": "negative-result", + "evidence": "Both directions contain 690 one-touch pairs and have identical candidate sets. A greedy matching and a separate path dynamic program agree that at most 674 can be used disjointly. The zero-extra-cost profile has exact ceiling bracket [0.001768911117731, 0.001768911117732], below the 5% target 0.00177455681454345; the least zero-overhead fusion count that passes is 720. The source-pinned verifier checks the archive and member hashes, source event data, baseline, matching, profile, ceiling intervals and adjacent 719/720 controls.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance for literature/overlap search, scope selection, exact matching analysis, implementation and packaging.", + "track": "complex-mechanisms", + "seed": "73506a45fb5f7d14ab78b42d26e1c4e8", + "scope_key": "02b31ebd160542c86299", + "catalogue_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1693", + "claim_finding_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1693#discussioncomment-18918212", + "claim_expiry": "2026-10-14T09:12:00Z", + "open_questions": [ + { + "question": "Can pairs with two or more intervening scalar operations supply at least 720 disjoint rank-2 fusions without adding an expensive child?", + "why_it_matters": "The complete one-touch class cannot meet the 5% target, while another exact chronological class large enough to pass may still admit a useful retiming mechanism.", + "first_step": "Enumerate consecutive same-column rank-1 pairs with exactly two intervening scalar events in both directions, intersect their identifiers, compute the maximum disjoint set, and screen the zero-overhead profile before synthesis.", + "blocked_by": "A physical construction must preserve both scalar dependencies, arbitrary dirty state, helper endpoints and restoration while fully charging any added frame or copy work." + } + ] +} diff --git a/research/complex-rank2-retiming-seed73506/TASK.md b/research/complex-rank2-retiming-seed73506/TASK.md new file mode 100644 index 0000000000..961c5c2cea --- /dev/null +++ b/research/complex-rank2-retiming-seed73506/TASK.md @@ -0,0 +1,18 @@ +# Task card: one-touch rank-2 retiming screen + +- **Task ID / scope key / track / seed:** `complex-rank-shape-decoder` / `02b31ebd160542c86299` / `complex-mechanisms` / `73506a45fb5f7d14ab78b42d26e1c4e8`. +- **Scope key:** refined from the catalogue card to selected-word chronological rank-1 pair fusions; scope status `changed` because the experiment permits a local scalar retiming and changes the paid rank profile. +- **Base commit:** `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. +- **Priority revision / catalogue hash:** revision 3 / `6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075`. +- **Selected-record SHA-256:** `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`; selected value `836330098538459/500000000000000000`. +- **Object and question:** In the source-pinned PR1094 gauge44 program, can two rank-1 climbs on one column, separated by exactly one scalar event that reads that column, be retimed into one rank-2 child while preserving the local operator and arbitrary dirty-state restoration? The bounded candidate set has 690 pairs in each of the forward and backward programs. Only mutually disjoint pairs may be fused. +- **Changed hypothesis:** Permit a local scalar/frame rewrite around a pair of climbs. The word, scalar alphabet, inputs, outputs, other helper endpoints, and selected global coverage contract stay fixed. This differs from PR1671/Discussion 1659 (all frame changes with the paid histogram fixed) and Discussion 1674 (nested endpoint/frame changes with scalar order fixed). +- **Method and domain:** Pin `research/community-frontier1094-audit/selected-replay.tar.gz` (SHA-256 `f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6`) and its member `candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz` (SHA-256 `241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a`). Enumerate only consecutive same-column `(1,1)` climb pairs with one intervening event naming that column; compute a maximum disjoint set and apply the exact `ceiling()` model to the resulting profile. +- **Nearest work:** Arham Tahir, PR1605 head `488f2ecf1835c6d813e96543656dddf0062fdc9a`, gives the integer block-rank cost thresholds but no physical block realization. Josie Elliston's finding in Discussion 1596 gives the rank-2 fusion thresholds but says no frame/dirty-state contract is shown. Navinor's source-bound count in Discussion 1659 comment `18916048` identifies the 690 one-touch pairs syntactically, with no frame or dirty-state semantics. PR1671 head `ce130d291f5ab6dd801544886a16f62d42d86118` fixes the paid rank profile; Discussion 1674 explicitly fixes scalar order and excludes rank reblocking. The present scope changes the scalar schedule and the rank profile, and will test a physical local rewrite only if its favorable cost has headroom. +- **Optimistic full budget:** Baseline local profile `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}`, width 73, 896 families, 9 stages, centre charge 64, and idle-rank cap 51. A fusion replaces two rank-1 children by one rank-2 child, preserving local rank mass. Grant all retiming, frame, copied-information, hosting, precision, interface, and restoration work for free for the initial upper-bound screen; all unchanged source/child/centre/coverage charges remain in the incumbent profile. Any construction must later charge every added operation and boundary transition. Require a certified ceiling at least 5% above the selected-word ceiling; otherwise stop this candidate family. +- **Preliminary overlap:** `find_overlap.py` was refreshed for the task and exact retiming phrases. It fetched all 333 discussions, but its PR refresh failed because the installed `gh api` lacks `--slurp`; open PRs including drafts were checked separately with `gh pr list` and targeted body searches. No active claim found for the scalar-retiming/rank-profile change. Claims #1671/#1674 and the completed #1605/#1596/#1659 boundaries are listed above. +- **Success / falsification:** Success requires a local exact identity with all sources, helpers and dirty contents restored, both directions checked, every extra frame/copy/child/hosting/precision/interface cost charged, and a complete per-call profile. Falsification is an exact optimistic profile below the predeclared 5% threshold for the maximum disjoint candidate set, or an exact counterexample to the proposed local retiming. +- **Stopping rule:** Screen the complete bounded candidate set once. If its zero-extra-cost completed profile cannot reach the target, stop this mechanism. Otherwise test the smallest source-pinned candidate class first; no unbounded synthesis. Reserve the final quarter of the cycle for verification and handoff. +- **Intended artifact:** A registered research package only if it contains a new exact construction or a useful scoped obstruction. Otherwise retain a short evidence-based local handoff. No new κ or selected-result change is presumed. +- **Attribution / disclosure:** Preserve the selected PR1094 lineage and credits to Douglas Colkitt/PR1240, Sagar Thakrar/PR1012, Arham Tahir/PR1605, Josie Elliston/Discussion 1596, and Navinor/Discussion 1659. Disclose substantial OpenAI Codex assistance. +- **Claim expiry:** 2026-10-14 09:12 UTC. diff --git a/research/complex-rank2-retiming-seed73506/VERIFY.json b/research/complex-rank2-retiming-seed73506/VERIFY.json new file mode 100644 index 0000000000..626e357566 --- /dev/null +++ b/research/complex-rank2-retiming-seed73506/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/community-batch1099-review.md", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-local-word-ceiling/README.md", + "research/complex-local-word-ceiling/ceiling.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pin selected result and compressed source archive/member; enumerate forward/backward one-touch pairs; verify maximum disjoint matching by greedy and dynamic programming; check baseline and optimistic exact ceiling intervals, the 5% target, and the adjacent 719/720 fusion controls." + } + ] +} diff --git a/research/complex-rank2-retiming-seed73506/verify.py b/research/complex-rank2-retiming-seed73506/verify.py new file mode 100644 index 0000000000..5b7facd4d2 --- /dev/null +++ b/research/complex-rank2-retiming-seed73506/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Exact bounded screen for one-touch rank-1 pair retiming.""" + +from __future__ import annotations + +import bisect +import collections +import gzip +import hashlib +import importlib.util +import io +import json +import tarfile +from fractions import Fraction as Q +from pathlib import Path +import sys + + +ROOT = Path(__file__).resolve().parents[2] +ARCHIVE = ROOT / "research/community-frontier1094-audit/selected-replay.tar.gz" +MEMBER = "candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz" +ARCHIVE_SHA256 = "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" +MEMBER_SHA256 = "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a" +SELECTED_SHA256 = "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" +CEILING_SHA256 = "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" +BASE_PROFILE = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} +M, FAMILIES, STAGES, CENTRE = 73, 896, 9, 64 +GRID = Q(1, 10**15) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def sha256(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def decode_program(compressed: bytes, expected_sha256: str) -> dict: + require(sha256(compressed) == expected_sha256, "LOCAL-PROGRAMS member hash mismatch") + return json.loads(gzip.decompress(compressed)) + + +def source_program() -> dict: + archive_bytes = ARCHIVE.read_bytes() + require(sha256(archive_bytes) == ARCHIVE_SHA256, "selected replay archive hash mismatch") + with tarfile.open(fileobj=io.BytesIO(archive_bytes), mode="r:gz") as archive: + member = archive.extractfile(MEMBER) + require(member is not None, "pinned local program is absent from archive") + compressed = member.read() + return decode_program(compressed, MEMBER_SHA256) + + +def load_ceiling(): + path = ROOT / "research/complex-local-word-ceiling/ceiling.py" + raw = path.read_bytes() + require(sha256(raw) == CEILING_SHA256, "pinned ceiling engine hash mismatch") + spec = importlib.util.spec_from_file_location("pinned_complex_ceiling", path) + require(spec is not None and spec.loader is not None, "cannot import pinned ceiling engine") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def candidate_edges(events: list) -> tuple[set[tuple[int, int]], dict[int, int]]: + """Return (column, climb-position) edges for one-touch (1,1) climb pairs.""" + climbs: dict[int, list[tuple[int, int]]] = collections.defaultdict(list) + touches: dict[int, list[tuple[int, str]]] = collections.defaultdict(list) + for index, event in enumerate(events): + require(isinstance(event, list) and event, "malformed local-program event") + tag = event[0] + if tag == "climb": + require(len(event) >= 6, "malformed climb event") + climbs[int(event[2])].append((index, int(event[5]))) + elif tag == "scalar": + require(len(event) >= 2 and isinstance(event[1], list), "malformed scalar event") + refs = set() + for operand in event[1][1:]: + if isinstance(operand, list) and len(operand) >= 2 and operand[0] == "L": + refs.add(int(operand[1])) + for column in refs: + touches[column].append((index, tag)) + elif tag in ("adapter", "residual_adapter"): + require(len(event) >= 3, "malformed adapter event") + touches[int(event[2])].append((index, tag)) + + edges: set[tuple[int, int]] = set() + sizes = {column: len(sequence) for column, sequence in climbs.items()} + for column, sequence in climbs.items(): + column_touches = touches.get(column, []) + positions = [index for index, _ in column_touches] + for position, ((left, rank_left), (right, rank_right)) in enumerate( + zip(sequence, sequence[1:]) + ): + if rank_left != 1 or rank_right != 1: + continue + first = bisect.bisect_right(positions, left) + last = bisect.bisect_left(positions, right) + between = column_touches[first:last] + if len(between) == 1 and between[0][1] == "scalar": + edges.add((column, position)) + return edges, sizes + + +def greedy_matching(edges: set[tuple[int, int]], sizes: dict[int, int]) -> set[tuple[int, int]]: + chosen = set() + for column in sorted(sizes): + last_used_vertex = -1 + for position in sorted(p for c, p in edges if c == column): + if position > last_used_vertex: + chosen.add((column, position)) + last_used_vertex = position + 1 + return chosen + + +def dynamic_matching_size(edges: set[tuple[int, int]], sizes: dict[int, int]) -> int: + total = 0 + for column, nodes in sizes.items(): + edge_positions = {p for c, p in edges if c == column} + dp = [0] * (nodes + 1) + for prefix in range(1, nodes + 1): + dp[prefix] = dp[prefix - 1] + position = prefix - 2 + if position >= 0 and position in edge_positions: + dp[prefix] = max(dp[prefix], dp[prefix - 2] + 1) + total += dp[nodes] + return total + + +def profile_after_fusions(count: int) -> dict[int, int]: + require(0 <= count <= sum(BASE_PROFILE.values()) // 2, "invalid fusion count") + profile = dict(BASE_PROFILE) + profile[1] -= 2 * count + profile[2] += count + return {rank: n for rank, n in profile.items() if n} + + +def main() -> None: + selected_bytes = (ROOT / "certificates/selected-result.json").read_bytes() + require(sha256(selected_bytes) == SELECTED_SHA256, "selected-record hash mismatch") + selected = json.loads(selected_bytes) + require(selected.get("kappa") == "836330098538459/500000000000000000", + "selected result value changed") + + program = source_program() + forward_edges, forward_sizes = candidate_edges(program["forward"]) + backward_edges, backward_sizes = candidate_edges(program["backward"]) + require(len(forward_edges) == 690, "forward one-touch candidate count changed") + require(len(backward_edges) == 690, "backward one-touch candidate count changed") + require(forward_edges == backward_edges, "forward/backward candidate sets differ") + require(forward_sizes == backward_sizes, "forward/backward climb-path sizes differ") + + chosen = greedy_matching(forward_edges, forward_sizes) + greedy_count = len(chosen) + dp_count = dynamic_matching_size(forward_edges, forward_sizes) + require(greedy_count == dp_count == 674, "maximum disjoint fusion count changed") + + # A path with consecutive eligible edges must not count an overlapping climb twice. + synthetic_edges = {(7, 0), (7, 1), (7, 2)} + synthetic_sizes = {7: 4} + require(len(greedy_matching(synthetic_edges, synthetic_sizes)) == 2, + "synthetic greedy matching control failed") + require(dynamic_matching_size(synthetic_edges, synthetic_sizes) == 2, + "synthetic DP matching control failed") + + # The source pin must reject changed compressed bytes before parsing them. + try: + decode_program(b"changed", MEMBER_SHA256) + except ValueError: + pass + else: + raise ValueError("source corruption control was accepted") + + ceiling = load_ceiling() + base_lo, base_hi = ceiling.ceiling(BASE_PROFILE, M, FAMILIES, STAGES, CENTRE, grid=GRID) + require(base_lo == Q(52814190909, 31250000000000), "baseline lower ceiling endpoint changed") + require(base_hi == Q(1690054109089, 10**15), "baseline upper ceiling endpoint changed") + + profile = profile_after_fusions(greedy_count) + require(profile == {1: 1064, 2: 1092, 3: 432, 4: 142, 5: 82, 8: 8}, + "optimistic fused profile changed") + require(sum(rank * count for rank, count in profile.items()) == 5586, + "fusion profile must preserve local rank mass") + model = ceiling.model(BASE_PROFILE, M, FAMILIES, STAGES, CENTRE) + require(model["idle_mass"] == 1646, "incumbent idle mass changed") + require(model["R"] == 51, "incumbent idle rank cap changed") + + fused_lo, fused_hi = ceiling.ceiling(profile, M, FAMILIES, STAGES, CENTRE, grid=GRID) + require(fused_lo == Q(1768911117731, 10**15), "optimistic lower ceiling endpoint changed") + require(fused_hi == Q(442227779433, 250_000_000_000_000), + "optimistic upper ceiling endpoint changed") + target = base_hi * Q(21, 20) + require(target == Q(35491136290869, 20_000_000_000_000_000), "5% target changed") + target_value = ceiling.relax(profile, M, FAMILIES, STAGES, CENTRE, target) + require(target_value[0] > 1, "674 fusions unexpectedly meet the 5% target") + require(fused_hi < target, "fused ceiling unexpectedly meets the 5% target") + + # Find the exact zero-overhead fusion threshold and check both adjacent cases. + def passes(count: int) -> bool: + return ceiling.relax(profile_after_fusions(count), M, FAMILIES, STAGES, CENTRE, target)[1] < 1 + + low, high = 0, sum(BASE_PROFILE.values()) // 2 + while low < high: + middle = (low + high) // 2 + if passes(middle): + high = middle + else: + low = middle + 1 + require(low == 720, "zero-overhead threshold changed") + require(ceiling.relax(profile_after_fusions(719), M, FAMILIES, STAGES, CENTRE, target)[0] > 1, + "719-fusion failure control did not fail") + require(passes(720), "720-fusion positive boundary control did not pass") + + gain_upper = fused_hi / base_lo - 1 + require(gain_upper < Q(46660, 1_000_000), "reported 4.6660% upper gain is not certified") + print( + "PASS_ONE_TOUCH_RANK2_RETIMING_SCREEN " + f"candidates={len(forward_edges)} matched={greedy_count} " + f"a_gain_pct<{float(gain_upper * 100):.6f} target_min={low}" + ) + + +if __name__ == "__main__": + main()