From cd120c8fa63861d27a00970257ad2dc967818dd4 Mon Sep 17 00:00:00 2001 From: Gonzalo-Mier Date: Sat, 17 Oct 2026 00:07:19 +0200 Subject: [PATCH 1/2] Research: independently audit rank-7 V45 profile --- research/rank7-v45-profile-audit/README.md | 32 ++ research/rank7-v45-profile-audit/SOURCES.json | 72 ++++ research/rank7-v45-profile-audit/TASK.json | 72 ++++ research/rank7-v45-profile-audit/VERIFY.json | 29 ++ research/rank7-v45-profile-audit/verify.py | 311 ++++++++++++++++++ 5 files changed, 516 insertions(+) create mode 100644 research/rank7-v45-profile-audit/README.md create mode 100644 research/rank7-v45-profile-audit/SOURCES.json create mode 100644 research/rank7-v45-profile-audit/TASK.json create mode 100644 research/rank7-v45-profile-audit/VERIFY.json create mode 100644 research/rank7-v45-profile-audit/verify.py diff --git a/research/rank7-v45-profile-audit/README.md b/research/rank7-v45-profile-audit/README.md new file mode 100644 index 0000000000..3139f163d5 --- /dev/null +++ b/research/rank7-v45-profile-audit/README.md @@ -0,0 +1,32 @@ +# Independent V45 frame and invoice audit for PR #2979 + +**Result: partial positive audit of one local group and the aggregate profile. It does not independently validate the full supplier or select a new κ.** + +The selected conditional result remains κ = 0.001672660197076918. PR #2979 claims κ ≈ 0.0017290339826465135, about `0.0000563737855695955` above the selected value, but its status remains an unadmitted source archive. This audit independently reconstructs its V45 rank-7 frame group from the pinned parent words using explicit XOR-span closure, then checks the published final words and T74 aggregate arithmetic. It does not replay the full admission chain. + +For V45, all 61 edited gate frames are hyperplanes of their old frames, each lies in the shared rank-7 subspace, and every gate touching a lowered helper stays in that subspace. Both parent providers give the same result. The coordinated four-helper lowering changes the exact weighted local profile price by −8,388,172 units and leaves +22,972 after paying for four freed width units. The single-helper control loses: its price delta is −2,038,159 and its margin is −53,141. The five-group positive control independently reproduces all 139 stage-1 edits, the declared stage-1 local profile and the changed width inventory. + +Profiling the pinned final words directly reproduces `{1:2445, 2:706, 3:232, 4:108, 5:18, 8:8}` and `{4:26, 5:2, 6:16, 7:52, 8:99, 9:213}` for both providers. Their exact weighted change from the parent is −56,726,747 units, equal to the sum of the three published stage deltas. The T74 allocation profile pays all 666 local calls, leaves idle profile `{1:17310, 3:4956, 5:1728, 48:28190}`, and closes the exact rank-mass identity at 4,816,512. A separate 90-digit Decimal evaluation places the full-profile root at approximately `0.00172903398264651351771759`, consistent with the conservative value in the claim and above the selected κ. This is a numerical cross-check, not a new exact root certificate. + +## Reproduce + +From the repository root: + +```sh +python3.12 scripts/research_package.py --package research/rank7-v45-profile-audit --check-only +python3.12 scripts/research_package.py --package research/rank7-v45-profile-audit +``` + +The verifier reads only standard-library JSON/gzip inputs pinned in [SOURCES.json](SOURCES.json). + +## Limits + +Stages 2 and 3 are not independently rebuilt from the five extraction records and fourteen rewrite records; the final words are read as pinned inputs. The T74 owner schedule and physical allocation chronology, fresh native admission, and outer release are also not independently checked here. Consequently, the audit supports the V45 local cost mechanism but does not certify the complete κ claim or update the selected frontier. + +## Open next questions + +The next useful test is a source-bound reconstruction of the changed local profile through stages 2 and 3, followed by one independent check of T74 ownership chronology and the supplier cap. See the structured questions in [TASK.json](TASK.json). Do not start another lowering census until those obligations are closed or explicitly handed off. + +## Credit + +The audited construction and its predecessor chain remain credited in `research/rank7-joint-endframes/NOTICE` and its README: Dugongue / Marius-Paul Dumitrean for PR #2979, Jeremy Kothe for the PR #2957 rewrites, and all listed predecessor contributors. This small audit does not replace or absorb those contributions. Prepared with substantial AI assistance by OpenAI Codex; Apache-2.0. diff --git a/research/rank7-v45-profile-audit/SOURCES.json b/research/rank7-v45-profile-audit/SOURCES.json new file mode 100644 index 0000000000..1e772e0b4b --- /dev/null +++ b/research/rank7-v45-profile-audit/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/rank7-joint-endframes/CLAIM.json", + "usage": "input", + "git_blob": "8ec2ce4e440c0b584ee982c551e526a011c9324c", + "sha256": "436e0d297cbdf195445d3697d496ac675e95210b79e70ce602a6a6667a4c6ce9" + }, + { + "path": "research/rank7-joint-endframes/allocation/PROFILE.json", + "usage": "input", + "git_blob": "46a83eeda67ab67cccbffe8b7ad8e44368b40ea7", + "sha256": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf" + }, + { + "path": "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "usage": "input", + "git_blob": "14de38f85eedf4a96500173576184a439348328c", + "sha256": "b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e" + }, + { + "path": "research/rank7-joint-endframes/construction/STAGE-PRICES.json", + "usage": "input", + "git_blob": "b06b369ace05b86377f9f73e13586b62b0b77b98", + "sha256": "dfb7d06724bf95367f3fdb398f4828fc70f803d23030bc0eee0b00541457f546" + }, + { + "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" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-base.json.gz", + "usage": "input", + "git_blob": "d9aa96a93fea5f7395e7783aef0bc117c0a0ae89", + "sha256": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "usage": "input", + "git_blob": "74f6cb64595c21f7726ae77e69437868620bdcee", + "sha256": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7" + } + ] +} diff --git a/research/rank7-v45-profile-audit/TASK.json b/research/rank7-v45-profile-audit/TASK.json new file mode 100644 index 0000000000..9401e8b944 --- /dev/null +++ b/research/rank7-v45-profile-audit/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "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 the V45 rank-7 group and losing single-helper control from both pinned PR2942 parent providers, reproduce the five-group stage-1 profile, then trace the published final local profiles into the pinned T74 aggregate arithmetic.", + "scope_change_reason": "Refines the card's complete-invoice audit to the source-bound V45 group and aggregate profile arithmetic. The final words and T74 allocation are pinned inputs, so stages 2/3, ownership chronology and admission remain explicitly open rather than being treated as independently checked.", + "bottleneck_link": "The complex supplier is the selected binding side. An independent frame and price reconstruction tests whether the claimed coordinated group actually changes the local rank/width profile and whether the published T74 aggregate pays that local profile.", + "budget_minutes": 60, + "stop_rule": "Stop after the V45 local positive/single-negative controls, five-group profile control and pinned T74 aggregate arithmetic. Do not run another lowering census or claim a new selected kappa until stages 2/3, owner chronology and physical/native admission receive source-bound review.", + "outcome": "partial", + "evidence": "verify.py independently derives F2 spans by XOR closure, reconstructs the V45 and five-group profiles for both providers, reproduces the final local profiles and exact staged local-price sum, and checks the T74 rank-mass decomposition. A 90-digit Decimal root is only a numerical cross-check. It does not rebuild the stage-2/3 transformations, ownership chronology, native admission, or outer release. The local overlap cache was stale as of 2026-10-14; remote refresh failed, and the canonical .git metadata is read-only in this environment. The live family-status page was checked on 2026-10-17 and still reports priority revision 6.", + "author": "OpenAI Codex", + "ai_assistance": "Substantial AI assistance by OpenAI Codex for mathematical analysis, independent implementation and verification.", + "open_questions": [ + { + "question": "Can the five extraction transforms and fourteen rewrites be replayed independently into the pinned final word while preserving the independently reconstructed paid profile?", + "why_it_matters": "The current final-profile check trusts the package's final word as an input; rebinding it to the source transformations is required before the local profile can be attributed to the whole proposed mechanism.", + "first_step": "Write a separate stage-2/3 applier from the pinned transform and rewrite records, reconstruct both final providers from the stage-1 words, and compare proof-relevant canonical fields and the independently computed profile.", + "blocked_by": "Exact transform/rewrite records are available, but this audit session stopped after the scoped invoice arithmetic; another independent reconstruction is needed." + }, + { + "question": "Does the pinned T74 profile have an independently reconstructed legal owner chronology and physical stock bill for the changed inventory?", + "why_it_matters": "The aggregate profile and its moment do not show that all roles fit legal bins, lifetimes, and physical stock under the claimed schedule.", + "first_step": "Bind the final words to the exact T74 ORDER and DISPATCH inputs, reconstruct one complete owner chronology with an independent checker, and reconcile all 66,813 physical families and 91 private buffers.", + "blocked_by": "This package checks only aggregate T74 rank mass; the source owner's chronology and admission remain outside its verifier." + } + ] +} diff --git a/research/rank7-v45-profile-audit/VERIFY.json b/research/rank7-v45-profile-audit/VERIFY.json new file mode 100644 index 0000000000..e472bb135c --- /dev/null +++ b/research/rank7-v45-profile-audit/VERIFY.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/CLAIM.json", + "research/rank7-joint-endframes/allocation/PROFILE.json", + "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "research/rank7-joint-endframes/construction/STAGE-PRICES.json", + "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", + "research/rank7-joint-endframes/data/WORD-base.json.gz", + "research/rank7-joint-endframes/data/WORD-extra.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent XOR-span frame chronology and rank accounting for the V45 positive group and losing single-helper control; five-group stage-1 profile/inventory positive control; final base/extra local profiles and exact weighted stage-delta sum; T74 local-plus-idle rank-mass reconciliation and high-precision numeric root sanity check. Does not certify chronology, exact root, supplier admission or release." + } + ] +} diff --git a/research/rank7-v45-profile-audit/verify.py b/research/rank7-v45-profile-audit/verify.py new file mode 100644 index 0000000000..2d0594b993 --- /dev/null +++ b/research/rank7-v45-profile-audit/verify.py @@ -0,0 +1,311 @@ +#!/usr/bin/env python3 +"""Independent XOR-span reconstruction of #2979's V45 frame group and invoice arithmetic. + +This checks the source-bound local frame/profile arithmetic and cross-checks the +published T74 aggregate numerically. It does not rebuild stages 2/3, owners, +chronology, native admission, or the exact outer release. +""" +from collections import Counter +from copy import deepcopy +from decimal import Decimal as D, localcontext +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PKG = ROOT / "research" / "rank7-joint-endframes" + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if raw[:2] == b"\x1f\x8b" else raw) + + +@lru_cache(maxsize=100_000) +def _span(vectors): + """Return an F2 span by explicit closure, independent of RREF implementations.""" + out = {0} + for v in vectors: + old = tuple(out) + out.update(x ^ v for x in old) + return frozenset(out) + + +def span(vectors): + return _span(tuple(vectors)) + + +def rank(vectors): + n = len(span(vectors)) + need(n and n & (n - 1) == 0, "span cardinality is not a power of two") + return n.bit_length() - 1 + + +def inside(a, b): + return span(a).issubset(span(b)) + + +def dot_parity(a, b): + return (a & b).bit_count() & 1 + + +def profile(word): + full = span([1 << i for i in range(9)]) + ends = [full] * 112 + ends += [span(z for z in range(1, 512) if not dot_parity(z, p)) for p in word["ports"]] + ends += [full] * 480 + starts = [span([p]) for p in word["ports"]] + [frozenset()] * 592 + for r, rows in word["start_extra"].items(): + starts[int(r)] = span(rows) + for r, rows in word["helper_final"].items(): + ends[int(r)] = span(rows) + + current = list(starts) + paid = Counter() + + def climb(r, rows): + rows = span(rows) + need(inside(current[r], rows), f"nonmonotone register {r}") + d = rank(rows) - rank(current[r]) + if d: + paid[d] += 1 + current[r] = rows + + def step(gate): + if gate[0] == "warp": + need(current[gate[1]] == span(gate[3]), "warp entry frame") + current[gate[1]] = span(gate[4]) + elif gate[0] == "add": + climb(gate[1], gate[-1]) + climb(gate[2], gate[-1]) + elif gate[0] == "scale": + climb(gate[1], gate[-1]) + else: + raise AssertionError(("unknown gate", gate[0])) + + for gate in word["A"]: + step(gate) + for r, rows in zip(word["centers"], word["center_frames"]): + need(current[r] == span(rows), f"center entry frame {r}") + levels = [] + for cut in word["cut"]: + if cut[2] == r: + levels.append(span(word["target_levels"].get(str(cut[1] - 112), []))) + rows = span(rows) + for target in sorted(set(levels), key=len, reverse=True): + if rows != target: + paid[rank(rows) - rank(target)] += 1 + rows = target + warps = {} + for entry in word["warps"]: + warps.setdefault(entry[0], []).append(entry) + for pos in range(len(word["B"]) + 1): + for entry in warps.get(pos, []): + need(current[entry[1]] == span(entry[3]), "B warp entry frame") + current[entry[1]] = span(entry[4]) + if pos < len(word["B"]): + step(word["B"][pos]) + for gate in word["restore"]: + step(gate) + + live = set(range(704)) - set(word["removed"]) + for r in live: + climb(r, ends[r]) + inventory = Counter(rank(ends[r]) - rank(starts[r]) for r in live if r >= 224) + return dict(sorted(paid.items())), dict(sorted(inventory.items())) + + +def roles(gate): + return set(gate[1:3] if gate[0] == "add" else gate[1:2]) + + +def apply_groups(parent, record, chosen): + out = deepcopy(parent) + changed = [] + for name in chosen: + W, helpers = record["groups"][name] + W = span(W) + for h in helpers: + row = record["helper_final_changes"][str(h)] + need(parent["helper_final"][str(h)] == row["old"], "helper old-frame pin") + need(span(row["new"]) == W and rank(row["new"]) == 7, "shared rank-7 helper endpoint") + need(inside(row["new"], row["old"]), "helper endpoint containment") + out["helper_final"][str(h)] = list(row["new"]) + for edit in record["frame_edits"]: + owners = [name for name, (W, _) in record["groups"].items() if inside(edit["new_frame"], W)] + need(len(owners) == 1, ("unique frame-edit owner", edit["section"], edit["index"], owners)) + name = owners[0] + if name not in chosen: + continue + section, i = edit["section"], edit["index"] + gate = out[section][i] + need(gate[:-1] == edit["gate"] and span(gate[-1]) == span(edit["old_frame"]), "gate preimage pin") + need(rank(edit["new_frame"]) == rank(edit["old_frame"]) - 1, "gate codimension one") + need(inside(edit["new_frame"], edit["old_frame"]), "gate hyperplane containment") + need(inside(edit["new_frame"], record["groups"][name][0]), "gate is inside shared W") + gate[-1] = list(edit["new_frame"]) + changed.append((name, section, i)) + for name in chosen: + W = record["groups"][name][0] + for h in record["groups"][name][1]: + for section in ("A", "B", "restore"): + for i, gate in enumerate(out[section]): + if h in roles(gate): + need(inside(gate[-1], W), ("lowered-helper event outside W", name, h, section, i)) + return out, changed + + +def price(profile_, weights): + return sum(weights[r] * n for r, n in profile_.items()) + + +def dec_fraction(value): + q = Q(value) + return D(q.numerator) / D(q.denominator) + + +def decimal_root(profile_, replicas): + """High-precision numerical cross-check; intentionally not an exact certificate.""" + with localcontext() as ctx: + ctx.prec = 90 + denominator = D(73 * 896 * replicas) + + def moment(b): + terms = [] + for r, n in profile_.items(): + base = D(73) / D(r) + terms.append(D(n) * D(r) * (b * base.ln()).exp()) + return sum(terms, D(0)) / denominator + + low, high = D(0), D("0.01") + need(moment(low) < 1 < moment(high), "T74 moment root bracket") + for _ in range(320): + mid = (low + high) / 2 + if moment(mid) < 1: + low = mid + else: + high = mid + root = (low + high) / 2 + return root, moment(root) - 1 + + +def main(): + selected = read(ROOT / "certificates/selected-result.json") + record = read(PKG / "data/STAGE1-FRAME-EDITS.json") + prices = read(PKG / "construction/STAGE-PRICES.json") + claim = read(PKG / "CLAIM.json") + cap = read(PKG / "certificates/RELAX-CAP.json") + allocation = {int(k): int(v) for k, v in read(PKG / "allocation/PROFILE.json").items()} + weights = {int(k): int(v) for k, v in prices["weights"]["c"].items()} + break_even = int(prices["weights"]["break_even"]) + + rows = {} + for variant in ("base", "extra"): + parent = read(PKG / f"data/PARENT-{variant}.json.gz") + parent_profile, parent_inventory = profile(parent) + need(parent_profile == {int(k): v for k, v in parent["report"]["local_profile"].items()}, "independent parent profile") + need(parent_inventory == {int(k): v for k, v in parent["report"]["width_inventory"].items()}, "independent parent inventory") + + stage1, edits = apply_groups(parent, record, list(record["groups"])) + stage1_profile, stage1_inventory = profile(stage1) + need(len(edits) == 139, "all five groups account for 139 frame edits") + need(stage1_profile == {int(k): v for k, v in record["declared_local_profile"].items()}, "five-group local profile") + need(stage1_inventory == {int(k): v for k, v in record["declared_width_inventory"].items()}, "five-group width inventory") + + v45, v45_edits = apply_groups(parent, record, ["V45"]) + joint_profile, joint_inventory = profile(v45) + need(len(v45_edits) == 61, "V45 frame edit count") + only_one = deepcopy(v45) + v45_helpers = record["groups"]["V45"][1] + for h in v45_helpers[1:]: + only_one["helper_final"][str(h)] = deepcopy(parent["helper_final"][str(h)]) + one_profile, one_inventory = profile(only_one) + delta = lambda newer: price(newer, weights) - price(parent_profile, weights) + joint_delta, one_delta = delta(joint_profile), delta(one_profile) + joint_margin = -joint_delta - len(v45_helpers) * break_even + one_margin = -one_delta - break_even + need((joint_delta, joint_margin) == (-8_388_172, 22_972), "V45 coordinated price and margin") + need((one_delta, one_margin) == (-2_038_159, -53_141), "V45 losing single-helper control") + rows[variant] = { + "parent_profile": parent_profile, + "stage1_profile": stage1_profile, + "stage1_inventory": stage1_inventory, + "v45_profile": joint_profile, + "v45_inventory": joint_inventory, + "v45_edit_count": len(v45_edits), + "v45_delta_units": joint_delta, + "v45_margin_units": joint_margin, + "single_helper": v45_helpers[0], + "single_delta_units": one_delta, + "single_margin_units": one_margin, + "single_inventory": one_inventory, + } + need(rows["base"] == rows["extra"], "provider profile agreement") + + final_rows = {} + for variant in ("base", "extra"): + final = read(PKG / f"data/WORD-{variant}.json.gz") + final_profile, final_inventory = profile(final) + need(final_profile == {int(k): v for k, v in final["report"]["local_profile"].items()}, "independent final-word profile") + need(final_inventory == {int(k): v for k, v in final["report"]["width_inventory"].items()}, "independent final-word inventory") + final_rows[variant] = (final_profile, final_inventory) + need(final_rows["base"] == final_rows["extra"], "final provider profile agreement") + final_profile, final_inventory = final_rows["base"] + + total_delta = price(final_profile, weights) - price(rows["base"]["parent_profile"], weights) + stage_delta_sum = sum(int(prices[f"stage{i}"]["literal_price_units"]) for i in (1, 2, 3)) + need(total_delta == stage_delta_sum == -56_726_747, "final frame-price delta equals three published stage deltas") + need(final_inventory == {int(k): v for k, v in claim["width_inventory"].items()}, "claim width inventory matches independently profiled final word") + need(final_profile == {int(k): v for k, v in claim["local_profile"].items()}, "claim local profile matches independently profiled final word") + + calls, replicas = int(claim["calls"]), int(claim["replicas"]) + idle = dict(allocation) + for r, n in final_profile.items(): + idle[r] = idle.get(r, 0) - calls * n + need(all(n >= 0 for n in idle.values()), "T74 profile pays all 666 complete local calls") + idle = {r: n for r, n in sorted(idle.items()) if n} + need(sum(r * n for r, n in allocation.items()) == replicas * 65_088, "complete T74 rank-mass identity") + need(sum(r * n for r, n in final_profile.items()) * calls + sum(r * n for r, n in idle.items()) == replicas * 65_088, + "local plus idle profile closes T74 rank mass") + need(allocation == {int(k): v for k, v in claim["profile"].items()}, "T74 profile matches claim") + + root, root_residual = decimal_root(allocation, replicas) + selected_kappa = Q(selected["kappa"]) + claimed_kappa = Q(claim["kappa"]) + cap_lower = dec_fraction(cap["cap_lower"]) + cap_upper = dec_fraction(cap["cap_upper"]) + need(claimed_kappa > selected_kappa, "claimed candidate kappa strictly exceeds selected kappa") + need(root > dec_fraction(claim["complex_lower"]), "numerical T74 root exceeds claimed conservative complex lower bound") + need(root < cap_lower < cap_upper, "numerical T74 root lies below the fixed-inventory cap bracket") + need(D(0) < root - dec_fraction(claimed_kappa) < D("1e-24"), "claim is a conservative floor of the numerical T74 root") + + print(json.dumps({ + "status": "PASS_V45_INDEPENDENT_LOCAL_PROFILE_AND_T74_AGGREGATE_ARITHMETIC", + "v45": rows["base"], + "final_local_profile": final_profile, + "final_width_inventory": final_inventory, + "local_stage_delta_units": total_delta, + "sum_of_stage_deltas_units": stage_delta_sum, + "t74_profile": allocation, + "t74_idle_profile_after_666_calls": idle, + "t74_rank_mass": sum(r * n for r, n in allocation.items()), + "root_decimal_crosscheck_only": str(root), + "root_moment_residual_decimal": str(root_residual), + "claimed_kappa_minus_selected_exact": str(claimed_kappa - selected_kappa), + "limitations": [ + "Stages 2 and 3 are not independently reconstructed from their transform/rewrite records.", + "T74 ownership chronology, physical admission, native admission, and outer release are not independently audited here.", + "The Decimal root is a numeric cross-check, not an exact root certificate." + ] + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() From 8aee45e6a918c99cdca98431c3e791d2b3fd4206 Mon Sep 17 00:00:00 2001 From: Gonzalo-Mier Date: Sat, 17 Oct 2026 00:15:29 +0200 Subject: [PATCH 2/2] Research: replay rank-7 profile through all source stages --- research/rank7-v45-profile-audit/README.md | 8 +- research/rank7-v45-profile-audit/SOURCES.json | 36 ++++ research/rank7-v45-profile-audit/TASK.json | 16 +- research/rank7-v45-profile-audit/VERIFY.json | 8 +- research/rank7-v45-profile-audit/verify.py | 200 +++++++++++++++++- 5 files changed, 250 insertions(+), 18 deletions(-) diff --git a/research/rank7-v45-profile-audit/README.md b/research/rank7-v45-profile-audit/README.md index 3139f163d5..ac64dce837 100644 --- a/research/rank7-v45-profile-audit/README.md +++ b/research/rank7-v45-profile-audit/README.md @@ -2,11 +2,11 @@ **Result: partial positive audit of one local group and the aggregate profile. It does not independently validate the full supplier or select a new κ.** -The selected conditional result remains κ = 0.001672660197076918. PR #2979 claims κ ≈ 0.0017290339826465135, about `0.0000563737855695955` above the selected value, but its status remains an unadmitted source archive. This audit independently reconstructs its V45 rank-7 frame group from the pinned parent words using explicit XOR-span closure, then checks the published final words and T74 aggregate arithmetic. It does not replay the full admission chain. +The selected conditional result remains κ = 0.001672660197076918. PR #2979 claims κ ≈ 0.0017290339826465135, about `0.0000563737855695955` above the selected value, but its status remains an unadmitted source archive. This audit independently reconstructs its V45 rank-7 frame group from the pinned parent words using explicit XOR-span closure, then rebuilds the profile-bearing word sections through the five extraction transforms and fourteen literal rewrites for both providers. It also checks the published T74 aggregate arithmetic. It does not replay the full admission chain. For V45, all 61 edited gate frames are hyperplanes of their old frames, each lies in the shared rank-7 subspace, and every gate touching a lowered helper stays in that subspace. Both parent providers give the same result. The coordinated four-helper lowering changes the exact weighted local profile price by −8,388,172 units and leaves +22,972 after paying for four freed width units. The single-helper control loses: its price delta is −2,038,159 and its margin is −53,141. The five-group positive control independently reproduces all 139 stage-1 edits, the declared stage-1 local profile and the changed width inventory. -Profiling the pinned final words directly reproduces `{1:2445, 2:706, 3:232, 4:108, 5:18, 8:8}` and `{4:26, 5:2, 6:16, 7:52, 8:99, 9:213}` for both providers. Their exact weighted change from the parent is −56,726,747 units, equal to the sum of the three published stage deltas. The T74 allocation profile pays all 666 local calls, leaves idle profile `{1:17310, 3:4956, 5:1728, 48:28190}`, and closes the exact rank-mass identity at 4,816,512. A separate 90-digit Decimal evaluation places the full-profile root at approximately `0.00172903398264651351771759`, consistent with the conservative value in the claim and above the selected κ. This is a numerical cross-check, not a new exact root certificate. +The source replay reproduces the stage-2 profile `{1:2449, 2:710, 3:236, 4:102, 5:18, 8:8}` and the final profile `{1:2445, 2:706, 3:232, 4:108, 5:18, 8:8}`, with the claimed width inventory, for both providers. Its exact weighted stage deltas are −46,150,994, −10,523,403, and −52,350 units, summing to −56,726,747. A missing stage-2 frame change, stale rewrite preimage, and unshifted phase warp are rejected by negative controls. The T74 allocation profile pays all 666 local calls, leaves idle profile `{1:17310, 3:4956, 5:1728, 48:28190}`, and closes the exact rank-mass identity at 4,816,512. A separate 90-digit Decimal evaluation places the full-profile root at approximately `0.00172903398264651351771759`, consistent with the conservative value in the claim and above the selected κ. This is a numerical cross-check, not a new exact root certificate. ## Reproduce @@ -21,11 +21,11 @@ The verifier reads only standard-library JSON/gzip inputs pinned in [SOURCES.jso ## Limits -Stages 2 and 3 are not independently rebuilt from the five extraction records and fourteen rewrite records; the final words are read as pinned inputs. The T74 owner schedule and physical allocation chronology, fresh native admission, and outer release are also not independently checked here. Consequently, the audit supports the V45 local cost mechanism but does not certify the complete κ claim or update the selected frontier. +The stage-2/3 replay reconstructs only sections that determine the paid profile; it does not independently prove the extraction or rewrite operator identities, or reconstruct compensation and cleanup semantics. The T74 owner schedule and physical allocation chronology, fresh native admission, and outer release are also not independently checked here. Consequently, the audit does not certify the complete κ claim or update the selected frontier. ## Open next questions -The next useful test is a source-bound reconstruction of the changed local profile through stages 2 and 3, followed by one independent check of T74 ownership chronology and the supplier cap. See the structured questions in [TASK.json](TASK.json). Do not start another lowering census until those obligations are closed or explicitly handed off. +The next useful test is an independent reconstruction of T74 ownership chronology and the supplier cap, binding the replayed final word to the exact ORDER and DISPATCH inputs. See the structured questions in [TASK.json](TASK.json). Do not start another lowering census until those obligations are closed or explicitly handed off. ## Credit diff --git a/research/rank7-v45-profile-audit/SOURCES.json b/research/rank7-v45-profile-audit/SOURCES.json index 1e772e0b4b..9c69d1295b 100644 --- a/research/rank7-v45-profile-audit/SOURCES.json +++ b/research/rank7-v45-profile-audit/SOURCES.json @@ -50,12 +50,48 @@ "git_blob": "c39913ce24cbce4c841eabcc9b1e5a18e4ccc754", "sha256": "eded756dfe8f411c3d1f80a3ac16516f0ea5dd6f9866728b2179b157630fa7b6" }, + { + "path": "research/rank7-joint-endframes/data/REWRITES-2957.json", + "usage": "input", + "git_blob": "7bf1633c93951828159b0d9f17d65eda6877101a", + "sha256": "a37ade675876e4f5b00b33066c84f495fccd264863b7eb5d813837b1d01c3e7d" + }, { "path": "research/rank7-joint-endframes/data/STAGE1-FRAME-EDITS.json", "usage": "input", "git_blob": "66525d293bd0e615e469b4c2191281e8cafb8788", "sha256": "5fbfce004330ebc1fbac8de264614fe295f1a074811b478db4892c3bc3852cd3" }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-226.json", + "usage": "input", + "git_blob": "bab8518d199e902d72e3b8ec649b62afb74c4e77", + "sha256": "1732a39728c068f9d663111c7876b4e0b96088f3dd3b8e6ff824551b5a711338" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-228.json", + "usage": "input", + "git_blob": "0097d9dbb972126bde3551ac11d7421494e9c4ec", + "sha256": "82346e6a5173c4822e16b2dad06ca232111b6795a340079f9aceabe0098797c0" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-230.json", + "usage": "input", + "git_blob": "11edd2e513f8dfd224c53dd8f5ab6bd000098d3a", + "sha256": "8ad70d545695b5d2246fb9e09d46abcc1e42926c1161884f69b77f978a28f46d" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-363.json", + "usage": "input", + "git_blob": "9260bdf0b87319f212c0a7527693c511cd45c736", + "sha256": "84d2a609739eb30d4d9356fb6f04b2ff32c8823a978d7a51db1ace1d6d2352cc" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-395.json", + "usage": "input", + "git_blob": "fb2f6a9d2d72324d7dc7505ed46d566cdf8603c8", + "sha256": "065aa5d7713683942bc2156b543681857e33c6e2f30f32cba47e2cbb9d1bef69" + }, { "path": "research/rank7-joint-endframes/data/WORD-base.json.gz", "usage": "input", diff --git a/research/rank7-v45-profile-audit/TASK.json b/research/rank7-v45-profile-audit/TASK.json index 9401e8b944..e3fcbf63ca 100644 --- a/research/rank7-v45-profile-audit/TASK.json +++ b/research/rank7-v45-profile-audit/TASK.json @@ -46,21 +46,21 @@ ] }, "scope_status": "refined", - "actual_scope": "Independently reconstruct the V45 rank-7 group and losing single-helper control from both pinned PR2942 parent providers, reproduce the five-group stage-1 profile, then trace the published final local profiles into the pinned T74 aggregate arithmetic.", - "scope_change_reason": "Refines the card's complete-invoice audit to the source-bound V45 group and aggregate profile arithmetic. The final words and T74 allocation are pinned inputs, so stages 2/3, ownership chronology and admission remain explicitly open rather than being treated as independently checked.", + "actual_scope": "Independently reconstruct the V45 rank-7 group and losing single-helper control from both pinned PR2942 parent providers, replay the profile-bearing sections through the five stage-2 extraction transforms and fourteen stage-3 rewrites, reproduce all local profiles and weighted deltas, then reconcile the pinned T74 aggregate rank mass.", + "scope_change_reason": "After the bounded V45 and aggregate audit, a separate literal replay of stages 2/3 closed the missing source-binding for paid profile fields in both providers. The replay deliberately does not import the production applier and does not claim compensation, cleanup, operator-identity, owner, physical, or outer-release verification.", "bottleneck_link": "The complex supplier is the selected binding side. An independent frame and price reconstruction tests whether the claimed coordinated group actually changes the local rank/width profile and whether the published T74 aggregate pays that local profile.", "budget_minutes": 60, - "stop_rule": "Stop after the V45 local positive/single-negative controls, five-group profile control and pinned T74 aggregate arithmetic. Do not run another lowering census or claim a new selected kappa until stages 2/3, owner chronology and physical/native admission receive source-bound review.", + "stop_rule": "Do not run another lowering census or claim a new selected kappa until the extraction/rewrite identities, compensation and cleanup, T74 owner chronology, physical/native admission and outer release receive source-bound review.", "outcome": "partial", - "evidence": "verify.py independently derives F2 spans by XOR closure, reconstructs the V45 and five-group profiles for both providers, reproduces the final local profiles and exact staged local-price sum, and checks the T74 rank-mass decomposition. A 90-digit Decimal root is only a numerical cross-check. It does not rebuild the stage-2/3 transformations, ownership chronology, native admission, or outer release. The local overlap cache was stale as of 2026-10-14; remote refresh failed, and the canonical .git metadata is read-only in this environment. The live family-status page was checked on 2026-10-17 and still reports priority revision 6.", + "evidence": "verify.py independently derives F2 spans by XOR closure, reconstructs the V45 and five-group profiles for both providers, then source-replays the five extraction transforms and fourteen literal rewrites to reproduce the profile-bearing final word sections, all published stage prices, and the final profile/inventory. Omitted-frame, stale-preimage and unshifted-warp controls reject. It also checks the T74 rank-mass decomposition; the 90-digit Decimal root is only a numerical cross-check. The extraction/rewrite operator identities, compensation/cleanup semantics, T74 ownership chronology, physical/native admission and outer release remain open. Canonical main was fetched at d8e0f83f00191df62174b641e9fff055c357f641 with no changed guidance. The refreshed overlap cache covers 320 open PRs and 1,829 discussion records through 2026-10-16; focused reads covered #3042, #3050, #3051, #3054, and #3064.", "author": "OpenAI Codex", "ai_assistance": "Substantial AI assistance by OpenAI Codex for mathematical analysis, independent implementation and verification.", "open_questions": [ { - "question": "Can the five extraction transforms and fourteen rewrites be replayed independently into the pinned final word while preserving the independently reconstructed paid profile?", - "why_it_matters": "The current final-profile check trusts the package's final word as an input; rebinding it to the source transformations is required before the local profile can be attributed to the whole proposed mechanism.", - "first_step": "Write a separate stage-2/3 applier from the pinned transform and rewrite records, reconstruct both final providers from the stage-1 words, and compare proof-relevant canonical fields and the independently computed profile.", - "blocked_by": "Exact transform/rewrite records are available, but this audit session stopped after the scoped invoice arithmetic; another independent reconstruction is needed." + "question": "Can the extraction and rewrite identities, compensation updates, and cleanup be independently checked from the same source records?", + "why_it_matters": "The new replay establishes where the paid profile comes from, but a profile-bearing word alone does not prove that the composed stages preserve the exact borrowing operator or arbitrary dirty-state restoration.", + "first_step": "Use a code-disjoint symbolic action on the 632 independent inputs to check each extraction before/after identity and each literal rewrite, then recompute compensation and inverse cleanup from the reconstructed words.", + "blocked_by": "This package only rebuilds fields that determine local rank pricing; the complete equality semantics require a separate exact checker." }, { "question": "Does the pinned T74 profile have an independently reconstructed legal owner chronology and physical stock bill for the changed inventory?", diff --git a/research/rank7-v45-profile-audit/VERIFY.json b/research/rank7-v45-profile-audit/VERIFY.json index e472bb135c..c9b72ae2cf 100644 --- a/research/rank7-v45-profile-audit/VERIFY.json +++ b/research/rank7-v45-profile-audit/VERIFY.json @@ -11,7 +11,13 @@ "research/rank7-joint-endframes/construction/STAGE-PRICES.json", "research/rank7-joint-endframes/data/PARENT-base.json.gz", "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "research/rank7-joint-endframes/data/REWRITES-2957.json", "research/rank7-joint-endframes/data/STAGE1-FRAME-EDITS.json", + "research/rank7-joint-endframes/data/TRANSFORM-226.json", + "research/rank7-joint-endframes/data/TRANSFORM-228.json", + "research/rank7-joint-endframes/data/TRANSFORM-230.json", + "research/rank7-joint-endframes/data/TRANSFORM-363.json", + "research/rank7-joint-endframes/data/TRANSFORM-395.json", "research/rank7-joint-endframes/data/WORD-base.json.gz", "research/rank7-joint-endframes/data/WORD-extra.json.gz" ], @@ -23,7 +29,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Independent XOR-span frame chronology and rank accounting for the V45 positive group and losing single-helper control; five-group stage-1 profile/inventory positive control; final base/extra local profiles and exact weighted stage-delta sum; T74 local-plus-idle rank-mass reconciliation and high-precision numeric root sanity check. Does not certify chronology, exact root, supplier admission or release." + "checks": "Independent XOR-span frame chronology and rank accounting for the V45 positive group and losing single-helper control; five-group stage-1 profile/inventory positive control; source replay of five extraction transforms and fourteen literal rewrites for both providers, matching all paid-profile fields and published stage prices; omitted-frame, stale-preimage and unshifted-warp negative controls; T74 local-plus-idle rank-mass reconciliation and high-precision numeric root sanity check. Does not certify the free-operator identities, compensation/cleanup semantics, exact root, owner chronology, supplier admission or release." } ] } diff --git a/research/rank7-v45-profile-audit/verify.py b/research/rank7-v45-profile-audit/verify.py index 2d0594b993..a410dd2409 100644 --- a/research/rank7-v45-profile-audit/verify.py +++ b/research/rank7-v45-profile-audit/verify.py @@ -1,9 +1,10 @@ #!/usr/bin/env python3 -"""Independent XOR-span reconstruction of #2979's V45 frame group and invoice arithmetic. +"""Independent XOR-span reconstruction of #2979's staged profile arithmetic. -This checks the source-bound local frame/profile arithmetic and cross-checks the -published T74 aggregate numerically. It does not rebuild stages 2/3, owners, -chronology, native admission, or the exact outer release. +This rebuilds the profile-bearing word sections through stages 1-3 and checks +the pinned T74 aggregate numerically. It does not certify the extraction or +rewrite identities, compensation/cleanup semantics, owners, chronology, native +admission, or the exact outer release. """ from collections import Counter from copy import deepcopy @@ -162,6 +163,123 @@ def apply_groups(parent, record, chosen): return out, changed +def basis_by_closure(vectors): + """Choose an independent basis by explicit XOR closure, without RREF.""" + accepted = [] + current = {0} + for vector in sorted(set(vectors)): + if vector not in current: + accepted.append(vector) + current.update(value ^ vector for value in tuple(current)) + need(span(accepted) == span(vectors), "closure-selected basis spans its input") + return accepted + + +def apply_extraction(word, transform): + """Rebuild the profile-bearing part of one paired extraction from literal gates.""" + x = deepcopy(word) + helper = int(transform["helper"]) + need(str(helper) not in x["helper_final"] and str(helper) not in x["start_extra"], "new extraction helper") + prelude = int(x["prelude_events"]) + protected = set(map(int, x["helper_final"])) | set(map(int, x["start_extra"])) + protected |= {int(c["source"]) for c in x["initial_corrections"]} + removed = set(map(int, x["removed"])) + + before = transform["before"] + after = transform["after"] + need(before and after, "nonempty paired extraction") + for gate in before: + need(gate[0] in ("add", "scale") and gate[-1] == [], "extraction inputs use zero frames") + involved = gate[1:3] if gate[0] == "add" else gate[1:2] + need(all(224 <= int(r) < 704 and int(r) not in protected and int(r) not in removed + for r in involved), "extraction inputs touch only live unprotected helpers") + + normal = int(transform["normal"]) + hyperplane = [v for v in range(1, 512) if not dot_parity(v, normal)] + end_frame = basis_by_closure(hyperplane) + need(rank(end_frame) == 8 and all(not dot_parity(v, normal) for v in end_frame), + "extraction endpoint is the declared rank-8 hyperplane") + need(all(g[0] in ("add", "scale") and inside(g[-1], end_frame) for g in after), + "extraction outputs lie in the declared hyperplane") + + x["A"] = x["A"][:prelude] + deepcopy(before) + x["A"][prelude:] + x["restore"] += deepcopy(after) + x["helper_final"][str(helper)] = end_frame + seen = set() + for edit in transform["frame_changes"]: + section, index = edit["section"], int(edit["index"]) + need(section in ("A", "B", "restore") and (section, index) not in seen, + "unique extraction frame-change address") + need(0 <= index < len(x[section]) and (section != "A" or index >= prelude), + "extraction frame-change address is live") + seen.add((section, index)) + gate = x[section][index] + need(gate[:-1] == edit["gate"] and span(gate[-1]) == span(edit["old_frame"]), + "extraction frame-change preimage") + need(rank(edit["new_frame"]) == rank(edit["old_frame"]) - 1 and + inside(edit["new_frame"], edit["old_frame"]), "extraction frame change lowers one dimension") + gate[-1] = list(edit["new_frame"]) + return x + + +def apply_literal_rewrites(word, rewrites, shift_warps=True): + """Apply declared stage-3 splices by exact old slices and source indices.""" + x = deepcopy(word) + taken = {section: [] for section in ("A", "B", "restore")} + edits = [] + for rewrite in rewrites: + for edit in rewrite["edits"]: + section, start, stop = edit["section"], int(edit["start"]), int(edit["stop"]) + need(section in taken and 0 <= start <= stop <= len(word[section]), "rewrite slice address") + need(section != "A" or start >= int(word["prelude_events"]), "rewrites preserve prelude") + need(word[section][start:stop] == edit["old"] and edit["old"] != edit["new"], + "rewrite old slice is exact and nonvacuous") + for left, right in taken[section]: + need(stop < left or right < start, "declared rewrite slices are disjoint and separated") + taken[section].append((start, stop)) + edits.append((section, start, stop, edit["new"])) + + for section, start, stop, new in sorted(edits, key=lambda row: (row[0], -row[1], -row[2])): + x[section][start:stop] = deepcopy(new) + + b_edits = [(start, stop, len(new) - (stop - start)) + for section, start, stop, new in edits if section == "B"] + if shift_warps: + for warp in x["warps"]: + pos = int(warp[0]) + need(not any(start < pos < stop for start, stop, _ in b_edits), "warp outside edited B slices") + warp[0] = pos + sum(delta for start, stop, delta in b_edits if stop <= pos and start < pos) + return x + + +def profile_projection(word): + """Fields sufficient to determine the complete paid local profile and inventory.""" + names = ("A", "B", "restore", "warps", "ports", "start_extra", "helper_final", + "centers", "center_frames", "cut", "target_levels", "removed", "prelude_events") + return {name: word[name] for name in names} + + +def replay_stages(parent, record, transforms, rewrites): + """Bind stages 2/3 to source records and return their independently priced profiles.""" + stage1, _ = apply_groups(parent, record, list(record["groups"])) + stage2 = stage1 + step_profiles = [] + for expected_step, transform in enumerate(transforms, 1): + need(int(transform["step"]) == expected_step, "extraction order") + stage2 = apply_extraction(stage2, transform) + step_profiles.append(profile(stage2)) + after2 = profile(stage2) + stage3 = apply_literal_rewrites(stage2, rewrites) + after3 = profile(stage3) + return stage1, stage2, stage3, { + "stage2_step_profiles": step_profiles, + "stage2_profile": after2[0], + "stage2_inventory": after2[1], + "stage3_profile": after3[0], + "stage3_inventory": after3[1], + } + + def price(profile_, weights): return sum(weights[r] * n for r, n in profile_.items()) @@ -259,6 +377,71 @@ def main(): need(final_rows["base"] == final_rows["extra"], "final provider profile agreement") final_profile, final_inventory = final_rows["base"] + transforms = [read(PKG / f"data/TRANSFORM-{helper}.json") + for helper in (226, 228, 230, 363, 395)] + rewrites = read(PKG / "data/REWRITES-2957.json") + stage_replays = {} + for variant in ("base", "extra"): + parent = read(PKG / f"data/PARENT-{variant}.json.gz") + stage1, stage2, stage3, ledger = replay_stages(parent, record, transforms, rewrites) + final = read(PKG / f"data/WORD-{variant}.json.gz") + for name, actual, expected in (("stage2", ledger["stage2_profile"], profile(stage2)[0]), + ("stage3", ledger["stage3_profile"], profile(stage3)[0])): + need(actual == expected, f"{name} replay ledger reports its derived profile") + stage2_delta = price(profile(stage2)[0], weights) - price(profile(stage1)[0], weights) + stage3_delta = price(profile(stage3)[0], weights) - price(profile(stage2)[0], weights) + need(stage2_delta == int(prices["stage2"]["literal_price_units"]), "stage-2 source replay price") + need(stage3_delta == int(prices["stage3"]["literal_price_units"]), "stage-3 source replay price") + need(profile(stage3) == profile(final), "stage-2/3 replay reproduces both final local profile and inventory") + for field in ("A", "B", "restore", "warps", "ports", "start_extra", "centers", "center_frames", + "cut", "target_levels", "removed", "prelude_events"): + need(stage3[field] == final[field], f"stage-2/3 replay final {field} matches pinned word") + need(set(stage3["helper_final"]) == set(final["helper_final"]), "stage-2/3 replay endpoint inventory") + need(all(span(stage3["helper_final"][h]) == span(final["helper_final"][h]) + for h in final["helper_final"]), "stage-2/3 replay endpoints match pinned spans") + stage_replays[variant] = { + "stage1_delta_units": price(profile(stage1)[0], weights) - price(profile(parent)[0], weights), + "stage2_delta_units": stage2_delta, + "stage3_delta_units": stage3_delta, + "stage2_profile": profile(stage2)[0], + "stage2_inventory": profile(stage2)[1], + "final_profile": profile(stage3)[0], + "final_inventory": profile(stage3)[1], + } + need(stage_replays["base"] == stage_replays["extra"], "base/extra source replay agrees across stages 2/3") + need(stage_replays["base"]["stage1_delta_units"] == int(prices["stage1"]["literal_price_units"]), + "stage-1 source replay price") + + # Semantic failure controls for the new source-bound stage-2/3 replayer. + control_parent = read(PKG / "data/PARENT-base.json.gz") + control_stage1, _ = apply_groups(control_parent, record, list(record["groups"])) + omitted_frame = deepcopy(transforms) + omitted_frame[1]["frame_changes"] = [] + wrong_stage2 = control_stage1 + for transform in omitted_frame: + wrong_stage2 = apply_extraction(wrong_stage2, transform) + wrong_stage3 = apply_literal_rewrites(wrong_stage2, rewrites) + need(profile(wrong_stage3) != profile(read(PKG / "data/WORD-base.json.gz")), + "omitting the declared stage-2 frame change is detected by the final paid profile") + + stale_rewrites = deepcopy(rewrites) + stale_edit = next(edit for rewrite in stale_rewrites for edit in rewrite["edits"] if edit["old"]) + stale_edit["start"] += 1 + stale_edit["stop"] += 1 + try: + apply_literal_rewrites(stage2, stale_rewrites) + except AssertionError: + stale_rewrite_rejected = True + else: + need(False, "stale stage-3 rewrite preimage must be rejected") + unshifted_warps = apply_literal_rewrites(stage2, rewrites, shift_warps=False) + try: + profile(unshifted_warps) + except AssertionError: + unshifted_warp_rejected = True + else: + need(False, "unshifted B-phase warp must be rejected by the profile replay") + total_delta = price(final_profile, weights) - price(rows["base"]["parent_profile"], weights) stage_delta_sum = sum(int(prices[f"stage{i}"]["literal_price_units"]) for i in (1, 2, 3)) need(total_delta == stage_delta_sum == -56_726_747, "final frame-price delta equals three published stage deltas") @@ -293,6 +476,12 @@ def main(): "final_width_inventory": final_inventory, "local_stage_delta_units": total_delta, "sum_of_stage_deltas_units": stage_delta_sum, + "source_replayed_stages_1_to_3": stage_replays["base"], + "stage_replay_controls": { + "omitted_stage2_frame_change_detected": True, + "stale_stage3_preimage_rejected": stale_rewrite_rejected, + "unshifted_stage3_warp_rejected": unshifted_warp_rejected, + }, "t74_profile": allocation, "t74_idle_profile_after_666_calls": idle, "t74_rank_mass": sum(r * n for r, n in allocation.items()), @@ -300,7 +489,8 @@ def main(): "root_moment_residual_decimal": str(root_residual), "claimed_kappa_minus_selected_exact": str(claimed_kappa - selected_kappa), "limitations": [ - "Stages 2 and 3 are not independently reconstructed from their transform/rewrite records.", + "Stage-2/3 replay checks the profile-bearing word sections and prices, not compensation or cleanup semantics.", + "The extracted operator identities and the fourteen rewrite identities are not independently certified here.", "T74 ownership chronology, physical admission, native admission, and outer release are not independently audited here.", "The Decimal root is a numeric cross-check, not an exact root certificate." ]