From b94bd17d3507f6223bd008e94c6877a6b14fce44 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 01:33:26 +0000 Subject: [PATCH 1/2] Audit #2979 group V45 against its losing single-helper controls. Independently recompute the shared rank-7 end frame on both PR2942 parents. Every proper subset loses under the published frame surrogate; all four helpers gain 22972 units, with cleanup and buffer count unchanged. No new kappa. Co-authored-by: unpaidmoon --- research/rank7-v45-group-audit/README.md | 113 +++++++ research/rank7-v45-group-audit/SOURCES.json | 36 +++ research/rank7-v45-group-audit/TASK.json | 72 +++++ research/rank7-v45-group-audit/VERIFY.json | 22 ++ research/rank7-v45-group-audit/verify.py | 337 ++++++++++++++++++++ 5 files changed, 580 insertions(+) create mode 100644 research/rank7-v45-group-audit/README.md create mode 100644 research/rank7-v45-group-audit/SOURCES.json create mode 100644 research/rank7-v45-group-audit/TASK.json create mode 100644 research/rank7-v45-group-audit/VERIFY.json create mode 100644 research/rank7-v45-group-audit/verify.py diff --git a/research/rank7-v45-group-audit/README.md b/research/rank7-v45-group-audit/README.md new file mode 100644 index 0000000000..4a106ed794 --- /dev/null +++ b/research/rank7-v45-group-audit/README.md @@ -0,0 +1,113 @@ +# Independent audit of #2979 group V45 + +**Partial frame-surrogate certificate. No new κ.** Selected κ stays +`0.001672660197076918`. PR #2979's conditional κ ≈ 0.001729 is not selected +and is not re-certified here. + +On both PR #2942 parent words, the four restored helpers 249, 251, 265 and 267 +share one rank-7 end frame + +```text +W = ⟨256, 128, 64, 35, 16, 11, 5⟩ = E_7 ∩ E_42 = E_7 ∩ E_42 ∩ E_45 +``` + +because `7 ⊕ 42 = 45`. Lowering any proper subset of those four end frames, after +the 61 gate frames that land only in `W`, loses money under #2979's published +integer frame weights. Lowering all four gains **22,972** surrogate units. +The shared gate-frame overhead is **78,512** units, and each added helper then +saves exactly one rank-1 climb, `c_1 = 2,116,671`. + +## What was checked + +The parents are `research/rank7-joint-endframes/data/PARENT-base.json.gz` and +`PARENT-extra.json.gz`, with the stage-1 record +`STAGE1-FRAME-EDITS.json`. Group V45 owns the 61 edits whose new frame is +contained in `W` and in no other declared group frame (20 in `B`, 41 in +`restore`). No `A` gate moves. Scalars, operators and the cleanup list are +unchanged, and the private-buffer count stays 86. + +The paid profile is recomputed by a separate transcription of the inherited +climb rules (monotone subspace climbs, warp resets, centre and target cuts, +final climb to the live end frame). It is not imported from +`rank7-joint-endframes/producer.py` or from `STAGE-PRICES.json`. Calibration: +both stored parent profiles and width inventories are reproduced before any +edit. Weights are the published surrogate + +```text +c = (2116671, 4228346, 6338140, 8446713, 10554378, 12661320, 14767661, 16873488, 18978865) +``` + +at the recorded base saving, and the break-even charge for one freed width is +`c_1 - 25371 = 2091300`. This package does not re-derive `c_r` from the moment +engines. + +For a subset of `k` helpers, with those end frames set to `W` and all 61 gate +frames applied, the margin is `-Δ - k·2091300`. Both providers give the same +margins: + +| k | subsets | margin | +|---:|---:|---:| +| 0 | 1 | −78,512 | +| 1 | 4 | −53,141 | +| 2 | 6 | −27,770 | +| 3 | 4 | −2,399 | +| 4 | 1 | **+22,972** | + +The `k = 4` profile delta is `−8,388,172`, and the width inventory moves four +units from width 8 to width 7. The identity + +```text +4·25371 − 78512 = 22972 +``` + +is the whole joint margin: partner frames are paid once, and each helper +returns `c_1` against a break-even of `c_1 - 25371`. Every one-helper control +loses. Omitting the first helper-touching edit, or putting that gate's old +frame back, makes the word nonmonotone. + +## What this does not establish + +Groups A–D, the five paired extractions, the fourteen rewrites, the T74 +allocation, idle packing, native admission and both supplier caps are +unchecked. A positive local margin in this surrogate is not a multiplication +exponent. `research/rank7-joint-endframes-restore-edit` starts from the #2979 +words and does not replace this group check. PR #3585 records archive blobs +only. + +## Reproduce + +Python 3.12, standard library, from the repository root: + +```sh +python3 -B research/rank7-v45-group-audit/verify.py +python3 -B scripts/research_package.py --package research/rank7-v45-group-audit +``` + +Expected first line: + +```text +PASS_RANK7_V45_GROUP_AUDIT providers=2 edits=61 sections=20+41 joint_delta=-8388172 joint_margin=22972 single_margin=-53141 pair_margin=-27770 triple_margin=-2399 frame_only_margin=-78512 overhead=78512 width_8_to_7=4 buffers=86 cleanup_unchanged=yes controls=omit-edit,stale-frame +``` + +The direct verifier finished in about 6 seconds on the recorded host. + +## Open next questions + +1. Isolate groups A, B, C and D by the same containment rule and test whether + each added helper saves exactly `c_1` after one shared overhead. That is the + same finite check; it was not run here. +2. Enclose `c_r` independently at `b = 0.001703676387993676` and price this + profile delta through the idle-width cap. Until that is done, the unit + margin does not move κ. The frame-domain-ceiling engines are the blocker. + +## Credit + +Marius-Paul Dumitrean (Dugongue / mdumitrean), PR #2979, for the words, the +V45 claim and the published weights under audit. The parent words descend from +Mason Hale's PR #2917 and the PR #2942 extractions; frame climb rules are +Jeremy Kothe's, from the PR #2894 lineage. Jeremy Diviney's paired-extraction +method and Dugongue's PR #2969 comparator sit behind that claim and are not +rechecked here. Archive disposition PR #3585 is separate. + +Prepared by unpaidmoon with substantial AI assistance (Cursor Grok). No +independent human or formal-kernel review is claimed. Apache-2.0. diff --git a/research/rank7-v45-group-audit/SOURCES.json b/research/rank7-v45-group-audit/SOURCES.json new file mode 100644 index 0000000000..5bcffb01ee --- /dev/null +++ b/research/rank7-v45-group-audit/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/rank7-joint-endframes/data/PARENT-base.json.gz", + "usage": "input", + "git_blob": "1ca8287d6ae5eb45d87db65b369be8d09ba692b2", + "sha256": "54ca34c749e3228d7e2df3d8dbf7aa1568c2872490166997c5962f12fd03da35" + }, + { + "path": "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "usage": "input", + "git_blob": "c39913ce24cbce4c841eabcc9b1e5a18e4ccc754", + "sha256": "eded756dfe8f411c3d1f80a3ac16516f0ea5dd6f9866728b2179b157630fa7b6" + }, + { + "path": "research/rank7-joint-endframes/data/STAGE1-FRAME-EDITS.json", + "usage": "input", + "git_blob": "66525d293bd0e615e469b4c2191281e8cafb8788", + "sha256": "5fbfce004330ebc1fbac8de264614fe295f1a074811b478db4892c3bc3852cd3" + } + ] +} diff --git a/research/rank7-v45-group-audit/TASK.json b/research/rank7-v45-group-audit/TASK.json new file mode 100644 index 0000000000..fd8a01ffdd --- /dev/null +++ b/research/rank7-v45-group-audit/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently reconstruct #2979 group V45 (helpers 249, 251, 265, 267 on the shared rank-7 frame E_7 intersect E_42) on both PR2942 parent words, and price every subset against the published integer frame surrogate, including the losing single-helper controls.", + "scope_change_reason": "The card asks for one coordinated group and its losing single-change control, then the complete invoice. This package does that for V45 only. It does not rerun #2979 admission, re-derive the moment weights, or audit groups A-D, stage 2, or stage 3.", + "bottleneck_link": "A joint frame lowering is useful only if its paid profile, freed widths and cleanup actually improve the supplier bill. Checking one group against its single-change controls separates that local saving from the unvalidated kappa claim.", + "budget_minutes": 60, + "stop_rule": "Stop after one group, both parent words, and the subset-margin identity. Do not launch another lowering census or a full native admission if the local invoice still leaves the moment weights or supplier caps open.", + "outcome": "partial", + "evidence": "verify.py recomputes both parent profiles, all 16 V45 subsets, the exact overhead identity 4*(c_1-2091300)-78512=22972, unchanged cleanup, and two nonmonotone mutants.", + "author": "unpaidmoon", + "ai_assistance": "Substantial AI assistance from Cursor Grok.", + "open_questions": [ + { + "question": "Do groups A, B, C and D have the same exact one-rank saving per added helper, with a single shared frame overhead, on both parent words?", + "why_it_matters": "V45 is only one of the five groups in the #2979 stage-1 claim. The other four are not certified by this package.", + "first_step": "Repeat this verifier with those groups isolated by the same new-frame containment rule, without importing producer.py.", + "blocked_by": "Nothing mathematical blocks the same finite check. It was left out to keep this package to one group." + }, + { + "question": "Does the V45 local margin survive an independent enclosure of c_r and the full idle-width packing cap?", + "why_it_matters": "The +22972 unit margin uses #2979 published integer weights and a fixed break-even of 2091300. It is not a kappa and does not price idle children or the other supplier.", + "first_step": "Recompute lo_r(b) at b=0.001703676387993676 from the frame-domain-ceiling engines, then price the measured profile delta.", + "blocked_by": "Those engines and the T74 allocation are outside this package. Unknown cap movement is not zero." + } + ] +} diff --git a/research/rank7-v45-group-audit/VERIFY.json b/research/rank7-v45-group-audit/VERIFY.json new file mode 100644 index 0000000000..fcd2aff644 --- /dev/null +++ b/research/rank7-v45-group-audit/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank7-joint-endframes/data/PARENT-base.json.gz", + "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "research/rank7-joint-endframes/data/STAGE1-FRAME-EDITS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both PR2942 parents: reproduced profiles; V45 equals E_7 intersect E_42; every subset margin; joint delta -8388172; cleanup and scalars unchanged; width 8 to 7 by 4; omit-one-edit and stale-frame mutants are nonmonotone." + } + ] +} diff --git a/research/rank7-v45-group-audit/verify.py b/research/rank7-v45-group-audit/verify.py new file mode 100644 index 0000000000..f8b24441f3 --- /dev/null +++ b/research/rank7-v45-group-audit/verify.py @@ -0,0 +1,337 @@ +#!/usr/bin/env python3 +"""Independent audit of one #2979 rank-7 group: V45. + +Reconstructs the shared end frame of helpers 249, 251, 265 and 267 on both +PR2942 parent words, prices every subset against the published integer frame +surrogate, and checks the losing single-helper controls. This file does not +import research/rank7-joint-endframes/producer.py, verify.py, or +construction/STAGE-PRICES.json. + +The frame profile is a separate transcription of the inherited climb rules +(Jeremy Kothe, PR #2894, as stated in that package's vendored preload_move.py): +monotone subspace climbs, warp resets, centre/target cuts, and a final climb +to each live end frame. Calibration is the parent's stored profile, which this +transcription recomputes before any edit is applied. +""" + +from __future__ import annotations + +import copy +import gzip +import json +from collections import Counter +from itertools import combinations +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +DATA = ROOT / "research" / "rank7-joint-endframes" / "data" + +# Integer surrogate c_r = floor(2^40 * lo_r(b)) at the #2979 base saving. +# Not re-derived from the moment engines in this package. The break-even +# charge for one freed width unit is the published gap c_1 - 25371. +WEIGHTS = { + 1: 2116671, + 2: 4228346, + 3: 6338140, + 4: 8446713, + 5: 10554378, + 6: 12661320, + 7: 14767661, + 8: 16873488, + 9: 18978865, +} +PARTNER_ALLOWANCE = 25371 +BREAK_EVEN = WEIGHTS[1] - PARTNER_ALLOWANCE +HELPERS = (249, 251, 265, 267) +NORMALS = (7, 42, 45) + + +def basis(vectors): + pivot = {} + for value in vectors: + value = int(value) + while value: + bit = value.bit_length() - 1 + if bit in pivot: + value ^= pivot[bit] + else: + pivot[bit] = value + break + for row in sorted(pivot): + for other in list(pivot): + if other > row and (pivot[other] >> row) & 1: + pivot[other] ^= pivot[row] + return tuple(pivot[row] for row in sorted(pivot, reverse=True)) + + +def contained(small, big): + return basis(list(big) + list(small)) == basis(list(big)) + + +def orthogonal(normals): + survivors = [ + vector + for vector in range(512) + if all((vector & normal).bit_count() % 2 == 0 for normal in normals) + ] + return basis(survivors) + + +def roles(gate): + if gate[0] == "add": + return gate[1:3] + if gate[0] == "scale": + return gate[1:2] + raise ValueError("not a scalar gate") + + +def frame_report(word): + full = basis(1 << i for i in range(9)) + ends = ( + [full] * 112 + + [ + basis(vector for vector in range(1, 512) if (vector & port).bit_count() % 2 == 0) + for port in word["ports"] + ] + + [full] * 480 + ) + for register, frame in word["helper_final"].items(): + ends[int(register)] = basis(frame) + current = [(port,) for port in word["ports"]] + [()] * (112 + 480) + for register, frame in word["start_extra"].items(): + current[int(register)] = basis(frame) + paid = Counter() + + def climb(register, frame): + frame = basis(frame) + if not contained(current[register], frame): + raise ValueError("nonmonotone") + rank_jump = len(frame) - len(current[register]) + if rank_jump: + paid[rank_jump] += 1 + current[register] = frame + + def step(gate): + if gate[0] == "warp": + if current[gate[1]] != basis(gate[3]): + raise ValueError("warp") + current[gate[1]] = basis(gate[4]) + return + for register in roles(gate): + climb(register, gate[-1]) + + for gate in word["A"]: + step(gate) + for register, frame in zip(word["centers"], word["center_frames"]): + if current[register] != basis(frame): + raise ValueError("centre") + level = frame + targets = sorted( + { + basis(word["target_levels"].get(str(gate[1] - 112), [])) + for gate in word["cut"] + if gate[2] == register + }, + key=len, + reverse=True, + ) + for target in targets: + if basis(level) != target: + paid[len(level) - len(target)] += 1 + level = target + warps = {} + for record in word["warps"]: + warps.setdefault(record[0], []).append(record) + for position in range(len(word["B"]) + 1): + for record in warps.get(position, []): + if current[record[1]] != basis(record[3]): + raise ValueError("Bwarp") + current[record[1]] = basis(record[4]) + if position < len(word["B"]): + step(word["B"][position]) + for gate in word["restore"]: + step(gate) + live = set(range(704)) - set(word["removed"]) + for register in live: + climb(register, ends[register]) + starts = [(port,) for port in word["ports"]] + [()] * (112 + 480) + for register, frame in word["start_extra"].items(): + starts[int(register)] = basis(frame) + inventory = Counter( + len(ends[register]) - len(starts[register]) + for register in live + if register >= 224 + ) + return ( + {str(rank): count for rank, count in sorted(paid.items())}, + {str(width): count for width, count in sorted(inventory.items())}, + ) + + +def cost(profile): + return sum(WEIGHTS[int(rank)] * count for rank, count in profile.items()) + + +def group_owners(record, frame): + return [ + name + for name, payload in record["groups"].items() + if contained(frame, payload[0]) + ] + + +def apply_v45(parent, record, edits, helpers): + word = copy.deepcopy(parent) + subspace = list(record["groups"]["V45"][0]) + for helper in helpers: + change = record["helper_final_changes"][str(helper)] + if change["old"] != word["helper_final"][str(helper)] or change["new"] != subspace: + raise ValueError("end-frame preimage") + word["helper_final"][str(helper)] = list(subspace) + for edit in edits: + gate = word[edit["section"]][edit["index"]] + if gate[:-1] != edit["gate"] or gate[-1] != edit["old_frame"]: + raise ValueError("gate preimage") + gate[-1] = list(edit["new_frame"]) + profile, inventory = frame_report(word) + return word, profile, inventory + + +def margin(delta, freed): + return -delta - freed * BREAK_EVEN + + +def gates_outside(word, helpers, subspace): + outside = 0 + for helper in helpers: + for section in ("A", "B", "restore"): + for gate in word[section]: + if gate[0] in ("add", "scale") and helper in roles(gate) and not contained(gate[-1], subspace): + outside += 1 + return outside + + +def expect_nonmonotone(parent, record, edits, helpers): + try: + apply_v45(parent, record, edits, helpers) + except ValueError as error: + if str(error) != "nonmonotone": + raise SystemExit("control rejected for the wrong reason: " + str(error)) + return + raise SystemExit("control accepted a nonmonotone mutant") + + +def audit_provider(tag, record, edits): + with gzip.open(DATA / f"PARENT-{tag}.json.gz", "rt", encoding="utf-8") as handle: + parent = json.load(handle) + parent_profile, parent_inventory = frame_report(parent) + if parent_profile != parent["report"]["local_profile"]: + raise SystemExit(tag + " parent profile was not reproduced") + if parent_inventory != parent["report"]["width_inventory"]: + raise SystemExit(tag + " parent width inventory was not reproduced") + subspace = record["groups"]["V45"][0] + if list(orthogonal((7, 42))) != list(subspace): + raise SystemExit("V45 is not E_7 intersect E_42") + if (7 ^ 42) != 45 or any((vector & normal).bit_count() % 2 for vector in subspace for normal in NORMALS): + raise SystemExit("V45 normal identity failed") + for helper in HELPERS: + old = parent["helper_final"][str(helper)] + if len(basis(old)) != 8 or len(basis(subspace)) != 7 or not contained(subspace, old): + raise SystemExit("lowered end frame is not a hyperplane of the old end frame") + + base = cost(parent_profile) + subset_margins = {} + joint_word = None + joint_profile = None + joint_inventory = None + for size in range(5): + found = set() + for subset in combinations(HELPERS, size): + word, profile, inventory = apply_v45(parent, record, edits, subset) + found.add(margin(cost(profile) - base, size)) + if size == 4: + joint_word, joint_profile, joint_inventory = word, profile, inventory + if size == len(subset) and gates_outside(word, subset, subspace): + raise SystemExit("a lowered helper is touched outside W") + subset_margins[size] = found + expected = { + 0: {-78512}, + 1: {-53141}, + 2: {-27770}, + 3: {-2399}, + 4: {22972}, + } + if subset_margins != expected: + raise SystemExit(tag + " subset margins " + str(subset_margins)) + joint_delta = cost(joint_profile) - base + if joint_delta != -8388172 or margin(joint_delta, 4) != 22972: + raise SystemExit(tag + " joint price mismatch") + overhead = joint_delta + 4 * WEIGHTS[1] + if overhead != 78512 or 4 * PARTNER_ALLOWANCE - overhead != 22972: + raise SystemExit(tag + " overhead decomposition mismatch") + if joint_word["cleanup"] != parent["cleanup"] or len(joint_word["helper_final"]) != 86: + raise SystemExit(tag + " cleanup or buffer count changed") + if any( + before[:-1] != after[:-1] + for section in ("A", "B", "restore") + for before, after in zip(parent[section], joint_word[section]) + ): + raise SystemExit(tag + " a scalar or operator changed") + width_delta = { + key: joint_inventory.get(key, 0) - parent_inventory.get(key, 0) + for key in sorted(set(joint_inventory) | set(parent_inventory), key=int) + } + if width_delta != {"4": 0, "5": 0, "7": 4, "8": -4, "9": 0}: + raise SystemExit(tag + " width inventory " + str(width_delta)) + sections = Counter(edit["section"] for edit in edits) + if set(sections) != {"B", "restore"}: + raise SystemExit(tag + " V45 edits are not confined to B and restore") + + touching = [edit for edit in edits if set(roles(edit["gate"])) & set(HELPERS)] + omitted = [edit for edit in edits if edit is not touching[0]] + expect_nonmonotone(parent, record, omitted, HELPERS) + stale = copy.deepcopy(edits) + for edit in stale: + if edit["section"] == touching[0]["section"] and edit["index"] == touching[0]["index"]: + edit["new_frame"] = list(edit["old_frame"]) + break + expect_nonmonotone(parent, record, stale, HELPERS) + return { + "joint_delta": joint_delta, + "joint_margin": 22972, + "sections": dict(sections), + "edits": len(edits), + } + + +def main(): + if BREAK_EVEN != 2091300: + raise SystemExit("break-even identity failed") + record = json.loads((DATA / "STAGE1-FRAME-EDITS.json").read_text(encoding="utf-8")) + if record["groups"]["V45"][1] != list(HELPERS): + raise SystemExit("V45 helper list changed") + edits = [ + edit + for edit in record["frame_edits"] + if group_owners(record, edit["new_frame"]) == ["V45"] + ] + if len(edits) != 61: + raise SystemExit("expected 61 V45-only frame edits") + reports = {tag: audit_provider(tag, record, edits) for tag in ("base", "extra")} + if reports["base"] != reports["extra"]: + raise SystemExit("providers disagree: " + str(reports)) + report = reports["base"] + print( + "PASS_RANK7_V45_GROUP_AUDIT" + f" providers=2 edits={report['edits']}" + f" sections={report['sections']['B']}+{report['sections']['restore']}" + " joint_delta=-8388172 joint_margin=22972" + " single_margin=-53141 pair_margin=-27770 triple_margin=-2399" + " frame_only_margin=-78512 overhead=78512" + " width_8_to_7=4 buffers=86 cleanup_unchanged=yes" + " controls=omit-edit,stale-frame" + ) + + +if __name__ == "__main__": + main() From 0a95f35e7f76a17f6029cfc7c808fdaf6cb9d488 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 01:47:41 +0000 Subject: [PATCH 2/2] Narrow the V45 audit to the measured 61-edit monotone walk. Open PRs #3911, #3543, #3823 and #3841 already cover the intersection, the printed margin ladder, and endpoint subsets on the full 139-edit word. The remaining witness is the exclusive-containment walk: 61 edits measure +78512 with endpoints fixed and -8388172 with all four lowered, while the 29 role edits stay nonmonotone at register 169. Co-authored-by: unpaidmoon --- research/rank7-v45-group-audit/README.md | 153 +++++++++++---------- research/rank7-v45-group-audit/TASK.json | 28 ++-- research/rank7-v45-group-audit/VERIFY.json | 4 +- research/rank7-v45-group-audit/verify.py | 148 +++++++++++++------- 4 files changed, 200 insertions(+), 133 deletions(-) diff --git a/research/rank7-v45-group-audit/README.md b/research/rank7-v45-group-audit/README.md index 4a106ed794..fbd7126e6e 100644 --- a/research/rank7-v45-group-audit/README.md +++ b/research/rank7-v45-group-audit/README.md @@ -1,78 +1,81 @@ -# Independent audit of #2979 group V45 +# Measured V45 price on a monotone 61-edit walk **Partial frame-surrogate certificate. No new κ.** Selected κ stays `0.001672660197076918`. PR #2979's conditional κ ≈ 0.001729 is not selected and is not re-certified here. -On both PR #2942 parent words, the four restored helpers 249, 251, 265 and 267 -share one rank-7 end frame +Upstream main checked 2026-10-20 is still `bb4bccbf42844d2801487450727c2f63e10d1d0f` +(priority revision 6). The three replay inputs have the same git blobs there. -```text -W = ⟨256, 128, 64, 35, 16, 11, 5⟩ = E_7 ∩ E_42 = E_7 ∩ E_42 ∩ E_45 -``` - -because `7 ⊕ 42 = 45`. Lowering any proper subset of those four end frames, after -the 61 gate frames that land only in `W`, loses money under #2979's published -integer frame weights. Lowering all four gains **22,972** surrogate units. -The shared gate-frame overhead is **78,512** units, and each added helper then -saves exactly one rank-1 climb, `c_1 = 2,116,671`. +## What the open V45 audits already cover -## What was checked +[PR #3911](https://github.com/CrocSwap/integer-mult-bounds/pull/3911) rebuilds +the frame walk and the stage-one ledger. It toggles the four V45 endpoints +under all 139 gate edits, checks the 15 nonempty subset profiles, and gets +margins `−53,141`, `−27,770`, `−2,399` and `+22,972`. The `+78,512` figure in +that audit is the pinned V45 `joint_delta` minus an endpoint delta of +`−4·c_1`. Its open question is to rederive that group price on a monotone +walk. The blocker it records is that the 29 edits naming helpers 249, 251, +265 or 267 are nonmonotone at register 169. -The parents are `research/rank7-joint-endframes/data/PARENT-base.json.gz` and -`PARENT-extra.json.gz`, with the stage-1 record -`STAGE1-FRAME-EDITS.json`. Group V45 owns the 61 edits whose new frame is -contained in `W` and in no other declared group frame (20 in `B`, 41 in -`restore`). No `A` gate moves. Scalars, operators and the cleanup list are -unchanged, and the private-buffer count stays 86. +[PR #3543](https://github.com/CrocSwap/integer-mult-bounds/pull/3543) checks +the printed intersection and the declared subset margins from the price table. +[PR #3823](https://github.com/CrocSwap/integer-mult-bounds/pull/3823) records +the 128-vector triple intersection `E_7 ∩ E_42 ∩ E_45`. +[PR #3841](https://github.com/CrocSwap/integer-mult-bounds/pull/3841) records +the printed arithmetic-progression ladder (difference 25,371) and the sum of +the five joint prices. Those three do not replay an isolated word. -The paid profile is recomputed by a separate transcription of the inherited -climb rules (monotone subspace climbs, warp resets, centre and target cuts, -final climb to the live end frame). It is not imported from -`rank7-joint-endframes/producer.py` or from `STAGE-PRICES.json`. Calibration: -both stored parent profiles and width inventories are reproduced before any -edit. Weights are the published surrogate - -```text -c = (2116671, 4228346, 6338140, 8446713, 10554378, 12661320, 14767661, 16873488, 18978865) -``` +## What this package adds -at the recorded base saving, and the break-even charge for one freed width is -`c_1 - 25371 = 2091300`. This package does not re-derive `c_r` from the moment -engines. +The stage-one record has 61 edits whose new frame is contained in the declared +V45 frame and in no other declared group frame: 20 in `B` and 41 in `restore`. +Twenty-nine of them name a V45 helper. That is the same set of 29 edits named +by #3911. The other 32 name only partner registers (14 in `B`, 18 in +`restore`; new-frame dimensions 18 of rank 7, 6 of rank 5, 4 of rank 6 and 4 +of rank 4). -For a subset of `k` helpers, with those end frames set to `W` and all 61 gate -frames applied, the margin is `-Δ - k·2091300`. Both providers give the same -margins: +On both PR #2942 parents, replaying those 61 gate frames is monotone. -| k | subsets | margin | +| Endpoints lowered | Measured profile delta | Margin `−Δ − k·2,091,300` | |---:|---:|---:| -| 0 | 1 | −78,512 | -| 1 | 4 | −53,141 | -| 2 | 6 | −27,770 | -| 3 | 4 | −2,399 | -| 4 | 1 | **+22,972** | - -The `k = 4` profile delta is `−8,388,172`, and the width inventory moves four -units from width 8 to width 7. The identity - -```text -4·25371 − 78512 = 22972 -``` - -is the whole joint margin: partner frames are paid once, and each helper -returns `c_1` against a break-even of `c_1 - 25371`. Every one-helper control -loses. Omitting the first helper-touching edit, or putting that gate's old -frame back, makes the word nonmonotone. +| 0 | **+78,512** | −78,512 | +| 1 | | −53,141 | +| 2 | | −27,770 | +| 3 | | −2,399 | +| 4 | **−8,388,172** | **+22,972** | + +The joint delta equals the measured gate-only cost minus four rank-1 tariffs: +`78512 − 4·2,116,671 = −8,388,172`. The weights are the published surrogate. +`STAGE-PRICES.json` is not read, so the overhead is a profile cost of this +walk. The same identity gives `4·25,371 − 78,512 = 22,972`. + +The 29 role edits alone, with or without the four endpoint changes, are +nonmonotone at register 169 on both parents. That agrees with the blocker +stated in #3911. Extending those 29 by any one partner edit, still with +endpoints unchanged, stays nonmonotone. Separately, every 60-edit subset of +the joint walk is nonmonotone, so each partner edit is required in the +four-endpoint witness. + +Every 60-edit subset of the 61 makes the four-endpoint walk nonmonotone. Two +role edits are a gate-only exception: omitting `restore` index 137, or +`restore` index 157, keeps the no-endpoint walk monotone and raises its cost +from 78,512 to 83,508. With all four endpoints lowered, those omissions fail +at registers 267 and 265. So the joint witness uses all 61 edits, and no +60-edit subset is a joint witness. + +Scalars, operators and the cleanup list stay fixed. The private-buffer count +stays 86. The joint width inventory moves four units from width 8 to width 7. ## What this does not establish -Groups A–D, the five paired extractions, the fourteen rewrites, the T74 -allocation, idle packing, native admission and both supplier caps are +The intersection, the printed ladder, the endpoint subsets of the full +139-edit word, and the physical invoice remain the subjects of #3823, #3841, +#3543 and #3911. This package does not rerun that ledger. Matching the pinned +V45 price on one monotone walk does not show that the frame search was +optimal. Groups A–D, idle packing, native admission and both supplier caps are unchecked. A positive local margin in this surrogate is not a multiplication -exponent. `research/rank7-joint-endframes-restore-edit` starts from the #2979 -words and does not replace this group check. PR #3585 records archive blobs -only. +exponent. ## Reproduce @@ -86,28 +89,34 @@ python3 -B scripts/research_package.py --package research/rank7-v45-group-audit Expected first line: ```text -PASS_RANK7_V45_GROUP_AUDIT providers=2 edits=61 sections=20+41 joint_delta=-8388172 joint_margin=22972 single_margin=-53141 pair_margin=-27770 triple_margin=-2399 frame_only_margin=-78512 overhead=78512 width_8_to_7=4 buffers=86 cleanup_unchanged=yes controls=omit-edit,stale-frame +PASS_RANK7_V45_MONOTONE_SPLIT providers=2 containment_edits=61 role_edits=29 partner_only=32 sections=20+41 role_only_nonmonotone=169 measured_overhead=78512 joint_delta=-8388172 joint_margin=22972 single_margin=-53141 leave_one_out_joint=nonmonotone one_partner_extension=nonmonotone gate_only_omit_restore_137_or_157=83508 ``` -The direct verifier finished in about 6 seconds on the recorded host. - ## Open next questions -1. Isolate groups A, B, C and D by the same containment rule and test whether - each added helper saves exactly `c_1` after one shared overhead. That is the - same finite check; it was not run here. -2. Enclose `c_r` independently at `b = 0.001703676387993676` and price this - profile delta through the idle-width cap. Until that is done, the unit - margin does not move κ. The frame-domain-ceiling engines are the blocker. +1. Is there a proper subset of these 61 edits, necessarily omitting at least + two of them, that stays monotone for every endpoint subset and still + measures `+78,512` and `−8,388,172`? Every 60-edit subset fails the joint + walk, and the two gate-only omissions above miss the joint price. A + compensating pair remains unchecked. The missing frame-search witness also + leaves optimality open. +2. Do groups A–D have an exclusive-containment superset of their + helper-touching edits that is monotone and prices the group from profile + costs? #3911's residual method still leaves those four group prices on the + pinned row. +3. Does this local margin survive an independent enclosure of `c_r` at + `b = 0.001703676387993676` and the idle-width cap? Until that is done, the + unit margin does not move κ. ## Credit Marius-Paul Dumitrean (Dugongue / mdumitrean), PR #2979, for the words, the -V45 claim and the published weights under audit. The parent words descend from -Mason Hale's PR #2917 and the PR #2942 extractions; frame climb rules are -Jeremy Kothe's, from the PR #2894 lineage. Jeremy Diviney's paired-extraction -method and Dugongue's PR #2969 comparator sit behind that claim and are not -rechecked here. Archive disposition PR #3585 is separate. +V45 claim and the published weights. The parent words descend from Mason +Hale's PR #2917 and the PR #2942 extractions. Frame climb rules are Jeremy +Kothe's, from the PR #2894 lineage. 1337isnot1337, PR #3911, for the +independent frame and ledger audit whose open question this walk answers. +jwr404, PRs #3543, #3823 and #3841, for the intersection and printed-ladder +checks cited above. Prepared by unpaidmoon with substantial AI assistance (Cursor Grok). No independent human or formal-kernel review is claimed. Apache-2.0. diff --git a/research/rank7-v45-group-audit/TASK.json b/research/rank7-v45-group-audit/TASK.json index fd8a01ffdd..50d73b00bb 100644 --- a/research/rank7-v45-group-audit/TASK.json +++ b/research/rank7-v45-group-audit/TASK.json @@ -46,25 +46,31 @@ ] }, "scope_status": "refined", - "actual_scope": "Independently reconstruct #2979 group V45 (helpers 249, 251, 265, 267 on the shared rank-7 frame E_7 intersect E_42) on both PR2942 parent words, and price every subset against the published integer frame surrogate, including the losing single-helper controls.", - "scope_change_reason": "The card asks for one coordinated group and its losing single-change control, then the complete invoice. This package does that for V45 only. It does not rerun #2979 admission, re-derive the moment weights, or audit groups A-D, stage 2, or stage 3.", - "bottleneck_link": "A joint frame lowering is useful only if its paid profile, freed widths and cleanup actually improve the supplier bill. Checking one group against its single-change controls separates that local saving from the unvalidated kappa claim.", + "actual_scope": "On both PR2942 parents, measure the V45 group price as the profile cost of the 61 stage-one edits whose new frame lies only in the declared V45 frame. That walk is monotone: +78512 with endpoints unchanged and -8388172 with all four endpoints lowered. The 29 helper-touching edits are nonmonotone at register 169, and every 60-edit subset of the joint walk is nonmonotone.", + "scope_change_reason": "The card asks for one coordinated group and its losing single-change control. After overlap with open PRs #3911, #3543, #3823 and #3841, the package keeps only the missing monotone decomposition: #3911 already prices endpoint subsets on the full 139-edit word and derives +78512 from the pinned price row, and it records that the 29 role edits are nonmonotone at register 169. Intersection, printed ladder and the physical ledger are not re-offered as the result. Moment weights, groups A-D, stage 2 and stage 3 stay out of scope.", + "bottleneck_link": "A joint frame lowering is useful only if its paid profile can be attributed without inheriting the search-time price row. Measuring one monotone group walk separates that local saving from the unvalidated kappa claim.", "budget_minutes": 60, - "stop_rule": "Stop after one group, both parent words, and the subset-margin identity. Do not launch another lowering census or a full native admission if the local invoice still leaves the moment weights or supplier caps open.", + "stop_rule": "Stop after the 61-edit witness, the 29-edit register-169 control, and the joint leave-one-out. Do not rerun the #3911 ledger or launch another lowering census.", "outcome": "partial", - "evidence": "verify.py recomputes both parent profiles, all 16 V45 subsets, the exact overhead identity 4*(c_1-2091300)-78512=22972, unchanged cleanup, and two nonmonotone mutants.", + "evidence": "verify.py replays both parents without STAGE-PRICES.json. The 61-edit walk measures overhead 78512 and joint delta -8388172. The 29 role edits fail at register 169 with and without the four endpoint changes, and adding any one partner edit to those 29 stays nonmonotone when endpoints are unchanged. Every 60-edit subset of the joint walk is nonmonotone. Omitting restore index 137 or 157 keeps the gate-only walk monotone at cost 83508 and breaks the joint walk.", "author": "unpaidmoon", "ai_assistance": "Substantial AI assistance from Cursor Grok.", "open_questions": [ { - "question": "Do groups A, B, C and D have the same exact one-rank saving per added helper, with a single shared frame overhead, on both parent words?", - "why_it_matters": "V45 is only one of the five groups in the #2979 stage-1 claim. The other four are not certified by this package.", - "first_step": "Repeat this verifier with those groups isolated by the same new-frame containment rule, without importing producer.py.", - "blocked_by": "Nothing mathematical blocks the same finite check. It was left out to keep this package to one group." + "question": "Is there a proper subset of the 61 V45-only edits, omitting at least two, that stays monotone for every endpoint subset and still measures +78512 and -8388172?", + "why_it_matters": "Every 60-edit subset fails the four-endpoint walk, so a smaller witness would have to omit two or more edits at once. The two gate-only omissions (restore 137 and restore 157) miss the joint price. A smaller witness, or a proof that none exists, is the remaining optimality gap left open by the absent frame-search log.", + "first_step": "Search pairs drawn from the 29 role edits, keep all 32 partner edits, and reject any walk whose joint profile cost is not -8388172.", + "blocked_by": "Nothing mathematical blocks a finite pair search. It was left unrun. The #2979 archive still has no optimizer witness." }, { - "question": "Does the V45 local margin survive an independent enclosure of c_r and the full idle-width packing cap?", - "why_it_matters": "The +22972 unit margin uses #2979 published integer weights and a fixed break-even of 2091300. It is not a kappa and does not price idle children or the other supplier.", + "question": "Do groups A, B, C and D have an exclusive-containment edit set that is monotone and prices each group from profile costs?", + "why_it_matters": "V45 is one of five stage-one groups. PR #3911 still takes the other four joint prices from the pinned row.", + "first_step": "Repeat the containment split for each remaining group, without importing producer.py or STAGE-PRICES.json.", + "blocked_by": "Nothing mathematical blocks the same finite check. It was left out after the V45 overlap shrink." + }, + { + "question": "Does the measured V45 margin survive an independent enclosure of c_r and the idle-width packing cap?", + "why_it_matters": "The +22972 unit margin uses the published integer weights and a fixed break-even of 2091300. It is a local surrogate margin, so it does not move kappa.", "first_step": "Recompute lo_r(b) at b=0.001703676387993676 from the frame-domain-ceiling engines, then price the measured profile delta.", "blocked_by": "Those engines and the T74 allocation are outside this package. Unknown cap movement is not zero." } diff --git a/research/rank7-v45-group-audit/VERIFY.json b/research/rank7-v45-group-audit/VERIFY.json index fcd2aff644..411ee9d6fa 100644 --- a/research/rank7-v45-group-audit/VERIFY.json +++ b/research/rank7-v45-group-audit/VERIFY.json @@ -15,8 +15,8 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 120, - "checks": "Both PR2942 parents: reproduced profiles; V45 equals E_7 intersect E_42; every subset margin; joint delta -8388172; cleanup and scalars unchanged; width 8 to 7 by 4; omit-one-edit and stale-frame mutants are nonmonotone." + "timeout_seconds": 180, + "checks": "Both PR2942 parents. The 29 helper-touching edits fail at register 169 with and without the four endpoint changes. Adding any one of the 32 partner edits to those 29 stays nonmonotone when endpoints are unchanged. The 61 exclusive-containment edits are monotone, measure gate-only cost +78512 and four-endpoint cost -8388172 without STAGE-PRICES.json, and every 60-edit subset of the joint walk is nonmonotone. Omitting restore 137 or restore 157 leaves the gate-only cost at 83508 and breaks the joint walk. Cleanup and scalars stay fixed." } ] } diff --git a/research/rank7-v45-group-audit/verify.py b/research/rank7-v45-group-audit/verify.py index f8b24441f3..720fe45db8 100644 --- a/research/rank7-v45-group-audit/verify.py +++ b/research/rank7-v45-group-audit/verify.py @@ -1,11 +1,19 @@ #!/usr/bin/env python3 -"""Independent audit of one #2979 rank-7 group: V45. - -Reconstructs the shared end frame of helpers 249, 251, 265 and 267 on both -PR2942 parent words, prices every subset against the published integer frame -surrogate, and checks the losing single-helper controls. This file does not -import research/rank7-joint-endframes/producer.py, verify.py, or -construction/STAGE-PRICES.json. +"""Measured V45 price on the monotone 61-edit walk. + +PR #3911 prices V45 endpoint subsets on the full 139-edit stage-one word and +obtains the shared overhead by subtracting a measured endpoint delta from the +pinned group-price row. The 29 edits that name helpers 249, 251, 265 or 267 +are nonmonotone at register 169, so that audit leaves the group price +underived. + +This verifier selects the 61 stage-one edits whose new frame lies in the +declared V45 frame and in no other declared group frame. On both PR #2942 +parents that walk is monotone. Its profile cost is +78512 with the four +endpoints left unchanged and -8388172 with all four lowered. Every 60-edit +subset of that joint walk is nonmonotone. The weights are the published +surrogate. This file does not import producer.py, verify.py, or +STAGE-PRICES.json. The frame profile is a separate transcription of the inherited climb rules (Jeremy Kothe, PR #2894, as stated in that package's vendored preload_move.py): @@ -44,6 +52,13 @@ BREAK_EVEN = WEIGHTS[1] - PARTNER_ALLOWANCE HELPERS = (249, 251, 265, 267) NORMALS = (7, 42, 45) +# These two role edits can be omitted from the gate-only walk. The walk stays +# monotone, and the profile cost rises from 78512 to 83508. With all four +# endpoints lowered, omitting either edit is nonmonotone at that helper. +GATE_ONLY_EXCEPTIONS = { + ("restore", 137): 267, + ("restore", 157): 265, +} def basis(vectors): @@ -85,6 +100,10 @@ def roles(gate): raise ValueError("not a scalar gate") +def edit_key(edit): + return (edit["section"], edit["index"]) + + def frame_report(word): full = basis(1 << i for i in range(9)) ends = ( @@ -105,7 +124,7 @@ def frame_report(word): def climb(register, frame): frame = basis(frame) if not contained(current[register], frame): - raise ValueError("nonmonotone") + raise ValueError("nonmonotone " + str(register)) rank_jump = len(frame) - len(current[register]) if rank_jump: paid[rank_jump] += 1 @@ -180,6 +199,10 @@ def group_owners(record, frame): ] +def touches_v45(edit): + return bool(set(roles(edit["gate"])) & set(HELPERS)) + + def apply_v45(parent, record, edits, helpers): word = copy.deepcopy(parent) subspace = list(record["groups"]["V45"][0]) @@ -211,17 +234,25 @@ def gates_outside(word, helpers, subspace): return outside -def expect_nonmonotone(parent, record, edits, helpers): +def expect_nonmonotone(parent, record, edits, helpers, register=None): try: apply_v45(parent, record, edits, helpers) except ValueError as error: - if str(error) != "nonmonotone": - raise SystemExit("control rejected for the wrong reason: " + str(error)) + text = str(error) + if register is None: + if not text.startswith("nonmonotone "): + raise SystemExit("control rejected for the wrong reason: " + text) + elif text != "nonmonotone " + str(register): + raise SystemExit("control rejected at " + text + ", expected register " + str(register)) return raise SystemExit("control accepted a nonmonotone mutant") -def audit_provider(tag, record, edits): +def without(edits, key): + return [edit for edit in edits if edit_key(edit) != key] + + +def audit_provider(tag, record, edits, role_edits): with gzip.open(DATA / f"PARENT-{tag}.json.gz", "rt", encoding="utf-8") as handle: parent = json.load(handle) parent_profile, parent_inventory = frame_report(parent) @@ -239,19 +270,31 @@ def audit_provider(tag, record, edits): if len(basis(old)) != 8 or len(basis(subspace)) != 7 or not contained(subspace, old): raise SystemExit("lowered end frame is not a hyperplane of the old end frame") + expect_nonmonotone(parent, record, role_edits, (), register=169) + expect_nonmonotone(parent, record, role_edits, HELPERS, register=169) + partner_edits = [edit for edit in edits if not touches_v45(edit)] + for edit in partner_edits: + expect_nonmonotone(parent, record, role_edits + [edit], ()) + base = cost(parent_profile) subset_margins = {} joint_word = None joint_profile = None joint_inventory = None + overhead = None + joint_delta = None for size in range(5): found = set() for subset in combinations(HELPERS, size): word, profile, inventory = apply_v45(parent, record, edits, subset) - found.add(margin(cost(profile) - base, size)) + delta = cost(profile) - base + found.add(margin(delta, size)) + if size == 0: + overhead = delta if size == 4: joint_word, joint_profile, joint_inventory = word, profile, inventory - if size == len(subset) and gates_outside(word, subset, subspace): + joint_delta = delta + if size and gates_outside(word, subset, subspace): raise SystemExit("a lowered helper is touched outside W") subset_margins[size] = found expected = { @@ -261,14 +304,12 @@ def audit_provider(tag, record, edits): 3: {-2399}, 4: {22972}, } - if subset_margins != expected: - raise SystemExit(tag + " subset margins " + str(subset_margins)) - joint_delta = cost(joint_profile) - base - if joint_delta != -8388172 or margin(joint_delta, 4) != 22972: - raise SystemExit(tag + " joint price mismatch") - overhead = joint_delta + 4 * WEIGHTS[1] - if overhead != 78512 or 4 * PARTNER_ALLOWANCE - overhead != 22972: - raise SystemExit(tag + " overhead decomposition mismatch") + if overhead != 78512 or subset_margins != expected: + raise SystemExit(tag + " measured margins " + str(subset_margins) + " overhead " + str(overhead)) + if joint_delta != overhead - 4 * WEIGHTS[1] or joint_delta != -8388172: + raise SystemExit(tag + " joint delta is not the measured gate cost minus four rank-1 savings") + if margin(joint_delta, 4) != 22972 or 4 * PARTNER_ALLOWANCE - overhead != 22972: + raise SystemExit(tag + " overhead identity failed") if joint_word["cleanup"] != parent["cleanup"] or len(joint_word["helper_final"]) != 86: raise SystemExit(tag + " cleanup or buffer count changed") if any( @@ -283,24 +324,20 @@ def audit_provider(tag, record, edits): } if width_delta != {"4": 0, "5": 0, "7": 4, "8": -4, "9": 0}: raise SystemExit(tag + " width inventory " + str(width_delta)) - sections = Counter(edit["section"] for edit in edits) - if set(sections) != {"B", "restore"}: - raise SystemExit(tag + " V45 edits are not confined to B and restore") - - touching = [edit for edit in edits if set(roles(edit["gate"])) & set(HELPERS)] - omitted = [edit for edit in edits if edit is not touching[0]] - expect_nonmonotone(parent, record, omitted, HELPERS) - stale = copy.deepcopy(edits) - for edit in stale: - if edit["section"] == touching[0]["section"] and edit["index"] == touching[0]["index"]: - edit["new_frame"] = list(edit["old_frame"]) - break - expect_nonmonotone(parent, record, stale, HELPERS) + + for edit in edits: + expect_nonmonotone(parent, record, without(edits, edit_key(edit)), HELPERS) + for key, helper_register in GATE_ONLY_EXCEPTIONS.items(): + reduced = without(edits, key) + _, profile, _ = apply_v45(parent, record, reduced, ()) + if cost(profile) - base != 83508: + raise SystemExit(tag + " gate-only omission " + str(key) + " changed cost unexpectedly") + expect_nonmonotone(parent, record, reduced, HELPERS, register=helper_register) return { "joint_delta": joint_delta, - "joint_margin": 22972, - "sections": dict(sections), + "overhead": overhead, "edits": len(edits), + "role_edits": len(role_edits), } @@ -315,21 +352,36 @@ def main(): for edit in record["frame_edits"] if group_owners(record, edit["new_frame"]) == ["V45"] ] - if len(edits) != 61: - raise SystemExit("expected 61 V45-only frame edits") - reports = {tag: audit_provider(tag, record, edits) for tag in ("base", "extra")} + role_edits = [edit for edit in record["frame_edits"] if touches_v45(edit)] + if [edit_key(edit) for edit in role_edits] != [edit_key(edit) for edit in edits if touches_v45(edit)]: + raise SystemExit("a helper-touching edit lies outside the V45-only frames") + partner_edits = [edit for edit in edits if not touches_v45(edit)] + if len(edits) != 61 or len(role_edits) != 29 or len(partner_edits) != 32: + raise SystemExit("expected 61 V45-only edits, 29 role edits and 32 partner edits") + if Counter(edit["section"] for edit in edits) != Counter({"B": 20, "restore": 41}): + raise SystemExit("V45-only edits are not 20 in B and 41 in restore") + if Counter(edit["section"] for edit in partner_edits) != Counter({"B": 14, "restore": 18}): + raise SystemExit("partner-only section counts changed") + if Counter(len(basis(edit["new_frame"])) for edit in partner_edits) != Counter({7: 18, 5: 6, 4: 4, 6: 4}): + raise SystemExit("partner-only new-frame dimensions changed") + if not set(GATE_ONLY_EXCEPTIONS) <= {edit_key(edit) for edit in role_edits}: + raise SystemExit("gate-only exceptions are not role edits") + reports = { + tag: audit_provider(tag, record, edits, role_edits) for tag in ("base", "extra") + } if reports["base"] != reports["extra"]: raise SystemExit("providers disagree: " + str(reports)) report = reports["base"] print( - "PASS_RANK7_V45_GROUP_AUDIT" - f" providers=2 edits={report['edits']}" - f" sections={report['sections']['B']}+{report['sections']['restore']}" - " joint_delta=-8388172 joint_margin=22972" - " single_margin=-53141 pair_margin=-27770 triple_margin=-2399" - " frame_only_margin=-78512 overhead=78512" - " width_8_to_7=4 buffers=86 cleanup_unchanged=yes" - " controls=omit-edit,stale-frame" + "PASS_RANK7_V45_MONOTONE_SPLIT" + f" providers=2 containment_edits={report['edits']}" + f" role_edits={report['role_edits']} partner_only=32" + " sections=20+41 role_only_nonmonotone=169" + f" measured_overhead={report['overhead']} joint_delta={report['joint_delta']}" + " joint_margin=22972 single_margin=-53141" + " leave_one_out_joint=nonmonotone" + " one_partner_extension=nonmonotone" + " gate_only_omit_restore_137_or_157=83508" )